Feb 6, 2013, 11:11:29 PM (9 years ago)


1 edited


  • Papers/itp-2013/ccexec.tex

    r2631 r2632  
    806806$s_1$ to $s_1'$ and $s_1 R s_2$ there exists an $s_2'$ such that
    807807$s_1' R s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
    808 $\tau_1 \approx \tau_2$.\\
     808$\tau_1$ is similar to $\tau_2$. We call this particular form of forward
     809simulation \emph{trace reconstruction}.
    810811The statement just introduced, however, is too simplicistic and not provable
    838839Therefore we now introduce an abstract notion of relation set between abstract
    839 statuses and an abstract notion of 1-to-0-or-many forward simulation. These
    840 two definitions enjoy the following remarkable properties:
     840statuses and an abstract notion of 1-to-0-or-many forward simulation conditions.
     841These two definitions enjoy the following remarkable properties:
    842843 \item they are generic enough to accomodate all passes of the CerCo compiler
    843  \item they allow to lift the 1-to-0-or-many forward simulation to the
    844    structured traces preserving forward simulation we are interested in
     844 \item the conjunction of the 1-to-0-or-many forward simulation conditions are
     845       just slightly stricter than the statement of a 1-to-0-or-many forward
     846       simulation in the classical case. In particular, they only require
     847       the construction of very simple forms of structured traces made of
     848       silent states only.
     849 \item they allow to prove our main result of the paper: the 1-to-0-or-many
     850       forward simulation conditions are sufficient to prove the trace
     851       reconstruction theorem
    847 The latter lifting is proved by the following theorem which has the
    848 1-to-0-or-many forward simulation statement as an hypothesis. Combined with
    849 the results in the previous section, it has as a corollary that the cost
    850 model can be computed on the object code and lifted to the source code to
    851 reason on non-functional properties iff a simpler 1-to-0-or-many forward
    852 simulation is proved. The statement of the latter is way more complex than a
    853 traditional 1-to-0-or-many forward simulation statement, but proofs have now
    854 about the same complexity. Indeed, it should be possible to largely reuse an
    855 existent traditional forward simulation proof. The lifting theorem below,
    856 proved once and for all in this paper, is the one that does all the job to
    857 put the labelling approach in motion.
     854Point 3. is the important one. First of all it means that we have reduced
     855the complex problem of trace reconstruction to a much simpler one that,
     856moreover, can be solved with slight adaptations of the forward simulation proof
     857that is performed for a compiler that only cares about functional properties.
     858Therefore we have successfully splitted as much as possible the proof of
     859preservation of functional properties from that of non-functional ones.
     860Secondly, combined with the results in the previous section, it implies
     861that the cost model can be computed on the object code and lifted to the
     862source code to reason on non-functional properties, assuming that
     863the 1-to-0-or-many forward simulation conditions are fullfilled for every
     864compiler pass.
     866\paragraph{Relation sets}
     868We introduce now the four relations $\mathcal{S,C,L,R}$ between abstract
     869statuses that are used to correlate the corresponding statues before and
     870after a compiler pass. The first two are abstract and must be instantiated
     871by every pass. The remaining two are derived relations.
     873The $\mathcal{S}$ relation between states is the classical relation used
     874in forward simulation proofs. It correlates the data of the status
     875(e.g. registers, memory, etc.).
     877The $\mathcal{C}$ relation correlates call states. It allows to track the
     878position in the target code of every call in the source code.
     880The $\mathcal{L}$ relation simply says that the two states are both label
     881emitting states that emit the same label. It allows to track the position in
     882the target code of every cost emitting statement in the source code.
     884Finally the $\mathcal{R}$ relation is the more complex one. Two states
     885$s_1$ and $s_2$ are $\mathcal{R}$ correlated if every time $s_1$ is the
     886successors of a call state that is $\mathcal{C}$-related to a call state
     887$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$.
     888We will require all pairs of states that follow a related call to be
     889$\mathcal{R}$-related. This is the fundamental requirement to grant
     890that the target trace is well structured, i.e. that function calls are well
     891nested and always return where they are supposed to.
     894record status_rel (S1,S2 : abstract_status) : Type[1] := \{
     895  \(\mathcal{S}\): S1 \(\to\) S2 \(\to\) Prop;
     896  \(\mathcal{C}\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\)
     897     (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop \}.
     899definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
     901definition \(\mathcal{R}\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
     902 \(\forall\)s1_pre,s2_pre.
     903  as_after_return s1_pre s1_ret \(\to\) s1_pre \(\mathcal{R}\) s2_pre \(\to\)
     904   as_after_return s2_pre s2_ret.
     907\paragraph{1-to-0-or-many forward simulation conditions}
    859908\begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}]
    860909 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and
    1002 \begin{alltt}
    1003 record status_rel (S1,S2 : abstract_status) : Type[1] := \{
    1004   \(\mathcal{S}\): S1 \(\to\) S2 \(\to\) Prop;
    1005   \(\mathcal{C}\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\) (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop
    1006   \}.
    1008 definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
    1010 definition \(\mathcal{R}\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
    1011  \(\forall\)s1_pre,s2_pre.
    1012   as_after_return s1_pre s1_ret \(\to\) call_rel s1_pre s2_pre \(\to\)
    1013    as_after_return s2_pre s2_ret.
    1014 \end{alltt}
     1051\paragraph{Main result: the 1-to-0-or-many forward simulation conditions
     1052are sufficient to trace reconstruction}
     1054Let us assume that a relation set is given such that the 1-to-0-or-many
     1055forward simulation conditions are satisfied. Under this assumption we
     1056can prove the following three trace reconstruction theorems by mutual
     1057structural induction over the traces given in input between the
     1058$s_1$ and $s_1'$ states.
     1060In particular, the \texttt{status\_simulation\_produce\_tlr} theorem
     1061applied to the \texttt{main} function of the program and equal
     1062$s_{2_b}$ and $s_2$ states shows that, for every initial state in the
     1063source code that induces a structured trace in the source code,
     1064the compiled code produces a similar structured trace.
    10261076$s_1' \mathcal{R} s_{2_m}$.
     1079The theorem states that a \texttt{trace\_label\_return} in the source code
     1080together with a precomputed preamble of silent states
     1081(the \texttt{trace\_any\_any}) in the target code induces a
     1082similar \texttt{trace\_label\_return} trace in the target code which can be
     1083followed by a sequence of silent states. Note that the statement does not
     1084require the produced \texttt{trace\_label\_return} trace to start with the
     1085precomputed preamble, even if this is likely to be the case in concrete
     1086implementations. The preamble in input is necessary for compositionality, e.g.
     1087because the 1-to-0-or-many forward simulation conditions allow in the
     1088case of function calls to execute a preamble of silent instructions just after
     1089the function call.
    10291092For every $s_1,s_1',s_{2_b},s_2$ s.t.
     1111The statement is similar to the previous one: a source
     1112\texttt{trace\_label\_label} and a given target preamble of silent states
     1113in the target code induce a similar \texttt{trace\_label\_label} in the
     1114target code, possibly followed by a sequence of silent moves that become the
     1115preamble for the next \texttt{trace\_label\_label} translation.
    10481118For every $s_1,s_1',s_2$ s.t.
     1138The statement is also similar to the previous ones, but for the lack of
     1139the target code preamble.
Note: See TracChangeset for help on using the changeset viewer.