# Changeset 3345

Ignore:
Timestamp:
Jun 12, 2013, 12:13:24 PM (4 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r3344 \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