Changeset 2632 for Papers/itp2013
 Timestamp:
 Feb 6, 2013, 11:11:29 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec.tex
r2631 r2632 806 806 $s_1$ to $s_1'$ and $s_1 R s_2$ there exists an $s_2'$ such that 807 807 $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 809 simulation \emph{trace reconstruction}. 809 810 810 811 The statement just introduced, however, is too simplicistic and not provable … … 837 838 838 839 Therefore we now introduce an abstract notion of relation set between abstract 839 statuses and an abstract notion of 1to0ormany forward simulation . These840 two definitions enjoy the following remarkable properties:840 statuses and an abstract notion of 1to0ormany forward simulation conditions. 841 These two definitions enjoy the following remarkable properties: 841 842 \begin{enumerate} 842 843 \item they are generic enough to accomodate all passes of the CerCo compiler 843 \item they allow to lift the 1to0ormany forward simulation to the 844 structured traces preserving forward simulation we are interested in 844 \item the conjunction of the 1to0ormany forward simulation conditions are 845 just slightly stricter than the statement of a 1to0ormany 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 1to0ormany 850 forward simulation conditions are sufficient to prove the trace 851 reconstruction theorem 845 852 \end{enumerate} 846 853 847 The latter lifting is proved by the following theorem which has the 848 1to0ormany 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 nonfunctional properties iff a simpler 1to0ormany forward 852 simulation is proved. The statement of the latter is way more complex than a 853 traditional 1to0ormany 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. 858 854 Point 3. is the important one. First of all it means that we have reduced 855 the complex problem of trace reconstruction to a much simpler one that, 856 moreover, can be solved with slight adaptations of the forward simulation proof 857 that is performed for a compiler that only cares about functional properties. 858 Therefore we have successfully splitted as much as possible the proof of 859 preservation of functional properties from that of nonfunctional ones. 860 Secondly, combined with the results in the previous section, it implies 861 that the cost model can be computed on the object code and lifted to the 862 source code to reason on nonfunctional properties, assuming that 863 the 1to0ormany forward simulation conditions are fullfilled for every 864 compiler pass. 865 866 \paragraph{Relation sets} 867 868 We introduce now the four relations $\mathcal{S,C,L,R}$ between abstract 869 statuses that are used to correlate the corresponding statues before and 870 after a compiler pass. The first two are abstract and must be instantiated 871 by every pass. The remaining two are derived relations. 872 873 The $\mathcal{S}$ relation between states is the classical relation used 874 in forward simulation proofs. It correlates the data of the status 875 (e.g. registers, memory, etc.). 876 877 The $\mathcal{C}$ relation correlates call states. It allows to track the 878 position in the target code of every call in the source code. 879 880 The $\mathcal{L}$ relation simply says that the two states are both label 881 emitting states that emit the same label. It allows to track the position in 882 the target code of every cost emitting statement in the source code. 883 884 Finally 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 886 successors 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'$. 888 We will require all pairs of states that follow a related call to be 889 $\mathcal{R}$related. This is the fundamental requirement to grant 890 that the target trace is well structured, i.e. that function calls are well 891 nested and always return where they are supposed to. 892 893 \begin{alltt} 894 record 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 \}. 898 899 definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2. 900 901 definition \(\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. 905 \end{alltt} 906 907 \paragraph{1to0ormany forward simulation conditions} 859 908 \begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}] 860 909 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and … … 1000 1049 \end{comment} 1001 1050 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 \}. 1007 1008 definition \(\mathcal{L}\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2. 1009 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 1to0ormany forward simulation conditions 1052 are sufficient to trace reconstruction} 1053 1054 Let us assume that a relation set is given such that the 1to0ormany 1055 forward simulation conditions are satisfied. Under this assumption we 1056 can prove the following three trace reconstruction theorems by mutual 1057 structural induction over the traces given in input between the 1058 $s_1$ and $s_1'$ states. 1059 1060 In particular, the \texttt{status\_simulation\_produce\_tlr} theorem 1061 applied 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 1063 source code that induces a structured trace in the source code, 1064 the compiled code produces a similar structured trace. 1015 1065 1016 1066 \begin{theorem}[\texttt{status\_simulation\_produce\_tlr}] … … 1026 1076 $s_1' \mathcal{R} s_{2_m}$. 1027 1077 \end{theorem} 1078 1079 The theorem states that a \texttt{trace\_label\_return} in the source code 1080 together with a precomputed preamble of silent states 1081 (the \texttt{trace\_any\_any}) in the target code induces a 1082 similar \texttt{trace\_label\_return} trace in the target code which can be 1083 followed by a sequence of silent states. Note that the statement does not 1084 require the produced \texttt{trace\_label\_return} trace to start with the 1085 precomputed preamble, even if this is likely to be the case in concrete 1086 implementations. The preamble in input is necessary for compositionality, e.g. 1087 because the 1to0ormany forward simulation conditions allow in the 1088 case of function calls to execute a preamble of silent instructions just after 1089 the function call. 1090 1028 1091 \begin{theorem}[\texttt{status\_simulation\_produce\_tll}] 1029 1092 For every $s_1,s_1',s_{2_b},s_2$ s.t. … … 1045 1108 \end{itemize} 1046 1109 \end{theorem} 1110 1111 The statement is similar to the previous one: a source 1112 \texttt{trace\_label\_label} and a given target preamble of silent states 1113 in the target code induce a similar \texttt{trace\_label\_label} in the 1114 target code, possibly followed by a sequence of silent moves that become the 1115 preamble for the next \texttt{trace\_label\_label} translation. 1116 1047 1117 \begin{theorem}[\texttt{status\_simulation\_produce\_tal}] 1048 1118 For every $s_1,s_1',s_2$ s.t. … … 1065 1135 \end{itemize} 1066 1136 \end{theorem} 1137 1138 The statement is also similar to the previous ones, but for the lack of 1139 the target code preamble. 1067 1140 1068 1141 \begin{comment}
Note: See TracChangeset
for help on using the changeset viewer.