# Changeset 2625

Ignore:
Timestamp:
Feb 6, 2013, 8:14:38 PM (6 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2622 as \texttt{cl\_other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds if the next instruction to be executed in $s_2$ follows the function call to be executed in (the witness of the $\Sigma$-type) $s_1$. to be executed in (the witness of the $\Sigma$-type) $s_1$. The two functions \texttt{as\_label} and \texttt{as\_cost\_ident} are used to extract the cost label/function call target from states whose next instruction is a cost emission/function call statement. \end{comment} A \texttt{trace\_label\_return} is isomorphic to a list of \texttt{trace\_label\_label}s that end with a cost emission followed by a \texttt{trace\_label\_label} that ends with a return. The interesting cases are those of $(\texttt{trace\_any\_label}~b~s_1~s_2)$. \texttt{trace\_label\_label}s that ends with a cost emission followed by a return terminated \texttt{trace\_label\_label}. The interesting cases are those of $\texttt{trace\_any\_label}~b~s_1~s_2$. A \texttt{trace\_any\_label} is a sequence of steps built by a syntax directed definition on the classification of $s_1$. The constructors of the datatype \begin{enumerate} \item the trace is never empty; it ends with a return iff $b$ is true (\texttt{ends\_with\_ret}) true \item a jump must always be the last instruction of the trace, and it must be followed by a cost emission statement; i.e. the target of a jump \item a cost emission statement can never occur inside the trace, only in the status immediately after \item the trace for a function call step is made from a subtrace of type $(\texttt{trace\_label\_return}~s_1~s_2)$, possibly followed by the \item the trace for a function call step is made of a subtrace for the function body of type $\texttt{trace\_label\_return}~s_1~s_2$, possibly followed by the rest of the trace for this basic block. The subtrace represents the function execution. Being an inductive datum, it grants totality of instruction is a cost emission statement. We only show here the type of one of them: \begin{verbatim} \begin{alltt} flatten_trace_label_return: (S: abstract_status) (start_status: S) (final_status: S) (the_trace: trace_label_return S start_status final_status) on the_trace: list (as_cost_label S) \end{verbatim} $$\forall$$S: abstract_status. $$\forall$$$$s_1,s_2$$. trace_label_return $$s_1$$ $$s_2$$ $$\to$$ list (as_cost_label S) \end{alltt} \paragraph{Cost prediction on structured traces} The first main theorem of CerCo about structured traces The first main theorem of CerCo about traces (theorem \texttt{compute\_max\_trace\_label\_return\_cost\_ok\_with\_trace}) holds for the of the structured traces to the concrete status of object code programs. Simplifying a bit, it states that $\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2. clock~s_2 = clock~s_1 + \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau} k(L(s))$ where $L$ maps a labelled state to its emitted label, and the \label{th1} \begin{array}{l}\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~ \texttt{clock}~s_2 = \texttt{clock}~s_1 + \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau)}\;k(\mathcal{L}(s)) \end{array} where $\mathcal{L}$ maps a labelled state to its emitted label, and the cost model $k$ is statically computed from the object code by associating to each label \texttt{L} the sum of the cost of the instructions interested only in those compiler passes that maps a trace $\tau_1$ to a trace $\tau_2$ such that \begin{displaymath}(\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2)\label{condition1}\end{displaymath} The reason is that when this happens we obviously have the following corollary to the previous theorem: $$\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2. clock~s_2 - clock~s_1 = \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau_1} k(L(s)) = \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau_2} k(L(s))$$ The corollary states that the actual execution time of the program can be computed equally well on the source or target language. Thus it becomes possible to $$\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2\label{condition1}\label{th2}$$ The reason is that the combination of~\ref{th1} with~\ref{th2} yields the corollary \begin{array}{l}\label{th3} \forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~~~~\; clock~s_2 - clock~s_1\\~ = \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau_1)}\;k(\mathcal{L}(s))\\~ = \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau_2)}\;k(\mathcal{L}(s)) \end{array} This corollary states that the actual execution time of the program can be computed equally well on the source or target language. Thus it becomes possible to transfer the cost model from the target to the source code and reason on the source code only. We are therefore interested in conditions stronger than~\ref{condition1}. Therefore we introduce here a similarity relation between traces that captures the fact that two traces have the same structure and that implies~\ref{condition1} (theorem \texttt{tlr\_rel\_to\_traces\_same\_flatten}). Two traces are similar when one can be obtained from the other by erasing or inserting steps classified as \texttt{other} into the \texttt{trace\_any\_label} blocks of the trace. In particular, Therefore we introduce here a similarity relation between traces with the same structure. Theorem~\texttt{tlr\_rel\_to\_traces\_same\_flatten} in the Matita formalization shows that~\ref{th2} holds for every pair $(\tau_1,\tau_2)$ of similar traces. Intuitively, two traces are similar when one can be obtained from the other by erasing or inserting silent steps, i.e. states that are not \texttt{as\_costed} and that are classified as \texttt{other}. Silent steps do not alter the structure of the traces. In particular, the relation maps function calls to function calls to the same function, label emission statements to emissions of the same label, concatenation of the same emissione statement, etc. The similarity relation definition if simple, but it involves a large number of cases. In the formalization, we define $(\texttt{tlr\_rel}~tlr_1~tlr_2)$ by structural recursion on $tlr_1$ and pattern matching over $tlr_2$. Here we turn In the formalization the three similarity relations --- one for each trace kind --- are defined by structural recursion on the first trace and pattern matching over the second. Here we turn the definition into inference rules for the sake of readability. We also omit from trace constructors all arguments, but those that are traces or that In the preceding rules, a $taa$ is an inhabitant of the $(\texttt{trace\_any\_any}~s_1~s_2)$ inductive data type whose definition we do not give in the paper for lack of space. It is the type of valid $\texttt{trace\_any\_any}~s_1~s_2$ inductive data type whose definition is not in the paper for lack of space. It is the type of valid prefixes (even empty ones) of \texttt{trace\_any\_label}s that do not contain any function call. Therefore it is possible to concatenate (using $@$'') a \texttt{trace\_any\_any} to the left of a \texttt{trace\_any\_label}. The intuition is that two traces are similar if one of them can perform more silent (non observables) moves, whose sequences are here represented by \texttt{trace\_any\_any}. left of a \texttt{trace\_any\_label}. A \texttt{trace\_any\_any} captures a sequence of silent moves. The \texttt{tal\_collapsable} unary predicate over \texttt{trace\_any\_label}s forward simulation is the existence of a relation $R$ over states such that if $s_1 R s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that $s_1' \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the $s_2 \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the one and multi step transition relations $\to^n$ with the existence of a structured trace between the two states, and we need to add the request that in the general case. To understand why, consider the case of a function call and the pass that fixes the parameter passing conventions. A function call in the source code takes in input an arbitrary number of pseudo-registers (the actual parameters to pass) and returns an arbitrary number of pseudo-registers (where the result is stored). A function call in the target call has no call in the source code takes in input an arbitrary number of pseudo-registers (the actual parameters to pass) and returns an arbitrary number of pseudo-registers (where the result is stored). A function call in the target language has no input nor output parameters. The pass must add explicit code before and after the function call to move the pseudo-registers content from/to the hardware For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and $\texttt{as\_execute}~s_1~s_1'$, and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ or $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ and $(\texttt{as\_costed}~s_1')$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either $\texttt{as\_costed}~s_1'$, there exists an $s_2'$ and a $\texttt{trace\_any\_any\_free}~s_2~s_2'$ called $taaf$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}. \end{condition} In the above condition, a $(\texttt{trace\_any\_any\_free}~s_1~s_2)$ is an In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ is an inductive type of structured traces that do not contain function calls or cost emission statements. Differently from a \texttt{trace\_any\_any}, the \begin{condition}[Case \texttt{cl\_call}] For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $taa_1$ of type $(\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that: For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$ and $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $\texttt{trace\_any\_any}~s_2~s_b$, and a $\texttt{trace\_any\_any\_free}~s_a~s_2'$ such that: $s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of the two call states are the same, $s_1 \mathcal{C} s_b$, the predicate $(\texttt{as\_execute}~s_b~s_a)$ holds, $s_1' \mathcal{L} s_b$ and the two call states are the same, $s_1 \mathcal{C} s_b$, $\texttt{as\_execute}~s_b~s_a$ holds, $s_1' \mathcal{L} s_b$ and $s_1' \mathcal{S} s_2'$. \end{condition}