Changeset 3348


Ignore:
Timestamp:
Jun 13, 2013, 1:22:56 PM (4 years ago)
Author:
tranquil
Message:

ipotesi della forward simulation

File:
1 edited

Legend:

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

    r3347 r3348  
    9292         diag/.style={row sep={11mm,between origins},
    9393                      column sep={11mm,between origins},
    94                       every node/.style={draw, is other}},
     94                      every node/.style={execute at begin node=$, execute at end node=$},
     95%                       every node/.style={draw, is other},
     96                      },
    9597         small vgap/.style={row sep={7mm,between origins}},
    96          small gap/.style={row sep={7mm,between origins},column sep={7mm,between origins}},
     98         small hgap/.style={column sep={7mm,between origins}},
     99         small gap/.style={small vgap, small hgap},
    97100         % for article, maybe temporary
    98101         is jump/.style=is other,
     
    695698where $\Functions$ is the set of names of functions that can occur in the
    696699program, $\Labels$ is a set of labels disjoint from $\Functions$
    697 and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$.
     700and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$. Moreover there
     701is an injective function $\ell : \Functions \to \Labels$ that tells the
     702starting label of the body of each function, and $\ell(\Functions)\subseteq \Labels$
     703denotes the image of this function.
    698704The transition function is defined as $s_1 \to[o] s_2$ if
    699705$s_1$ moves to $s_2$ according to the SOS; moreover $o = f \in \Functions$ if
     
    715721 \item For every $i$, if $s_i \to[f] s_{i+1}$ then there is a
    716722   label $L$ and a $k\ge i+2$ such that
    717     $s_{i+1} \to[L] s_{i+2} \To s_k \to[RET] s_{k+1}$, with
     723    $s_{i+1} \to[\ell(f)] s_{i+2} \To s_k \to[RET] s_{k+1}$, with
    718724    $s_i \ar s_{k+1}$.
    719    In other words, $s_{i+1}$ must start execution with an \verb+EMIT $L$+
     725   In other words, $s_{i+1}$ must start execution with \verb+EMIT $\ell(f)$+
    720726   and then continue with a structured fragment returning control
    721727   to the instruction immediately following the call.
     
    723729   with a label emission statement, and every function
    724730   call must converge yielding back control just after it.
     731 \item For every $i$ and $f$, if $s_{i+1}\to[\ell(f)]s_{i+2}$ then
     732   $s_i\to[f]s_{i+1}$. This is a technical condition needed to ensure that
     733   labels associated with functions always follow a call.
    725734 \item The number of $RET$'s in the fragment is equal to the number of
    726735   calls, i.e.\ the number of observables in $\Functions$. This, together with
     
    732741   live code must start with a label emission.
    733742\end{enumerate}
    734 
    735 Let $T = s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ be an
     743One might wonder why $f$ and $\ell(f)$, that aways appear in this order, are not
     744collapsed into a single observable. This would indeed simplify some aspects of
     745the formalisation, but has the problem of misassagning the cost of calls, which would
     746fall under the associated label. As different call instructions with different costs
     747are possible, this is not acceptable.
     748
     749Let $T = s_0 \to[o_0] s_1 \ldots \to[o_n] s_{n+1}$ be an
    736750execution fragment. The \emph{weak trace} $|T|$ associated to $T$ is the
    737751subsequence $o_{i_0} \ldots o_{i_m}$ of $o_0 \ldots o_n$ obtained dropping
     
    739753
    740754Let $k$ be a cost model that maps observables actions to any commutative cost
    741 monoid (e.g. natural numbers). We extend the domain of $k$ to weak traces
    742 by posing $k(\mathcal{T}) = \Sigma_{o \in \mathcal{T}} k(o)$.
     755monoid (e.g. natural numbers). We extend the domain of $k$ to fragments
     756by posing $k(T) = \Sigma_{o \in |T|} k(o)$.
    743757
    744758The labelling approach is based on the idea that the execution cost of
     
    13911405%    as_after_return s2_pre s2_ret.
    13921406% \end{alltt}
    1393 
    13941407\begin{figure}
    13951408\centering
    1396 \begin{tabular}{@{}c@{}c@{}c@{}}
    13971409% \begin{subfigure}{.475\linewidth}
    13981410% \centering
     
    14151427% \end{subfigure}
    14161428% &
    1417 \begin{subfigure}{.25\linewidth}
    14181429\centering
    1419 \begin{tikzpicture}[every join/.style={ar}, join all, thick,
    1420                             every label/.style=overlay, node distance=10mm]
     1430\begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}]
    14211431    \matrix [diag] (m) {%
    1422          \node (s1) {}; & \node (t1) {};\\
    1423          \node (s2) {}; & \node (t2) {}; \\
     1432         \node (s1) {s_1}; & \node (t1) {s_1'};\\
     1433         \node (s2) {s_2}; & \node (t2) {s_2'}; \\
    14241434    };
    14251435    {[-stealth]
    1426     \draw (s1) -- (t1);
    1427     \draw [new] (s2) -- node [above] {$*$} (t2);
     1436    \draw (s1) -- node [above] {$\tau$} (t1);
     1437    \draw [new] (s2) -- node [above] {$\tau *$} (t2);
    14281438    }
    14291439    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
    1430     \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2);
     1440    \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2);
    14311441\end{tikzpicture}
    1432 \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.}
    1433 \label{subfig:cl_other_jump}
    1434 \end{subfigure}
    1435 &
    1436 \begin{subfigure}{.375\linewidth}
    1437 \centering
    1438 \begin{tikzpicture}[every join/.style={ar}, join all, thick,
    1439                             every label/.style=overlay, node distance=10mm]
    1440     \matrix [diag, small gap] (m) {%
    1441          &\node (t1) {}; \\
    1442          \node (s1) [is call] {}; \\
    1443          && \node (l) {}; & \node (t2) {};\\
    1444          \node (s2) {}; & \node (c) [is call] {};\\   
     1442\qquad
     1443\begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}]
     1444    \matrix [diag] (m) {%
     1445         \node (s1) {s_1}; & \node (t1) {s_1'};\\
     1446         \node (s2) {s_2}; & \node (t2) {s_2'}; \\
     1447    };
     1448    {[-stealth]
     1449    \draw (s1) -- node [above] {$L$} (t1);
     1450    \draw [new] (s2) -- node [above] {$L$} (t2);
     1451    }
     1452    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
     1453    \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2);
     1454\end{tikzpicture}
     1455\text{ if $L\notin\ell(\Functions)$}
     1456\qquad
     1457\begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}]
     1458    \matrix [diag] (m) {%
     1459         \node (s1) {s_1}; & \node (t1) {s_1'};\\
     1460         \node (s2) {s_2};\\
     1461    };
     1462    {[-stealth]
     1463    \draw (s1) -- node [above] {$\ell(f)$} (t1);
     1464    }
     1465    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
     1466    \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (s2);
     1467\end{tikzpicture}
     1468\\[10pt]
     1469\begin{tikzpicture}
     1470    \matrix [diag, small vgap] (m) {%
     1471         &\node (t1) {s_1'}; \\
     1472         \node (s1) {s_1}; \\
     1473         && \node (l1) {s_b}; & \node (l2) {s_c}; & \node (t2) {s_2'};\\
     1474         \node (s2) {s_2}; & \node (c) {s_a};\\   
    14451475    };
    14461476    {[-stealth]
    14471477    \draw (s1) -- node [above left] {$f$} (t1);
    1448     \draw [new] (s2) -- node [above] {$*$} (c);
    1449     \draw [new] (c) -- node [below right] {$f$} (l);
    1450     \draw [new] (l) -- node [above] {$*$} (t2);
     1478    \draw [new] (s2) -- node [above] {$\tau *$} (c);
     1479    \draw [new] (c) -- node [above left] {$f$} (l1);
     1480    \draw [new] (l1) -- node [above] {$\ell(f)$} (l2);
     1481    \draw [new] (l2) -- node [above] {$\tau *$} (t2);
    14511482    }
    14521483    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
    14531484    \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2);
    1454     \draw [new] (t1) to [bend left] node [rel] {$\L$} (l);
    14551485    \draw [new] (t1) to [bend right] node [rel] {$\C$} (c);
    1456     \end{tikzpicture}
    1457 \caption{The \verb+cl_call+ case.}
    1458 \label{subfig:cl_call}
    1459 \end{subfigure}
    1460 &
    1461 \begin{subfigure}{.375\linewidth}
    1462 \centering
    1463 \begin{tikzpicture}[every join/.style={ar}, join all, thick,
    1464                             every label/.style=overlay, node distance=10mm]
    1465     \matrix [diag, small gap] (m) {%
    1466         \node (s1) [is ret] {}; \\
    1467         &\node (t1) {}; \\
    1468         \node (s2) {}; & \node (c) [is ret] {};\\
    1469         && \node (r) {}; & \node (t2) {}; \\   
     1486\end{tikzpicture}
     1487\qquad\qquad
     1488\begin{tikzpicture}
     1489    \matrix [diag, small vgap] (m) {%
     1490        \node (s1) {s_1}; \\
     1491        &\node (t1) {s_1'}; \\
     1492        \node (s2) {s_2}; & \node (c) {s_a};\\
     1493        && \node (r) {s_b}; & \node (t2) {s_2'}; \\   
    14701494    };
    14711495    {[-stealth]
    14721496    \draw (s1) -- node [above right] {$RET$} (t1);
    1473     \draw [new] (s2) -- node [above] {$*$} (c);
     1497    \draw [new] (s2) -- node [above] {$\tau *$} (c);
    14741498    \draw [new] (c) -- node [below left] {$RET$} (r);
    1475     \draw [new] (r) -- node [above] {$*$} (t2);
     1499    \draw [new] (r) -- node [above] {$\tau *$} (t2);
    14761500    }
    14771501    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
    1478     \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2);
     1502    \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S$} (t2);
    14791503    \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
    14801504\end{tikzpicture}
    1481 \caption{The \verb+cl_return+ case.}
    1482 \label{subfig:cl_return}
    1483 \end{subfigure}
    1484 \end{tabular}
    1485 \caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.
    1486          Dashed lines
    1487          and arrows indicates how the diagrams must be closed when solid relations
    1488          are present.}
     1505\caption{The hypotheses of ???. Dashed relations are implied by solid ones.}
    14891506\label{fig:forwardsim}
    14901507\end{figure}
     1508
     1509
     1510% \begin{figure}
     1511% \centering
     1512% \begin{tabular}{@{}c@{}c@{}c@{}}
     1513% % \begin{subfigure}{.475\linewidth}
     1514% % \centering
     1515% % \begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1516% %                             every label/.style=overlay, node distance=10mm]
     1517% %     \matrix [diag] (m) {%
     1518% %          \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
     1519% %          \node (s2) {}; & \node (t2) {}; \\
     1520% %     };
     1521% %     \node [above=0 of t1, overlay] {$\alpha$};
     1522% %     {[-stealth]
     1523% %     \draw (s1) -- (t1);
     1524% %     \draw [new] (s2) -- node [above] {$*$} (t2);
     1525% %     }
     1526% %     \draw (s1) to node [rel] {$\S$} (s2);
     1527% %     \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
     1528% % \end{tikzpicture}
     1529% % \caption{The \verb+cl_jump+ case.}
     1530% % \label{subfig:cl_jump}
     1531% % \end{subfigure}
     1532% % &
     1533% \begin{subfigure}{.25\linewidth}
     1534% \centering
     1535% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1536%                             every label/.style=overlay, node distance=10mm]
     1537%     \matrix [diag] (m) {%
     1538%          \node (s1) {}; & \node (t1) {};\\
     1539%          \node (s2) {}; & \node (t2) {}; \\
     1540%     };
     1541%     {[-stealth]
     1542%     \draw (s1) -- (t1);
     1543%     \draw [new] (s2) -- node [above] {$*$} (t2);
     1544%     }
     1545%     \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
     1546%     \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2);
     1547% \end{tikzpicture}
     1548% \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.}
     1549% \label{subfig:cl_other_jump}
     1550% \end{subfigure}
     1551% &
     1552% \begin{subfigure}{.375\linewidth}
     1553% \centering
     1554% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1555%                             every label/.style=overlay, node distance=10mm]
     1556%     \matrix [diag, small gap] (m) {%
     1557%          &\node (t1) {}; \\
     1558%          \node (s1) [is call] {}; \\
     1559%          && \node (l) {}; & \node (t2) {};\\
     1560%          \node (s2) {}; & \node (c) [is call] {};\\   
     1561%     };
     1562%     {[-stealth]
     1563%     \draw (s1) -- node [above left] {$f$} (t1);
     1564%     \draw [new] (s2) -- node [above] {$*$} (c);
     1565%     \draw [new] (c) -- node [below right] {$f$} (l);
     1566%     \draw [new] (l) -- node [above] {$*$} (t2);
     1567%     }
     1568%     \draw (s1) to [bend right] node [rel] {$\S$} (s2);
     1569%     \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2);
     1570%     \draw [new] (t1) to [bend left] node [rel] {$\L$} (l);
     1571%     \draw [new] (t1) to [bend right] node [rel] {$\C$} (c);
     1572%     \end{tikzpicture}
     1573% \caption{The \verb+cl_call+ case.}
     1574% \label{subfig:cl_call}
     1575% \end{subfigure}
     1576% &
     1577% \begin{subfigure}{.375\linewidth}
     1578% \centering
     1579% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
     1580%                             every label/.style=overlay, node distance=10mm]
     1581%     \matrix [diag, small gap] (m) {%
     1582%         \node (s1) [is ret] {}; \\
     1583%         &\node (t1) {}; \\
     1584%         \node (s2) {}; & \node (c) [is ret] {};\\
     1585%         && \node (r) {}; & \node (t2) {}; \\   
     1586%     };
     1587%     {[-stealth]
     1588%     \draw (s1) -- node [above right] {$RET$} (t1);
     1589%     \draw [new] (s2) -- node [above] {$*$} (c);
     1590%     \draw [new] (c) -- node [below left] {$RET$} (r);
     1591%     \draw [new] (r) -- node [above] {$*$} (t2);
     1592%     }
     1593%     \draw (s1) to [bend right] node [rel] {$\S$} (s2);
     1594%     \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2);
     1595%     \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
     1596% \end{tikzpicture}
     1597% \caption{The \verb+cl_return+ case.}
     1598% \label{subfig:cl_return}
     1599% \end{subfigure}
     1600% \end{tabular}
     1601% \caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.
     1602%          Dashed lines
     1603%          and arrows indicates how the diagrams must be closed when solid relations
     1604%          are present.}
     1605% \label{fig:forwardsim}
     1606% \end{figure}
    14911607
    14921608\paragraph{1-to-many forward simulation conditions.}
Note: See TracChangeset for help on using the changeset viewer.