# Changeset 3346

Ignore:
Timestamp:
Jun 12, 2013, 2:50:49 PM (6 years ago)
Message:

...

File:
1 edited

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

 r3345 Among all possible finite execution fragments $s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_1}{\to} s_n$ we want to $s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ 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 \end{enumerate} Let $T = s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} 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 every internal action $\tau$. 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)$. The labelling approach is based on the idea that the execution cost of certain execution fragments, that we call \emph{measurable fragments}, can be computed from their weak trace by choosing a $k$ that assigns to any label the cost of the instructions in its scope. A fragment $T = s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ is measurable if it does not start or end in the middle of a basic block. Ending in the middle of a block would mean having pre-paid more instructions than the ones executed, and starting in the middle would mean not paying any instruction up to the first label emission. Formally we require $o_0 \in \mathcal{L}$ (or equivalently in $s_0$ the program must emit a label) and $s_{n+1}$ must either be a \texttt{RETURN} or a label emission statement (or, equivalently, $s_{n+1} \stackrel{o_{n+1}} s_{n+2}$ with $o_{n+1} \in \mathcal{L} \cup \{RET\}$). Given two deterministic unstructured programming languages with their own operational semantics, we say that a state $s_2$ of the second language (weakly) simulates the state $s_1$ of the first iff the two unique weak traces that originate from them are equal. If $s_1$ also (weakly) simulates $s_2$, then the two states are weakly trace equivalent. or, equivalently because of determinism, that they are weakly bisimilar.
Note: See TracChangeset for help on using the changeset viewer.