# Changeset 2632 for Papers/itp-2013/ccexec.tex

Ignore:
Timestamp:
Feb 6, 2013, 11:11:29 PM (8 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2631 $s_1$ to $s_1'$ and $s_1 R s_2$ there exists an $s_2'$ such that $s_1' R s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that $\tau_1 \approx \tau_2$.\\ $\tau_1$ is similar to $\tau_2$. We call this particular form of forward simulation \emph{trace reconstruction}. The statement just introduced, however, is too simplicistic and not provable Therefore we now introduce an abstract notion of relation set between abstract statuses and an abstract notion of 1-to-0-or-many forward simulation. These two definitions enjoy the following remarkable properties: statuses and an abstract notion of 1-to-0-or-many forward simulation conditions. These two definitions enjoy the following remarkable properties: \begin{enumerate} \item they are generic enough to accomodate all passes of the CerCo compiler \item they allow to lift the 1-to-0-or-many forward simulation to the structured traces preserving forward simulation we are interested in \item the conjunction of the 1-to-0-or-many forward simulation conditions are just slightly stricter than the statement of a 1-to-0-or-many forward simulation in the classical case. In particular, they only require the construction of very simple forms of structured traces made of silent states only. \item they allow to prove our main result of the paper: the 1-to-0-or-many forward simulation conditions are sufficient to prove the trace reconstruction theorem \end{enumerate} The latter lifting is proved by the following theorem which has the 1-to-0-or-many forward simulation statement as an hypothesis. Combined with the results in the previous section, it has as a corollary that the cost model can be computed on the object code and lifted to the source code to reason on non-functional properties iff a simpler 1-to-0-or-many forward simulation is proved. The statement of the latter is way more complex than a traditional 1-to-0-or-many forward simulation statement, but proofs have now about the same complexity. Indeed, it should be possible to largely reuse an existent traditional forward simulation proof. The lifting theorem below, proved once and for all in this paper, is the one that does all the job to put the labelling approach in motion. Point 3. is the important one. First of all it means that we have reduced the complex problem of trace reconstruction to a much simpler one that, moreover, can be solved with slight adaptations of the forward simulation proof that is performed for a compiler that only cares about functional properties. Therefore we have successfully splitted as much as possible the proof of preservation of functional properties from that of non-functional ones. Secondly, combined with the results in the previous section, it implies that the cost model can be computed on the object code and lifted to the source code to reason on non-functional properties, assuming that the 1-to-0-or-many forward simulation conditions are fullfilled for every compiler pass. \paragraph{Relation sets} We introduce now the four relations $\mathcal{S,C,L,R}$ between abstract statuses that are used to correlate the corresponding statues before and after a compiler pass. The first two are abstract and must be instantiated by every pass. The remaining two are derived relations. The $\mathcal{S}$ relation between states is the classical relation used in forward simulation proofs. It correlates the data of the status (e.g. registers, memory, etc.). The $\mathcal{C}$ relation correlates call states. It allows to track the position in the target code of every call in the source code. The $\mathcal{L}$ relation simply says that the two states are both label emitting states that emit the same label. It allows to track the position in the target code of every cost emitting statement in the source code. Finally the $\mathcal{R}$ relation is the more complex one. Two states $s_1$ and $s_2$ are $\mathcal{R}$ correlated if every time $s_1$ is the successors of a call state that is $\mathcal{C}$-related to a call state $s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. We will require all pairs of states that follow a related call to be $\mathcal{R}$-related. This is the fundamental requirement to grant that the target trace is well structured, i.e. that function calls are well nested and always return where they are supposed to. \begin{alltt} record status_rel (S1,S2 : abstract_status) : Type[1] := \{ $$\mathcal{S}$$: S1 $$\to$$ S2 $$\to$$ Prop; $$\mathcal{C}$$: ($$\Sigma$$s.as_classifier S1 s cl_call) $$\to$$ ($$\Sigma$$s.as_classifier S2 s cl_call) $$\to$$ Prop \}. definition $$\mathcal{L}$$ S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2. definition $$\mathcal{R}$$ S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝ $$\forall$$s1_pre,s2_pre. as_after_return s1_pre s1_ret $$\to$$ s1_pre $$\mathcal{R}$$ s2_pre $$\to$$ as_after_return s2_pre s2_ret. \end{alltt} \paragraph{1-to-0-or-many forward simulation conditions} \begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}] For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and \end{comment} \begin{alltt} record status_rel (S1,S2 : abstract_status) : Type[1] := \{ $$\mathcal{S}$$: S1 $$\to$$ S2 $$\to$$ Prop; $$\mathcal{C}$$: ($$\Sigma$$s.as_classifier S1 s cl_call) $$\to$$ ($$\Sigma$$s.as_classifier S2 s cl_call) $$\to$$ Prop \}. definition $$\mathcal{L}$$ S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2. definition $$\mathcal{R}$$ S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝ $$\forall$$s1_pre,s2_pre. as_after_return s1_pre s1_ret $$\to$$ call_rel s1_pre s2_pre $$\to$$ as_after_return s2_pre s2_ret. \end{alltt} \paragraph{Main result: the 1-to-0-or-many forward simulation conditions are sufficient to trace reconstruction} Let us assume that a relation set is given such that the 1-to-0-or-many forward simulation conditions are satisfied. Under this assumption we can prove the following three trace reconstruction theorems by mutual structural induction over the traces given in input between the $s_1$ and $s_1'$ states. In particular, the \texttt{status\_simulation\_produce\_tlr} theorem applied to the \texttt{main} function of the program and equal $s_{2_b}$ and $s_2$ states shows that, for every initial state in the source code that induces a structured trace in the source code, the compiled code produces a similar structured trace. \begin{theorem}[\texttt{status\_simulation\_produce\_tlr}] $s_1' \mathcal{R} s_{2_m}$. \end{theorem} The theorem states that a \texttt{trace\_label\_return} in the source code together with a precomputed preamble of silent states (the \texttt{trace\_any\_any}) in the target code induces a similar \texttt{trace\_label\_return} trace in the target code which can be followed by a sequence of silent states. Note that the statement does not require the produced \texttt{trace\_label\_return} trace to start with the precomputed preamble, even if this is likely to be the case in concrete implementations. The preamble in input is necessary for compositionality, e.g. because the 1-to-0-or-many forward simulation conditions allow in the case of function calls to execute a preamble of silent instructions just after the function call. \begin{theorem}[\texttt{status\_simulation\_produce\_tll}] For every $s_1,s_1',s_{2_b},s_2$ s.t. \end{itemize} \end{theorem} The statement is similar to the previous one: a source \texttt{trace\_label\_label} and a given target preamble of silent states in the target code induce a similar \texttt{trace\_label\_label} in the target code, possibly followed by a sequence of silent moves that become the preamble for the next \texttt{trace\_label\_label} translation. \begin{theorem}[\texttt{status\_simulation\_produce\_tal}] For every $s_1,s_1',s_2$ s.t. \end{itemize} \end{theorem} The statement is also similar to the previous ones, but for the lack of the target code preamble. \begin{comment}