Index: /Papers/itp-2013/ccexec2.tex
===================================================================
--- /Papers/itp-2013/ccexec2.tex (revision 3344)
+++ /Papers/itp-2013/ccexec2.tex (revision 3345)
@@ -588,4 +588,50 @@
\section{Structured traces}
\label{semantics}
+
+Let's consider a generic unstructured language already equipped with a
+small step structured operational semantics (SOS). We introduce a
+deterministic labelled transition system~\cite{LTS} $(S,s_i,\Lambda,\to)$
+that refines the
+SOS by observing function calls and the beginning of basic blocks.
+$S$ is the set of states of the program, $s_i$ the initial state and
+$\Lambda = \{ \tau, RET \} \cup \mathcal{L} \cup \mathcal{F}$
+where $\mathcal{F}$ is the set of names of functions that can occur in the
+program, $\mathcal{L}$ is a set of labels disjoint from $\mathcal{F}$
+and $\tau$ and $RET$ do not belong to $\mathcal{F} \cup \mathcal{L}$.
+The transition function is defined as $s_1 \stackrel{o}{\to} s_2$ if
+$s_1$ moves to $s_2$ according to the SOS; moreover $o = f \in \mathcal{F}$ if
+the function $f$ is called, $o = RET$ if a \texttt{RETURN} is executed,
+$o = L \in \mathcal{L}$ if a \texttt{EMIT L} is executed to signal the
+beginning of a basic block, and $o = \tau$ in all other cases.
+Because we assume the language to be deterministic, the label emitted can
+actually be computed simply observing $s_1$.
+
+Among all possible finite execution fragments
+$s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_1}{\to} s_n$ we want to
+identify the ones that satisfy the requirements we sketched in the previous
+section. We say that an execution fragment is \emph{structured} iff
+\begin{enumerate}
+ \item for every $i$, if $s_i \stackrel{f}{\to} s_{i+1}$ then there is a
+ label $L$ such that $s_{i+1} \stackrel{L}{\to} s_{i+2}$.
+ Equivalently, $s_{i+1}$ must start execution with an \texttt{EMIT L}.
+ This captures the requirement that the body of function calls always start
+ with a label emission statement.
+ \item for every $i$, if $s_i \stackrel{f}{\to} s_{i+1}$ then
+ there is a strucuted $s_{i+1} \stackrel{o_{i+1}}{\to} \ldots
+ \stackrel{o_n}{\to} s_{n+1}$ such that $s_{n+1} \stackrel{RET}{\to} s_{n+2}$
+ and the instruction to be executed in $s_{n+2}$ follows the call that was
+ executed in $s_i$. This captures the double requirement that every function
+ call must converge and that it must yield back control just after the call.
+ \item for every $i$, if the instruction to be executed in $s_i$ is a
+ conditional branch, then there is an $L$ such that $s_{i+1} \stackrel{L}{\to} s_{i+2}$ or, equivalently, that $s_{i+1}$ must start execution with an
+ \texttt{EMIT L}. This captures the requirement that every branch which is
+ live code must start with a label emission.
+\end{enumerate}
+
+
+
+
+========================================================================
+
The program semantics adopted in the traditional labelling approach is based
on labelled deductive systems. Given a set of observables $\mathcal{O}$ and