Changeset 3349 for Papers

Ignore:
Timestamp:
Jun 13, 2013, 6:10:14 PM (6 years ago)
Message:

statements

File:
1 edited

Legend:

Unmodified
 r3348 \def\to{\@ifnextchar[{\new@to}{\oldto}} \def\new@to[#1]{\xrightarrow{#1}} \def\To{\@ifnextchar[{\new@To}{\implies}} \def\new@To[#1]{\stackrel{#1}{\implies}} \def\st@ck#1[#2]{\stackrel{#2}{#1}} \def\defst@ck#1#2{\def#1{\@ifnextchar[{\st@ck#2}{#2}}} \defst@ck\To\implies \defst@ck\MeasTo\rightsquigarrow \makeatother \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. @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Let $S_1$ and $S_2$ be two deterministic labelled transition systems as described in \autoref{semantics}. We introduce now the four relations $\mathcal{S,C,R,L}\subseteq S_1\times S_2$ between states of the two systems. The first two are abstract and must be instantiated by every pass. The remaining two are derived. The $\S$ relation between states is the classical relation used in forward simulation proofs. It correlates the data of the status in forward simulation proofs. It correlates the data of the states (e.g. registers, memory, etc.). The $\C$ relation correlates call states. It allows to track the position in the target code of every call in the source code. The $\L$ relation simply says that the two states are both label emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$. It allows to track the position in the target code of every cost emitting statement in the source code. Finally the $\R$ relation is the more complex one. Two states $s_1$ and $s_2$ are $\R$ correlated if every time $s_1$ is the successors of a call state that is $\C$-related to a call state The $\C$ relation correlates states that are about to execute calls. It allows to track the position in the target code of every call in the source code. % The $\L$ relation simply says that the two states are both label % emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$. % It allows to track the position in % the target code of every cost emitting statement in the source code. Two states $s_1$ and $s_2$ are $\R$-related if every time $s_1$ is the successor of a call state that is $\C$-related to a call state $s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally: $$s_1\R s_2 \iffdef \forall s_1',s_2'.s_1'\C s_2' \to s_1'\ar s_1 \to s_2' \ar s_2.$$ We will require all pairs of states that follow a related call to be We will require all pairs of states that return from related calls to be $\R$-related. This is the fundamental requirement granting that the target trace is well structured, \emph{i.e.}\ that calls are well nested and returning where they are supposed to. % \begin{alltt} % record status_rel (S1,S2 : abstract_status) : Type[1] := \{ %   $$\S$$: S1 $$\to$$ S2 $$\to$$ Prop; %   $$\C$$: ($$\Sigma$$s.as_classifier S1 s cl_call) $$\to$$ %      ($$\Sigma$$s.as_classifier S2 s cl_call) $$\to$$ Prop \}. % % definition $$\L$$ S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2. % % definition $$\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 $$\R$$ s2_pre $$\to$$ %    as_after_return s2_pre s2_ret. % \end{alltt} We say states in $s_1\in S_1$ and $s_2\in S_2$ are label-related (marked $s_1\L s_2$) if \begin{itemize} \item they both emit the same label $L$; \item if $L\in \ell(\Functions)$ then there is a state $s_2'$ such that $s_2\to[L]\to[\tau *]s_2'$ with $s_1\S s_2'$, otherwise if $L\notin\ell(\Functions)$ then $s_1\S s_2$. \end{itemize} The results that follow all rely on common hypotheses to hold for the systems $S_1$ and $S_2$ endowed with the relations $\S$ and $\C$. These hypotheses are depicted by the diagrams in \autoref{fig:forwardsim}. \begin{figure} \centering % & \centering \tikzset{diag/.append style= {every node/.append style={is other, text height=0,text depth=0,text width=0, text opacity=0} }, } \begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}] \matrix [diag] (m) {% \matrix [diag] (m) {% \node (s1) {s_1}; & \node (t1) {s_1'};\\ \node (s2) {s_2}; & \node (t2) {s_2'}; \\ \node (s2) {s_2}; & \node (mid) {s_a}; & \node (t2) {s_2'}; \\ }; {[-stealth] \draw (s1) -- node [above] {$L$} (t1); \draw [new] (s2) -- node [above] {$L$} (t2); \draw [new] (s2) -- node [above] {$L$} (mid); \draw [new] (mid) -- node [above] {$\tau *$} (t2); } \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); \end{figure} \begin{lemma} If $S_1$, $S_2$,$\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim}, $T_1:s_1\To s_1'$ is a structured fragment not starting with a $\ell(f)$ emission, and $s_1\S s_2$, then there is $T_2:s_2\To s_2'$ with $T\approx T'$ and $s_1'\S s_2$. \end{lemma} \begin{theorem} If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim}, $M_1:s_1\MeasTo s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that $s_1\L s_2$, then there is $M_2:s_2\MeasTo s_2'$ with $M_1\approx M_2$. \end{theorem} @@@@@@@@@@@@@@@@@@@@@@@ % \begin{figure} % \end{figure} \paragraph{1-to-many forward simulation conditions.} \begin{condition}[Cases \verb+cl_other+ and \verb+cl_jump+] For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or both $s_1\class\verb+cl_other+\}$ and $\ell~s_1'$, there exists an $s_2'$ and a $\verb+trace_any_any_free+~s_2~s_2'$ called $taaf$ such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \verb+as_costed+. \end{condition} In the above condition depicted in \autoref{subfig:cl_other_jump}, a $\verb+trace_any_any_free+~s_1~s_2$ (which from now on will be shorthanded as \verb+TAAF+) is an inductive type of structured traces that do not contain function calls or cost emission statements. Differently from a \verb+TAA+, the instruction to be executed in the lookahead state $s_2$ may be a cost emission statement. The intuition of the condition is that one step can be replaced with zero or more steps if it preserves the relation between the data and if the two final statuses are labelled in the same way. Moreover, we must take special care of the empty case to avoid collapsing two consecutive states that emit a label, missing one of the two emissions. \begin{condition}[Case \verb+cl_call+] For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a $\verb+TAA+~s_2~s_a$, and a $\verb+TAAF+~s_b~s_2'$ such that: $s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of the two call states are the same, $s_1 \C s_a$, $s_a\exec s_b$, $s_1' \L s_b$ and $s_1' \S s_2'$. \end{condition} The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a sequence of silent actions before and after the function call itself. The old and new call states must be $\C$-related, the old and new states at the beginning of the function execution must be $\L$-related and, finally, the two initial and final states must be $\S$-related as usual. \begin{condition}[Case \verb+cl_return+] For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$, $s_1\exec s_1'$ and $s_1 \class \verb+cl_return+$, there exists $s_a, s_b, s_2'$, a $\verb+TAA+~s_2~s_a$, a $\verb+TAAF+~s_b~s_2'$ called $taaf$ such that: $s_a\class\verb+cl_return+$, $s_a\exec s_b$, $s_1' \R s_b$ and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either $taaf$ is non empty, or $\lnot \ell~s_a$. \end{condition} Similarly to the call condition, to simulate a return we can perform a sequence of silent actions before and after the return statement itself, as depicted in \autoref{subfig:cl_return}. The old and the new statements after the return must be $\R$-related, to grant that they returned to corresponding calls. The two initial and final states must be $\S$-related as usual and, moreover, they must exhibit the same labels. Finally, when the suffix is non empty we must take care of not inserting a new unmatched cost emission statement just after the return statement. \begin{comment} \begin{verbatim} definition status_simulation ≝ λS1 : abstract_status. λS2 : abstract_status. λsim_status_rel : status_rel S1 S2. ∀st1,st1',st2.as_execute S1 st1 st1' → sim_status_rel st1 st2 → match as_classify … st1 with [ None ⇒ True | Some cl ⇒ match cl with [ cl_call ⇒ ∀prf. (* st1' ------------S----------\ ↑ \                         \ st1 \--L--\                   \ | \       \                   \ S  \-C-\  st2_after_call →taa→ st2' |       \     ↑ st2 →taa→ st2_pre_call *) ∃st2_pre_call. as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ ∃st2_after_call,st2'. ∃taa2 : trace_any_any … st2 st2_pre_call. ∃taa2' : trace_any_any … st2_after_call st2'. as_execute … st2_pre_call st2_after_call ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2_after_call | cl_return ⇒ (* st1 / ↓ | st1'----------S,L------------\ S   \                           \ \   \-----R-------\            | \                 |           | st2 →taa→ st2_ret |           | ↓   /            | st2_after_ret →taaf→ st2' we also ask that st2_after_ret be not labelled if the taaf tail is not empty *) ∃st2_ret,st2_after_ret,st2'. ∃taa2 : trace_any_any … st2 st2_ret. ∃taa2' : trace_any_any_free … st2_after_ret st2'. (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ as_classifier … st2_ret cl_return ∧ as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ ret_rel … sim_status_rel st1' st2_after_ret ∧ label_rel … st1' st2' | cl_other ⇒ (* st1 → st1' |      \ S      S,L |        \ st2 →taaf→ st2' the taaf can be empty (e.g. tunneling) but we ask it must not be the case when both st1 and st1' are labelled (we would be able to collapse labels otherwise) *) ∃st2'. ∃taa2 : trace_any_any_free … st2 st2'. (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2' | cl_jump ⇒ (* just like cl_other, but with a hypothesis more *) as_costed … st1' → ∃st2'. ∃taa2 : trace_any_any_free … st2 st2'. (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ sim_status_rel st1' st2' ∧ label_rel … st1' st2' ] ]. \end{verbatim} \end{comment} \paragraph{Main result: the 1-to-many forward simulation conditions are sufficient to trace reconstruction} Let us assume that a relation set is given such that the 1-to-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 \verb+status_simulation_produce_tlr+ theorem applied to the \verb+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}[\verb+status_simulation_produce_tlr+] For every $s_1,s_1',s_{2_b},s_2$ s.t. there is a $\verb+TLR+~s_1~s_1'$ called $tlr_1$ and a $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t. there is a $\verb+TLR+~s_{2_b}~s_{2_m}$ called $tlr_2$ and there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$ s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$, and $tlr_1\approx tlr_2$ and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and $s_1' \R s_{2_m}$. \end{theorem} The theorem states that a \verb+trace_label_return+ in the source code together with a precomputed preamble of silent states (the \verb+TAA+) in the target code induces a similar \verb+trace_label_return+ in the target code which can be followed by a sequence of silent states. Note that the statement does not require the produced \verb+trace_label_return+ 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-many forward simulation conditions allow in the case of function calls to execute a preamble of silent instructions just after the function call. Clearly similar results are also available for the other two types of structured traces (in fact, they are all proved simultaneously by mutual induction). % \paragraph{1-to-many forward simulation conditions.} % \begin{condition}[Cases \verb+cl_other+ and \verb+cl_jump+] % For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and % $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or % both $s_1\class\verb+cl_other+\}$ and $\ell~s_1'$, % there exists an $s_2'$ and a $\verb+trace_any_any_free+~s_2~s_2'$ called $taaf$ % such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either % $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \verb+as_costed+. % \end{condition} % % In the above condition depicted in \autoref{subfig:cl_other_jump}, % a $\verb+trace_any_any_free+~s_1~s_2$ (which from now on % will be shorthanded as \verb+TAAF+) is an % inductive type of structured traces that do not contain function calls or % cost emission statements. Differently from a \verb+TAA+, the % instruction to be executed in the lookahead state $s_2$ may be a cost emission % statement. % % The intuition of the condition is that one step can be replaced with zero or more steps if it % preserves the relation between the data and if the two final statuses are % labelled in the same way. Moreover, we must take special care of the empty case % to avoid collapsing two consecutive states that emit a label, missing one of the two emissions. % % \begin{condition}[Case \verb+cl_call+] % For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and % $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a % $\verb+TAA+~s_2~s_a$, and a % $\verb+TAAF+~s_b~s_2'$ such that: % $s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of % the two call states are the same, $s_1 \C s_a$, % $s_a\exec s_b$, $s_1' \L s_b$ and % $s_1' \S s_2'$. % \end{condition} % % The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a % sequence of silent actions before and after the function call itself. % The old and new call states must be $\C$-related, the old and new % states at the beginning of the function execution must be $\L$-related % and, finally, the two initial and final states must be $\S$-related % as usual. % % \begin{condition}[Case \verb+cl_return+] % For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$, % $s_1\exec s_1'$ and $s_1 \class \verb+cl_return+$, there exists $s_a, s_b, s_2'$, a % $\verb+TAA+~s_2~s_a$, a % $\verb+TAAF+~s_b~s_2'$ called $taaf$ such that: % $s_a\class\verb+cl_return+$, % $s_a\exec s_b$, % $s_1' \R s_b$ and % $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either % $taaf$ is non empty, or $\lnot \ell~s_a$. % \end{condition} % % Similarly to the call condition, to simulate a return we can perform a % sequence of silent actions before and after the return statement itself, % as depicted in \autoref{subfig:cl_return}. % The old and the new statements after the return must be $\R$-related, % to grant that they returned to corresponding calls. % The two initial and final states must be $\S$-related % as usual and, moreover, they must exhibit the same labels. Finally, when % the suffix is non empty we must take care of not inserting a new % unmatched cost emission statement just after the return statement. % % \begin{comment} % \begin{verbatim} % definition status_simulation ≝ %   λS1 : abstract_status. %   λS2 : abstract_status. %   λsim_status_rel : status_rel S1 S2. %     ∀st1,st1',st2.as_execute S1 st1 st1' → %     sim_status_rel st1 st2 → %     match as_classify … st1 with %     [ None ⇒ True %     | Some cl ⇒ %       match cl with %       [ cl_call ⇒ ∀prf. %         (* %              st1' ------------S----------\ %               ↑ \                         \ %              st1 \--L--\                   \ %               | \       \                   \ %               S  \-C-\  st2_after_call →taa→ st2' %               |       \     ↑ %              st2 →taa→ st2_pre_call %         *) %         ∃st2_pre_call. %         as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ %         call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ %         ∃st2_after_call,st2'. %         ∃taa2 : trace_any_any … st2 st2_pre_call. %         ∃taa2' : trace_any_any … st2_after_call st2'. %         as_execute … st2_pre_call st2_after_call ∧ %         sim_status_rel st1' st2' ∧ %         label_rel … st1' st2_after_call %       | cl_return ⇒ %         (* %              st1 %             / ↓ %            | st1'----------S,L------------\ %            S   \                           \ %             \   \-----R-------\            | %              \                 |           | %              st2 →taa→ st2_ret |           | %                           ↓   /            | %                      st2_after_ret →taaf→ st2' % %            we also ask that st2_after_ret be not labelled if the taaf tail is %            not empty %         *) %         ∃st2_ret,st2_after_ret,st2'. %         ∃taa2 : trace_any_any … st2 st2_ret. %         ∃taa2' : trace_any_any_free … st2_after_ret st2'. %         (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ %         as_classifier … st2_ret cl_return ∧ %         as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ %         ret_rel … sim_status_rel st1' st2_after_ret ∧ %         label_rel … st1' st2' %       | cl_other ⇒ %           (* %           st1 → st1' %             |      \ %             S      S,L %             |        \ %            st2 →taaf→ st2' % %            the taaf can be empty (e.g. tunneling) but we ask it must not be the %            case when both st1 and st1' are labelled (we would be able to collapse %            labels otherwise) %          *) %         ∃st2'. %         ∃taa2 : trace_any_any_free … st2 st2'. %         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ %         sim_status_rel st1' st2' ∧ %         label_rel … st1' st2' %       | cl_jump ⇒ %         (* just like cl_other, but with a hypothesis more *) %         as_costed … st1' → %         ∃st2'. %         ∃taa2 : trace_any_any_free … st2 st2'. %         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ %         sim_status_rel st1' st2' ∧ %         label_rel … st1' st2' %       ] %     ]. % \end{verbatim} % \end{comment} % \paragraph{Main result: the 1-to-many forward simulation conditions % are sufficient to trace reconstruction} % % Let us assume that a relation set is given such that the 1-to-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 \verb+status_simulation_produce_tlr+ theorem % applied to the \verb+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}[\verb+status_simulation_produce_tlr+] % For every $s_1,s_1',s_{2_b},s_2$ s.t. % there is a $\verb+TLR+~s_1~s_1'$ called $tlr_1$ and a % $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and % $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t. % there is a $\verb+TLR+~s_{2_b}~s_{2_m}$ called $tlr_2$ and % there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$ % s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$, % and $tlr_1\approx tlr_2$ % and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and % $s_1' \R s_{2_m}$. % \end{theorem} % % The theorem states that a \verb+trace_label_return+ in the source code % together with a precomputed preamble of silent states % (the \verb+TAA+) in the target code induces a % similar \verb+trace_label_return+ in the target code which can be % followed by a sequence of silent states. Note that the statement does not % require the produced \verb+trace_label_return+ 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-many forward simulation conditions allow in the % case of function calls to execute a preamble of silent instructions just after % the function call. % % Clearly similar results are also available for the other two types of structured % traces (in fact, they are all proved simultaneously by mutual induction). % \begin{theorem}[\verb+status_simulation_produce_tll+] % For every $s_1,s_1',s_{2_b},s_2$ s.t. \section{Conclusions and future works} AGGIUNGERE DISCORSO SU APPROCCIO ALTERNATIVO: LABEL DOPO OGNI CALL. COMUNQUE CON TRACCE STRUTTURATE, MA DIVERSAMENTE \label{conclusions} The labelling approach is a technique to implement compilers that induce on