Changeset 3345


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

...

File:
1 edited

Legend:

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

    r3344 r3345  
    588588\section{Structured traces}
    589589\label{semantics}
     590
     591Let's consider a generic unstructured language already equipped with a
     592small step structured operational semantics (SOS). We introduce a
     593deterministic labelled transition system~\cite{LTS} $(S,s_i,\Lambda,\to)$
     594that refines the
     595SOS by observing function calls and the beginning of basic blocks.
     596$S$ is the set of states of the program, $s_i$ the initial state and
     597$\Lambda = \{ \tau, RET \} \cup \mathcal{L} \cup \mathcal{F}$
     598where $\mathcal{F}$ is the set of names of functions that can occur in the
     599program, $\mathcal{L}$ is a set of labels disjoint from $\mathcal{F}$
     600and $\tau$ and $RET$ do not belong to $\mathcal{F} \cup \mathcal{L}$.
     601The transition function is defined as $s_1 \stackrel{o}{\to} s_2$ if
     602$s_1$ moves to $s_2$ according to the SOS; moreover $o = f \in \mathcal{F}$ if
     603the function $f$ is called, $o = RET$ if a \texttt{RETURN} is executed,
     604$o = L \in \mathcal{L}$ if a \texttt{EMIT L} is executed to signal the
     605beginning of a basic block, and $o = \tau$ in all other cases.
     606Because we assume the language to be deterministic, the label emitted can
     607actually be computed simply observing $s_1$.
     608
     609Among all possible finite execution fragments
     610$s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_1}{\to} s_n$ we want to
     611identify the ones that satisfy the requirements we sketched in the previous
     612section. We say that an execution fragment is \emph{structured} iff
     613\begin{enumerate}
     614 \item for every $i$, if $s_i \stackrel{f}{\to} s_{i+1}$ then there is a
     615   label $L$ such that $s_{i+1} \stackrel{L}{\to} s_{i+2}$.
     616   Equivalently, $s_{i+1}$ must start execution with an \texttt{EMIT L}.
     617   This captures the requirement that the body of function calls always start
     618   with a label emission statement.
     619 \item for every $i$, if $s_i \stackrel{f}{\to} s_{i+1}$ then
     620   there is a strucuted $s_{i+1} \stackrel{o_{i+1}}{\to} \ldots
     621   \stackrel{o_n}{\to} s_{n+1}$ such that $s_{n+1} \stackrel{RET}{\to} s_{n+2}$
     622   and the instruction to be executed in $s_{n+2}$ follows the call that was
     623   executed in $s_i$. This captures the double requirement that every function
     624   call must converge and that it must yield back control just after the call.
     625 \item for every $i$, if the instruction to be executed in $s_i$ is a
     626   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
     627   \texttt{EMIT L}. This captures the requirement that every branch which is
     628   live code must start with a label emission.
     629\end{enumerate}
     630
     631
     632
     633
     634========================================================================
     635
    590636The program semantics adopted in the traditional labelling approach is based
    591637on labelled deductive systems. Given a set of observables $\mathcal{O}$ and
Note: See TracChangeset for help on using the changeset viewer.