Changeset 3345 for Papers/itp2013/ccexec2.tex
 Timestamp:
 Jun 12, 2013, 12:13:24 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec2.tex
r3344 r3345 588 588 \section{Structured traces} 589 589 \label{semantics} 590 591 Let's consider a generic unstructured language already equipped with a 592 small step structured operational semantics (SOS). We introduce a 593 deterministic labelled transition system~\cite{LTS} $(S,s_i,\Lambda,\to)$ 594 that refines the 595 SOS 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}$ 598 where $\mathcal{F}$ is the set of names of functions that can occur in the 599 program, $\mathcal{L}$ is a set of labels disjoint from $\mathcal{F}$ 600 and $\tau$ and $RET$ do not belong to $\mathcal{F} \cup \mathcal{L}$. 601 The 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 603 the 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 605 beginning of a basic block, and $o = \tau$ in all other cases. 606 Because we assume the language to be deterministic, the label emitted can 607 actually be computed simply observing $s_1$. 608 609 Among all possible finite execution fragments 610 $s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_1}{\to} s_n$ we want to 611 identify the ones that satisfy the requirements we sketched in the previous 612 section. 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 590 636 The program semantics adopted in the traditional labelling approach is based 591 637 on labelled deductive systems. Given a set of observables $\mathcal{O}$ and
Note: See TracChangeset
for help on using the changeset viewer.