Changeset 3348 for Papers/itp-2013

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

ipotesi della forward simulation

File:
1 edited

Legend:

Unmodified
 r3347 diag/.style={row sep={11mm,between origins}, column sep={11mm,between origins}, every node/.style={draw, is other}}, every node/.style={execute at begin node=$, execute at end node=$}, %                       every node/.style={draw, is other}, }, small vgap/.style={row sep={7mm,between origins}}, small gap/.style={row sep={7mm,between origins},column sep={7mm,between origins}}, small hgap/.style={column sep={7mm,between origins}}, small gap/.style={small vgap, small hgap}, % for article, maybe temporary is jump/.style=is other, where $\Functions$ is the set of names of functions that can occur in the program, $\Labels$ is a set of labels disjoint from $\Functions$ and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$. and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$. Moreover there is an injective function $\ell : \Functions \to \Labels$ that tells the starting label of the body of each function, and $\ell(\Functions)\subseteq \Labels$ denotes the image of this function. The transition function is defined as $s_1 \to[o] s_2$ if $s_1$ moves to $s_2$ according to the SOS; moreover $o = f \in \Functions$ if \item For every $i$, if $s_i \to[f] s_{i+1}$ then there is a label $L$ and a $k\ge i+2$ such that $s_{i+1} \to[L] s_{i+2} \To s_k \to[RET] s_{k+1}$, with $s_{i+1} \to[\ell(f)] s_{i+2} \To s_k \to[RET] s_{k+1}$, with $s_i \ar s_{k+1}$. In other words, $s_{i+1}$ must start execution with an \verb+EMIT $L$+ In other words, $s_{i+1}$ must start execution with \verb+EMIT $\ell(f)$+ and then continue with a structured fragment returning control to the instruction immediately following the call. with a label emission statement, and every function call must converge yielding back control just after it. \item For every $i$ and $f$, if $s_{i+1}\to[\ell(f)]s_{i+2}$ then $s_i\to[f]s_{i+1}$. This is a technical condition needed to ensure that labels associated with functions always follow a call. \item The number of $RET$'s in the fragment is equal to the number of calls, i.e.\ the number of observables in $\Functions$. This, together with live code must start with a label emission. \end{enumerate} Let $T = s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ be an One might wonder why $f$ and $\ell(f)$, that aways appear in this order, are not collapsed into a single observable. This would indeed simplify some aspects of the formalisation, but has the problem of misassagning the cost of calls, which would fall under the associated label. As different call instructions with different costs are possible, this is not acceptable. Let $T = s_0 \to[o_0] s_1 \ldots \to[o_n] s_{n+1}$ be an execution fragment. The \emph{weak trace} $|T|$ associated to $T$ is the subsequence $o_{i_0} \ldots o_{i_m}$ of $o_0 \ldots o_n$ obtained dropping Let $k$ be a cost model that maps observables actions to any commutative cost monoid (e.g. natural numbers). We extend the domain of $k$ to weak traces by posing $k(\mathcal{T}) = \Sigma_{o \in \mathcal{T}} k(o)$. monoid (e.g. natural numbers). We extend the domain of $k$ to fragments by posing $k(T) = \Sigma_{o \in |T|} k(o)$. The labelling approach is based on the idea that the execution cost of %    as_after_return s2_pre s2_ret. % \end{alltt} \begin{figure} \centering \begin{tabular}{@{}c@{}c@{}c@{}} % \begin{subfigure}{.475\linewidth} % \centering % \end{subfigure} % & \begin{subfigure}{.25\linewidth} \centering \begin{tikzpicture}[every join/.style={ar}, join all, thick, every label/.style=overlay, node distance=10mm] \begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}] \matrix [diag] (m) {% \node (s1) {}; & \node (t1) {};\\ \node (s2) {}; & \node (t2) {}; \\ \node (s1) {s_1}; & \node (t1) {s_1'};\\ \node (s2) {s_2}; & \node (t2) {s_2'}; \\ }; {[-stealth] \draw (s1) -- (t1); \draw [new] (s2) -- node [above] {$*$} (t2); \draw (s1) -- node [above] {$\tau$} (t1); \draw [new] (s2) -- node [above] {$\tau *$} (t2); } \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2); \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2); \end{tikzpicture} \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.} \label{subfig:cl_other_jump} \end{subfigure} & \begin{subfigure}{.375\linewidth} \centering \begin{tikzpicture}[every join/.style={ar}, join all, thick, every label/.style=overlay, node distance=10mm] \matrix [diag, small gap] (m) {% &\node (t1) {}; \\ \node (s1) [is call] {}; \\ && \node (l) {}; & \node (t2) {};\\ \node (s2) {}; & \node (c) [is call] {};\\ \qquad \begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}] \matrix [diag] (m) {% \node (s1) {s_1}; & \node (t1) {s_1'};\\ \node (s2) {s_2}; & \node (t2) {s_2'}; \\ }; {[-stealth] \draw (s1) -- node [above] {$L$} (t1); \draw [new] (s2) -- node [above] {$L$} (t2); } \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2); \end{tikzpicture} \text{ if $L\notin\ell(\Functions)$} \qquad \begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}] \matrix [diag] (m) {% \node (s1) {s_1}; & \node (t1) {s_1'};\\ \node (s2) {s_2};\\ }; {[-stealth] \draw (s1) -- node [above] {$\ell(f)$} (t1); } \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (s2); \end{tikzpicture} \\[10pt] \begin{tikzpicture} \matrix [diag, small vgap] (m) {% &\node (t1) {s_1'}; \\ \node (s1) {s_1}; \\ && \node (l1) {s_b}; & \node (l2) {s_c}; & \node (t2) {s_2'};\\ \node (s2) {s_2}; & \node (c) {s_a};\\ }; {[-stealth] \draw (s1) -- node [above left] {$f$} (t1); \draw [new] (s2) -- node [above] {$*$} (c); \draw [new] (c) -- node [below right] {$f$} (l); \draw [new] (l) -- node [above] {$*$} (t2); \draw [new] (s2) -- node [above] {$\tau *$} (c); \draw [new] (c) -- node [above left] {$f$} (l1); \draw [new] (l1) -- node [above] {$\ell(f)$} (l2); \draw [new] (l2) -- node [above] {$\tau *$} (t2); } \draw (s1) to [bend right] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); \draw [new] (t1) to [bend left] node [rel] {$\L$} (l); \draw [new] (t1) to [bend right] node [rel] {$\C$} (c); \end{tikzpicture} \caption{The \verb+cl_call+ case.} \label{subfig:cl_call} \end{subfigure} & \begin{subfigure}{.375\linewidth} \centering \begin{tikzpicture}[every join/.style={ar}, join all, thick, every label/.style=overlay, node distance=10mm] \matrix [diag, small gap] (m) {% \node (s1) [is ret] {}; \\ &\node (t1) {}; \\ \node (s2) {}; & \node (c) [is ret] {};\\ && \node (r) {}; & \node (t2) {}; \\ \end{tikzpicture} \qquad\qquad \begin{tikzpicture} \matrix [diag, small vgap] (m) {% \node (s1) {s_1}; \\ &\node (t1) {s_1'}; \\ \node (s2) {s_2}; & \node (c) {s_a};\\ && \node (r) {s_b}; & \node (t2) {s_2'}; \\ }; {[-stealth] \draw (s1) -- node [above right] {$RET$} (t1); \draw [new] (s2) -- node [above] {$*$} (c); \draw [new] (s2) -- node [above] {$\tau *$} (c); \draw [new] (c) -- node [below left] {$RET$} (r); \draw [new] (r) -- node [above] {$*$} (t2); \draw [new] (r) -- node [above] {$\tau *$} (t2); } \draw (s1) to [bend right] node [rel] {$\S$} (s2); \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2); \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S$} (t2); \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r); \end{tikzpicture} \caption{The \verb+cl_return+ case.} \label{subfig:cl_return} \end{subfigure} \end{tabular} \caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces. Dashed lines and arrows indicates how the diagrams must be closed when solid relations are present.} \caption{The hypotheses of ???. Dashed relations are implied by solid ones.} \label{fig:forwardsim} \end{figure} % \begin{figure} % \centering % \begin{tabular}{@{}c@{}c@{}c@{}} % % \begin{subfigure}{.475\linewidth} % % \centering % % \begin{tikzpicture}[every join/.style={ar}, join all, thick, % %                             every label/.style=overlay, node distance=10mm] % %     \matrix [diag] (m) {% % %          \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\ % %          \node (s2) {}; & \node (t2) {}; \\ % %     }; % %     \node [above=0 of t1, overlay] {$\alpha$}; % %     {[-stealth] % %     \draw (s1) -- (t1); % %     \draw [new] (s2) -- node [above] {$*$} (t2); % %     } % %     \draw (s1) to node [rel] {$\S$} (s2); % %     \draw [new] (t1) to node [rel] {$\S,\L$} (t2); % % \end{tikzpicture} % % \caption{The \verb+cl_jump+ case.} % % \label{subfig:cl_jump} % % \end{subfigure} % % & % \begin{subfigure}{.25\linewidth} % \centering % \begin{tikzpicture}[every join/.style={ar}, join all, thick, %                             every label/.style=overlay, node distance=10mm] %     \matrix [diag] (m) {% %          \node (s1) {}; & \node (t1) {};\\ %          \node (s2) {}; & \node (t2) {}; \\ %     }; %     {[-stealth] %     \draw (s1) -- (t1); %     \draw [new] (s2) -- node [above] {$*$} (t2); %     } %     \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); %     \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2); % \end{tikzpicture} % \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.} % \label{subfig:cl_other_jump} % \end{subfigure} % & % \begin{subfigure}{.375\linewidth} % \centering % \begin{tikzpicture}[every join/.style={ar}, join all, thick, %                             every label/.style=overlay, node distance=10mm] %     \matrix [diag, small gap] (m) {% %          &\node (t1) {}; \\ %          \node (s1) [is call] {}; \\ %          && \node (l) {}; & \node (t2) {};\\ %          \node (s2) {}; & \node (c) [is call] {};\\ %     }; %     {[-stealth] %     \draw (s1) -- node [above left] {$f$} (t1); %     \draw [new] (s2) -- node [above] {$*$} (c); %     \draw [new] (c) -- node [below right] {$f$} (l); %     \draw [new] (l) -- node [above] {$*$} (t2); %     } %     \draw (s1) to [bend right] node [rel] {$\S$} (s2); %     \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); %     \draw [new] (t1) to [bend left] node [rel] {$\L$} (l); %     \draw [new] (t1) to [bend right] node [rel] {$\C$} (c); %     \end{tikzpicture} % \caption{The \verb+cl_call+ case.} % \label{subfig:cl_call} % \end{subfigure} % & % \begin{subfigure}{.375\linewidth} % \centering % \begin{tikzpicture}[every join/.style={ar}, join all, thick, %                             every label/.style=overlay, node distance=10mm] %     \matrix [diag, small gap] (m) {% %         \node (s1) [is ret] {}; \\ %         &\node (t1) {}; \\ %         \node (s2) {}; & \node (c) [is ret] {};\\ %         && \node (r) {}; & \node (t2) {}; \\ %     }; %     {[-stealth] %     \draw (s1) -- node [above right] {$RET$} (t1); %     \draw [new] (s2) -- node [above] {$*$} (c); %     \draw [new] (c) -- node [below left] {$RET$} (r); %     \draw [new] (r) -- node [above] {$*$} (t2); %     } %     \draw (s1) to [bend right] node [rel] {$\S$} (s2); %     \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2); %     \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r); % \end{tikzpicture} % \caption{The \verb+cl_return+ case.} % \label{subfig:cl_return} % \end{subfigure} % \end{tabular} % \caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces. %          Dashed lines %          and arrows indicates how the diagrams must be closed when solid relations %          are present.} % \label{fig:forwardsim} % \end{figure} \paragraph{1-to-many forward simulation conditions.}