Changeset 3349


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

statements

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec2.tex

    r3348 r3349  
    129129\def\to{\@ifnextchar[{\new@to}{\oldto}}
    130130\def\new@to[#1]{\xrightarrow{#1}}
    131 \def\To{\@ifnextchar[{\new@To}{\implies}}
    132 \def\new@To[#1]{\stackrel{#1}{\implies}}
     131\def\st@ck#1[#2]{\stackrel{#2}{#1}}
     132\def\defst@ck#1#2{\def#1{\@ifnextchar[{\st@ck#2}{#2}}}
     133\defst@ck\To\implies
     134\defst@ck\MeasTo\rightsquigarrow
    133135\makeatother
    134136
     
    13641366
    13651367\paragraph{Relation sets.}
    1366 
    1367 We introduce now the four relations $\mathcal{S,C,L,R}$ between abstract
    1368 statuses that are used to correlate the corresponding statues before and
    1369 after a compiler pass. The first two are abstract and must be instantiated
    1370 by every pass. The remaining two are derived relations.
     1368@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
     1369Let $S_1$ and $S_2$ be two deterministic labelled transition systems as described
     1370in \autoref{semantics}. We introduce now the four relations $\mathcal{S,C,R,L}\subseteq S_1\times S_2$
     1371between states of the two systems. The first two are abstract and must be instantiated
     1372by every pass. The remaining two are derived.
    13711373
    13721374The $\S$ relation between states is the classical relation used
    1373 in forward simulation proofs. It correlates the data of the status
     1375in forward simulation proofs. It correlates the data of the states
    13741376(e.g. registers, memory, etc.).
    13751377
    1376 The $\C$ relation correlates call states. It allows to track the
    1377 position in the target code of every call in the source code.
    1378 
    1379 The $\L$ relation simply says that the two states are both label
    1380 emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$.
    1381 It allows to track the position in
    1382 the target code of every cost emitting statement in the source code.
    1383 
    1384 Finally the $\R$ relation is the more complex one. Two states
    1385 $s_1$ and $s_2$ are $\R$ correlated if every time $s_1$ is the
    1386 successors of a call state that is $\C$-related to a call state
     1378The $\C$ relation correlates states that are about to execute calls.
     1379It allows to track the position in the target code of every call in the source code.
     1380
     1381% The $\L$ relation simply says that the two states are both label
     1382% emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$.
     1383% It allows to track the position in
     1384% the target code of every cost emitting statement in the source code.
     1385
     1386Two states
     1387$s_1$ and $s_2$ are $\R$-related if every time $s_1$ is the
     1388successor of a call state that is $\C$-related to a call state
    13871389$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally:
    13881390$$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.$$
    1389 We will require all pairs of states that follow a related call to be
     1391We will require all pairs of states that return from related calls to be
    13901392$\R$-related. This is the fundamental requirement granting
    13911393that the target trace is well structured, \emph{i.e.}\ that calls are well
    13921394nested and returning where they are supposed to.
    13931395
    1394 % \begin{alltt}
    1395 % record status_rel (S1,S2 : abstract_status) : Type[1] := \{
    1396 %   \(\S\): S1 \(\to\) S2 \(\to\) Prop;
    1397 %   \(\C\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\)
    1398 %      (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop \}.
    1399 %
    1400 % definition \(\L\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
    1401 %
    1402 % definition \(\R\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
    1403 %  \(\forall\)s1_pre,s2_pre.
    1404 %   as_after_return s1_pre s1_ret \(\to\) s1_pre \(\R\) s2_pre \(\to\)
    1405 %    as_after_return s2_pre s2_ret.
    1406 % \end{alltt}
     1396We say states in $s_1\in S_1$ and $s_2\in S_2$ are label-related
     1397(marked $s_1\L s_2$) if
     1398\begin{itemize}
     1399\item they both emit the same label $L$;
     1400\item if $L\in \ell(\Functions)$ then
     1401there is a state $s_2'$ such that $s_2\to[L]\to[\tau *]s_2'$ with
     1402 $s_1\S s_2'$, otherwise if $L\notin\ell(\Functions)$ then $s_1\S s_2$.
     1403\end{itemize}
     1404
     1405The results that follow all rely on common hypotheses to hold for the
     1406systems $S_1$ and $S_2$ endowed with the relations $\S$ and $\C$. These hypotheses
     1407are depicted by the diagrams in \autoref{fig:forwardsim}.
    14071408\begin{figure}
    14081409\centering
     
    14281429% &
    14291430\centering
     1431\tikzset{diag/.append style=
     1432         {every node/.append style={is other,
     1433                                    text height=0,text depth=0,text width=0,
     1434                                    text opacity=0}                                                         
     1435         },
     1436         }
    14301437\begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}]
    14311438    \matrix [diag] (m) {%
     
    14441451    \matrix [diag] (m) {%
    14451452         \node (s1) {s_1}; & \node (t1) {s_1'};\\
    1446          \node (s2) {s_2}; & \node (t2) {s_2'}; \\
     1453         \node (s2) {s_2}; & \node (mid) {s_a}; & \node (t2) {s_2'}; \\
    14471454    };
    14481455    {[-stealth]
    14491456    \draw (s1) -- node [above] {$L$} (t1);
    1450     \draw [new] (s2) -- node [above] {$L$} (t2);
     1457    \draw [new] (s2) -- node [above] {$L$} (mid);
     1458    \draw [new] (mid) -- node [above] {$\tau *$} (t2);
    14511459    }
    14521460    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
     
    15071515\end{figure}
    15081516
     1517\begin{lemma}
     1518If $S_1$, $S_2$,$\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
     1519$T_1:s_1\To s_1'$ is a structured fragment not starting with a $\ell(f)$ emission,
     1520and $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$.
     1521\end{lemma}
     1522\begin{theorem}
     1523If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
     1524$M_1:s_1\MeasTo s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that
     1525$s_1\L s_2$, then there is $M_2:s_2\MeasTo s_2'$ with $M_1\approx M_2$.
     1526\end{theorem}
     1527@@@@@@@@@@@@@@@@@@@@@@@
    15091528
    15101529% \begin{figure}
     
    16061625% \end{figure}
    16071626
    1608 \paragraph{1-to-many forward simulation conditions.}
    1609 \begin{condition}[Cases \verb+cl_other+ and \verb+cl_jump+]
    1610  For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
    1611  $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or
    1612  both $s_1\class\verb+cl_other+\}$ and $\ell~s_1'$,
    1613  there exists an $s_2'$ and a $\verb+trace_any_any_free+~s_2~s_2'$ called $taaf$
    1614  such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
    1615 $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \verb+as_costed+.
    1616 \end{condition}
    1617 
    1618 In the above condition depicted in \autoref{subfig:cl_other_jump},
    1619 a $\verb+trace_any_any_free+~s_1~s_2$ (which from now on
    1620 will be shorthanded as \verb+TAAF+) is an
    1621 inductive type of structured traces that do not contain function calls or
    1622 cost emission statements. Differently from a \verb+TAA+, the
    1623 instruction to be executed in the lookahead state $s_2$ may be a cost emission
    1624 statement.
    1625 
    1626 The intuition of the condition is that one step can be replaced with zero or more steps if it
    1627 preserves the relation between the data and if the two final statuses are
    1628 labelled in the same way. Moreover, we must take special care of the empty case
    1629 to avoid collapsing two consecutive states that emit a label, missing one of the two emissions.
    1630 
    1631 \begin{condition}[Case \verb+cl_call+]
    1632  For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and
    1633  $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a
    1634 $\verb+TAA+~s_2~s_a$, and a
    1635 $\verb+TAAF+~s_b~s_2'$ such that:
    1636 $s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of
    1637 the two call states are the same, $s_1 \C s_a$,
    1638 $s_a\exec s_b$, $s_1' \L s_b$ and
    1639 $s_1' \S s_2'$.
    1640 \end{condition}
    1641 
    1642 The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a
    1643 sequence of silent actions before and after the function call itself.
    1644 The old and new call states must be $\C$-related, the old and new
    1645 states at the beginning of the function execution must be $\L$-related
    1646 and, finally, the two initial and final states must be $\S$-related
    1647 as usual.
    1648 
    1649 \begin{condition}[Case \verb+cl_return+]
    1650  For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$,
    1651  $s_1\exec s_1'$ and $s_1 \class \verb+cl_return+$, there exists $s_a, s_b, s_2'$, a
    1652 $\verb+TAA+~s_2~s_a$, a
    1653 $\verb+TAAF+~s_b~s_2'$ called $taaf$ such that:
    1654 $s_a\class\verb+cl_return+$,
    1655 $s_a\exec s_b$,
    1656 $s_1' \R s_b$ and
    1657 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
    1658 $taaf$ is non empty, or $\lnot \ell~s_a$.
    1659 \end{condition}
    1660 
    1661 Similarly to the call condition, to simulate a return we can perform a
    1662 sequence of silent actions before and after the return statement itself,
    1663 as depicted in \autoref{subfig:cl_return}.
    1664 The old and the new statements after the return must be $\R$-related,
    1665 to grant that they returned to corresponding calls.
    1666 The two initial and final states must be $\S$-related
    1667 as usual and, moreover, they must exhibit the same labels. Finally, when
    1668 the suffix is non empty we must take care of not inserting a new
    1669 unmatched cost emission statement just after the return statement.
    1670 
    1671 \begin{comment}
    1672 \begin{verbatim}
    1673 definition status_simulation ≝
    1674   λS1 : abstract_status.
    1675   λS2 : abstract_status.
    1676   λsim_status_rel : status_rel S1 S2.
    1677     ∀st1,st1',st2.as_execute S1 st1 st1' →
    1678     sim_status_rel st1 st2 →
    1679     match as_classify … st1 with
    1680     [ None ⇒ True
    1681     | Some cl ⇒
    1682       match cl with
    1683       [ cl_call ⇒ ∀prf.
    1684         (*
    1685              st1' ------------S----------\
    1686               ↑ \                         \
    1687              st1 \--L--\                   \
    1688               | \       \                   \
    1689               S  \-C-\  st2_after_call →taa→ st2'
    1690               |       \     ↑
    1691              st2 →taa→ st2_pre_call
    1692         *)
    1693         ∃st2_pre_call.
    1694         as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
    1695         call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
    1696         ∃st2_after_call,st2'.
    1697         ∃taa2 : trace_any_any … st2 st2_pre_call.
    1698         ∃taa2' : trace_any_any … st2_after_call st2'.
    1699         as_execute … st2_pre_call st2_after_call ∧
    1700         sim_status_rel st1' st2' ∧
    1701         label_rel … st1' st2_after_call
    1702       | cl_return ⇒
    1703         (*
    1704              st1
    1705             / ↓
    1706            | st1'----------S,L------------\
    1707            S   \                           \
    1708             \   \-----R-------\            |     
    1709              \                 |           |
    1710              st2 →taa→ st2_ret |           |
    1711                           ↓   /            |
    1712                      st2_after_ret →taaf→ st2'
    1713 
    1714            we also ask that st2_after_ret be not labelled if the taaf tail is
    1715            not empty
    1716         *)
    1717         ∃st2_ret,st2_after_ret,st2'.
    1718         ∃taa2 : trace_any_any … st2 st2_ret.
    1719         ∃taa2' : trace_any_any_free … st2_after_ret st2'.
    1720         (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
    1721         as_classifier … st2_ret cl_return ∧
    1722         as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
    1723         ret_rel … sim_status_rel st1' st2_after_ret ∧
    1724         label_rel … st1' st2'
    1725       | cl_other ⇒
    1726           (*         
    1727           st1 → st1'
    1728             |      \
    1729             S      S,L
    1730             |        \
    1731            st2 →taaf→ st2'
    1732            
    1733            the taaf can be empty (e.g. tunneling) but we ask it must not be the
    1734            case when both st1 and st1' are labelled (we would be able to collapse
    1735            labels otherwise)
    1736          *)
    1737         ∃st2'.
    1738         ∃taa2 : trace_any_any_free … st2 st2'.
    1739         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    1740         sim_status_rel st1' st2' ∧
    1741         label_rel … st1' st2'
    1742       | cl_jump ⇒
    1743         (* just like cl_other, but with a hypothesis more *)
    1744         as_costed … st1' →
    1745         ∃st2'.
    1746         ∃taa2 : trace_any_any_free … st2 st2'.
    1747         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
    1748         sim_status_rel st1' st2' ∧
    1749         label_rel … st1' st2'
    1750       ]
    1751     ].
    1752 \end{verbatim}
    1753 \end{comment}
    1754 
    1755 \paragraph{Main result: the 1-to-many forward simulation conditions
    1756 are sufficient to trace reconstruction}
    1757 
    1758 Let us assume that a relation set is given such that the 1-to-many
    1759 forward simulation conditions are satisfied. Under this assumption we
    1760 can prove the following three trace reconstruction theorems by mutual
    1761 structural induction over the traces given in input between the
    1762 $s_1$ and $s_1'$ states.
    1763 
    1764 In particular, the \verb+status_simulation_produce_tlr+ theorem
    1765 applied to the \verb+main+ function of the program and equal
    1766 $s_{2_b}$ and $s_2$ states shows that, for every initial state in the
    1767 source code that induces a structured trace in the source code,
    1768 the compiled code produces a similar structured trace.
    1769 
    1770 \begin{theorem}[\verb+status_simulation_produce_tlr+]
    1771 For every $s_1,s_1',s_{2_b},s_2$ s.t.
    1772 there is a $\verb+TLR+~s_1~s_1'$ called $tlr_1$ and a
    1773 $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
    1774 $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
    1775 there is a $\verb+TLR+~s_{2_b}~s_{2_m}$ called $tlr_2$ and
    1776 there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$
    1777 s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$,
    1778 and $tlr_1\approx tlr_2$
    1779 and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
    1780 $s_1' \R s_{2_m}$.
    1781 \end{theorem}
    1782 
    1783 The theorem states that a \verb+trace_label_return+ in the source code
    1784 together with a precomputed preamble of silent states
    1785 (the \verb+TAA+) in the target code induces a
    1786 similar \verb+trace_label_return+ in the target code which can be
    1787 followed by a sequence of silent states. Note that the statement does not
    1788 require the produced \verb+trace_label_return+ to start with the
    1789 precomputed preamble, even if this is likely to be the case in concrete
    1790 implementations. The preamble in input is necessary for compositionality, e.g.
    1791 because the 1-to-many forward simulation conditions allow in the
    1792 case of function calls to execute a preamble of silent instructions just after
    1793 the function call.
    1794 
    1795 Clearly similar results are also available for the other two types of structured
    1796 traces (in fact, they are all proved simultaneously by mutual induction).
     1627% \paragraph{1-to-many forward simulation conditions.}
     1628% \begin{condition}[Cases \verb+cl_other+ and \verb+cl_jump+]
     1629% For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
     1630% $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or
     1631% both $s_1\class\verb+cl_other+\}$ and $\ell~s_1'$,
     1632% there exists an $s_2'$ and a $\verb+trace_any_any_free+~s_2~s_2'$ called $taaf$
     1633% such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
     1634% $taaf$ is non empty, or one among $s_1$ and $s_1'$ is \verb+as_costed+.
     1635% \end{condition}
     1636%
     1637% In the above condition depicted in \autoref{subfig:cl_other_jump},
     1638% a $\verb+trace_any_any_free+~s_1~s_2$ (which from now on
     1639% will be shorthanded as \verb+TAAF+) is an
     1640% inductive type of structured traces that do not contain function calls or
     1641% cost emission statements. Differently from a \verb+TAA+, the
     1642% instruction to be executed in the lookahead state $s_2$ may be a cost emission
     1643% statement.
     1644%
     1645% The intuition of the condition is that one step can be replaced with zero or more steps if it
     1646% preserves the relation between the data and if the two final statuses are
     1647% labelled in the same way. Moreover, we must take special care of the empty case
     1648% to avoid collapsing two consecutive states that emit a label, missing one of the two emissions.
     1649%
     1650% \begin{condition}[Case \verb+cl_call+]
     1651% For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and
     1652% $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a
     1653% $\verb+TAA+~s_2~s_a$, and a
     1654% $\verb+TAAF+~s_b~s_2'$ such that:
     1655% $s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of
     1656% the two call states are the same, $s_1 \C s_a$,
     1657% $s_a\exec s_b$, $s_1' \L s_b$ and
     1658% $s_1' \S s_2'$.
     1659% \end{condition}
     1660%
     1661% The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a
     1662% sequence of silent actions before and after the function call itself.
     1663% The old and new call states must be $\C$-related, the old and new
     1664% states at the beginning of the function execution must be $\L$-related
     1665% and, finally, the two initial and final states must be $\S$-related
     1666% as usual.
     1667%
     1668% \begin{condition}[Case \verb+cl_return+]
     1669% For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$,
     1670% $s_1\exec s_1'$ and $s_1 \class \verb+cl_return+$, there exists $s_a, s_b, s_2'$, a
     1671% $\verb+TAA+~s_2~s_a$, a
     1672% $\verb+TAAF+~s_b~s_2'$ called $taaf$ such that:
     1673% $s_a\class\verb+cl_return+$,
     1674% $s_a\exec s_b$,
     1675% $s_1' \R s_b$ and
     1676% $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
     1677% $taaf$ is non empty, or $\lnot \ell~s_a$.
     1678% \end{condition}
     1679%
     1680% Similarly to the call condition, to simulate a return we can perform a
     1681% sequence of silent actions before and after the return statement itself,
     1682% as depicted in \autoref{subfig:cl_return}.
     1683% The old and the new statements after the return must be $\R$-related,
     1684% to grant that they returned to corresponding calls.
     1685% The two initial and final states must be $\S$-related
     1686% as usual and, moreover, they must exhibit the same labels. Finally, when
     1687% the suffix is non empty we must take care of not inserting a new
     1688% unmatched cost emission statement just after the return statement.
     1689%
     1690% \begin{comment}
     1691% \begin{verbatim}
     1692% definition status_simulation ≝
     1693%   λS1 : abstract_status.
     1694%   λS2 : abstract_status.
     1695%   λsim_status_rel : status_rel S1 S2.
     1696%     ∀st1,st1',st2.as_execute S1 st1 st1' →
     1697%     sim_status_rel st1 st2 →
     1698%     match as_classify … st1 with
     1699%     [ None ⇒ True
     1700%     | Some cl ⇒
     1701%       match cl with
     1702%       [ cl_call ⇒ ∀prf.
     1703%         (*
     1704%              st1' ------------S----------\
     1705%               ↑ \                         \
     1706%              st1 \--L--\                   \
     1707%               | \       \                   \
     1708%               S  \-C-\  st2_after_call →taa→ st2'
     1709%               |       \     ↑
     1710%              st2 →taa→ st2_pre_call
     1711%         *)
     1712%         ∃st2_pre_call.
     1713%         as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
     1714%         call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
     1715%         ∃st2_after_call,st2'.
     1716%         ∃taa2 : trace_any_any … st2 st2_pre_call.
     1717%         ∃taa2' : trace_any_any … st2_after_call st2'.
     1718%         as_execute … st2_pre_call st2_after_call ∧
     1719%         sim_status_rel st1' st2' ∧
     1720%         label_rel … st1' st2_after_call
     1721%       | cl_return ⇒
     1722%         (*
     1723%              st1
     1724%             / ↓
     1725%            | st1'----------S,L------------\
     1726%            S   \                           \
     1727%             \   \-----R-------\            |     
     1728%              \                 |           |
     1729%              st2 →taa→ st2_ret |           |
     1730%                           ↓   /            |
     1731%                      st2_after_ret →taaf→ st2'
     1732%
     1733%            we also ask that st2_after_ret be not labelled if the taaf tail is
     1734%            not empty
     1735%         *)
     1736%         ∃st2_ret,st2_after_ret,st2'.
     1737%         ∃taa2 : trace_any_any … st2 st2_ret.
     1738%         ∃taa2' : trace_any_any_free … st2_after_ret st2'.
     1739%         (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
     1740%         as_classifier … st2_ret cl_return ∧
     1741%         as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
     1742%         ret_rel … sim_status_rel st1' st2_after_ret ∧
     1743%         label_rel … st1' st2'
     1744%       | cl_other ⇒
     1745%           (*         
     1746%           st1 → st1'
     1747%             |      \
     1748%             S      S,L
     1749%             |        \
     1750%            st2 →taaf→ st2'
     1751%            
     1752%            the taaf can be empty (e.g. tunneling) but we ask it must not be the
     1753%            case when both st1 and st1' are labelled (we would be able to collapse
     1754%            labels otherwise)
     1755%          *)
     1756%         ∃st2'.
     1757%         ∃taa2 : trace_any_any_free … st2 st2'.
     1758%         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     1759%         sim_status_rel st1' st2' ∧
     1760%         label_rel … st1' st2'
     1761%       | cl_jump ⇒
     1762%         (* just like cl_other, but with a hypothesis more *)
     1763%         as_costed … st1' →
     1764%         ∃st2'.
     1765%         ∃taa2 : trace_any_any_free … st2 st2'.
     1766%         (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
     1767%         sim_status_rel st1' st2' ∧
     1768%         label_rel … st1' st2'
     1769%       ]
     1770%     ].
     1771% \end{verbatim}
     1772% \end{comment}
     1773
     1774% \paragraph{Main result: the 1-to-many forward simulation conditions
     1775% are sufficient to trace reconstruction}
     1776%
     1777% Let us assume that a relation set is given such that the 1-to-many
     1778% forward simulation conditions are satisfied. Under this assumption we
     1779% can prove the following three trace reconstruction theorems by mutual
     1780% structural induction over the traces given in input between the
     1781% $s_1$ and $s_1'$ states.
     1782%
     1783% In particular, the \verb+status_simulation_produce_tlr+ theorem
     1784% applied to the \verb+main+ function of the program and equal
     1785% $s_{2_b}$ and $s_2$ states shows that, for every initial state in the
     1786% source code that induces a structured trace in the source code,
     1787% the compiled code produces a similar structured trace.
     1788%
     1789% \begin{theorem}[\verb+status_simulation_produce_tlr+]
     1790% For every $s_1,s_1',s_{2_b},s_2$ s.t.
     1791% there is a $\verb+TLR+~s_1~s_1'$ called $tlr_1$ and a
     1792% $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
     1793% $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
     1794% there is a $\verb+TLR+~s_{2_b}~s_{2_m}$ called $tlr_2$ and
     1795% there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$
     1796% s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$,
     1797% and $tlr_1\approx tlr_2$
     1798% and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
     1799% $s_1' \R s_{2_m}$.
     1800% \end{theorem}
     1801%
     1802% The theorem states that a \verb+trace_label_return+ in the source code
     1803% together with a precomputed preamble of silent states
     1804% (the \verb+TAA+) in the target code induces a
     1805% similar \verb+trace_label_return+ in the target code which can be
     1806% followed by a sequence of silent states. Note that the statement does not
     1807% require the produced \verb+trace_label_return+ to start with the
     1808% precomputed preamble, even if this is likely to be the case in concrete
     1809% implementations. The preamble in input is necessary for compositionality, e.g.
     1810% because the 1-to-many forward simulation conditions allow in the
     1811% case of function calls to execute a preamble of silent instructions just after
     1812% the function call.
     1813%
     1814% Clearly similar results are also available for the other two types of structured
     1815% traces (in fact, they are all proved simultaneously by mutual induction).
    17971816% \begin{theorem}[\verb+status_simulation_produce_tll+]
    17981817% For every $s_1,s_1',s_{2_b},s_2$ s.t.
     
    18931912
    18941913\section{Conclusions and future works}
     1914AGGIUNGERE DISCORSO SU APPROCCIO ALTERNATIVO: LABEL DOPO OGNI CALL. COMUNQUE
     1915CON TRACCE STRUTTURATE, MA DIVERSAMENTE
    18951916\label{conclusions}
    18961917The labelling approach is a technique to implement compilers that induce on
Note: See TracChangeset for help on using the changeset viewer.