Changeset 3349 for Papers/itp2013
 Timestamp:
 Jun 13, 2013, 6:10:14 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec2.tex
r3348 r3349 129 129 \def\to{\@ifnextchar[{\new@to}{\oldto}} 130 130 \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 133 135 \makeatother 134 136 … … 1364 1366 1365 1367 \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 instantiated1370 by every pass. The remaining two are derived relations.1368 @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ 1369 Let $S_1$ and $S_2$ be two deterministic labelled transition systems as described 1370 in \autoref{semantics}. We introduce now the four relations $\mathcal{S,C,R,L}\subseteq S_1\times S_2$ 1371 between states of the two systems. The first two are abstract and must be instantiated 1372 by every pass. The remaining two are derived. 1371 1373 1372 1374 The $\S$ relation between states is the classical relation used 1373 in forward simulation proofs. It correlates the data of the stat us1375 in forward simulation proofs. It correlates the data of the states 1374 1376 (e.g. registers, memory, etc.). 1375 1377 1376 The $\C$ relation correlates call states. It allows to track the1377 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 label1380 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 in1382 the target code of every cost emitting statement in the source code.1383 1384 Finally the $\R$ relation is the more complex one.Two states1385 $s_1$ and $s_2$ are $\R$ correlated if every time $s_1$ is the1386 successor sof a call state that is $\C$related to a call state1378 The $\C$ relation correlates states that are about to execute calls. 1379 It 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 1386 Two states 1387 $s_1$ and $s_2$ are $\R$related if every time $s_1$ is the 1388 successor of a call state that is $\C$related to a call state 1387 1389 $s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally: 1388 1390 $$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 callto be1391 We will require all pairs of states that return from related calls to be 1390 1392 $\R$related. This is the fundamental requirement granting 1391 1393 that the target trace is well structured, \emph{i.e.}\ that calls are well 1392 1394 nested and returning where they are supposed to. 1393 1395 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} 1396 We say states in $s_1\in S_1$ and $s_2\in S_2$ are labelrelated 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 1401 there 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 1405 The results that follow all rely on common hypotheses to hold for the 1406 systems $S_1$ and $S_2$ endowed with the relations $\S$ and $\C$. These hypotheses 1407 are depicted by the diagrams in \autoref{fig:forwardsim}. 1407 1408 \begin{figure} 1408 1409 \centering … … 1428 1429 % & 1429 1430 \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 } 1430 1437 \begin{tikzpicture}[baseline={([yshift=.5ex]s2)}] 1431 1438 \matrix [diag] (m) {% … … 1444 1451 \matrix [diag] (m) {% 1445 1452 \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'}; \\ 1447 1454 }; 1448 1455 {[stealth] 1449 1456 \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); 1451 1459 } 1452 1460 \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); … … 1507 1515 \end{figure} 1508 1516 1517 \begin{lemma} 1518 If $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, 1520 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$. 1521 \end{lemma} 1522 \begin{theorem} 1523 If $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 @@@@@@@@@@@@@@@@@@@@@@@ 1509 1528 1510 1529 % \begin{figure} … … 1606 1625 % \end{figure} 1607 1626 1608 \paragraph{1tomany 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'$, and1611 $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or1612 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 either1615 $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 on1620 will be shorthanded as \verb+TAAF+) is an1621 inductive type of structured traces that do not contain function calls or1622 cost emission statements. Differently from a \verb+TAA+, the1623 instruction to be executed in the lookahead state $s_2$ may be a cost emission1624 statement.1625 1626 The intuition of the condition is that one step can be replaced with zero or more steps if it1627 preserves the relation between the data and if the two final statuses are1628 labelled in the same way. Moreover, we must take special care of the empty case1629 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'$ and1633 $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a1634 $\verb+TAA+~s_2~s_a$, and a1635 $\verb+TAAF+~s_b~s_2'$ such that:1636 $s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of1637 the two call states are the same, $s_1 \C s_a$,1638 $s_a\exec s_b$, $s_1' \L s_b$ and1639 $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 a1643 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 new1645 states at the beginning of the function execution must be $\L$related1646 and, finally, the two initial and final states must be $\S$related1647 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'$, a1652 $\verb+TAA+~s_2~s_a$, a1653 $\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$ and1657 $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either1658 $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 a1662 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$related1667 as usual and, moreover, they must exhibit the same labels. Finally, when1668 the suffix is non empty we must take care of not inserting a new1669 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 with1680 [ None ⇒ True1681  Some cl ⇒1682 match cl with1683 [ 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_call1692 *)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_call1702  cl_return ⇒1703 (*1704 st11705 / ↓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 is1715 not empty1716 *)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,L1730  \1731 st2 →taaf→ st2'1732 1733 the taaf can be empty (e.g. tunneling) but we ask it must not be the1734 case when both st1 and st1' are labelled (we would be able to collapse1735 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 1tomany forward simulation conditions1756 are sufficient to trace reconstruction}1757 1758 Let us assume that a relation set is given such that the 1tomany1759 forward simulation conditions are satisfied. Under this assumption we1760 can prove the following three trace reconstruction theorems by mutual1761 structural induction over the traces given in input between the1762 $s_1$ and $s_1'$ states.1763 1764 In particular, the \verb+status_simulation_produce_tlr+ theorem1765 applied to the \verb+main+ function of the program and equal1766 $s_{2_b}$ and $s_2$ states shows that, for every initial state in the1767 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 a1773 $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and1774 $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$ and1776 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'$ and1780 $s_1' \R s_{2_m}$.1781 \end{theorem}1782 1783 The theorem states that a \verb+trace_label_return+ in the source code1784 together with a precomputed preamble of silent states1785 (the \verb+TAA+) in the target code induces a1786 similar \verb+trace_label_return+ in the target code which can be1787 followed by a sequence of silent states. Note that the statement does not1788 require the produced \verb+trace_label_return+ to start with the1789 precomputed preamble, even if this is likely to be the case in concrete1790 implementations. The preamble in input is necessary for compositionality, e.g.1791 because the 1tomany forward simulation conditions allow in the1792 case of function calls to execute a preamble of silent instructions just after1793 the function call.1794 1795 Clearly similar results are also available for the other two types of structured1796 traces (in fact, they are all proved simultaneously by mutual induction).1627 % \paragraph{1tomany 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 1tomany forward simulation conditions 1775 % are sufficient to trace reconstruction} 1776 % 1777 % Let us assume that a relation set is given such that the 1tomany 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 1tomany 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). 1797 1816 % \begin{theorem}[\verb+status_simulation_produce_tll+] 1798 1817 % For every $s_1,s_1',s_{2_b},s_2$ s.t. … … 1893 1912 1894 1913 \section{Conclusions and future works} 1914 AGGIUNGERE DISCORSO SU APPROCCIO ALTERNATIVO: LABEL DOPO OGNI CALL. COMUNQUE 1915 CON TRACCE STRUTTURATE, MA DIVERSAMENTE 1895 1916 \label{conclusions} 1896 1917 The labelling approach is a technique to implement compilers that induce on
Note: See TracChangeset
for help on using the changeset viewer.