Changeset 3346


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

...

File:
1 edited

Legend:

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

    r3345 r3346  
    608608
    609609Among all possible finite execution fragments
    610 $s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_1}{\to} s_n$ we want to
     610$s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ we want to
    611611identify the ones that satisfy the requirements we sketched in the previous
    612612section. We say that an execution fragment is \emph{structured} iff
     
    629629\end{enumerate}
    630630
    631 
     631Let $T = s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ be an
     632execution fragment. The \emph{weak trace} $|T|$ associated to $T$ is the
     633subsequence $o_{i_0} \ldots o_{i_m}$ of $o_0 \ldots o_n$ obtained dropping
     634every internal action $\tau$.
     635
     636Let $k$ be a cost model that maps observables actions to any commutative cost
     637monoid (e.g. natural numbers). We extend the domain of $k$ to weak traces
     638by posing $k(\mathcal{T}) = \Sigma_{o \in \mathcal{T}} k(o)$.
     639
     640The labelling approach is based on the idea that the execution cost of
     641certain execution fragments, that we call \emph{measurable fragments}, can be
     642computed from their weak trace by choosing a $k$ that assigns to any label
     643the cost of the instructions in its scope.
     644A fragment
     645$T = s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ is
     646measurable if it does not start or end in the middle of a basic block.
     647Ending in the middle of a block would mean having pre-paid more instructions
     648than the ones executed, and starting in the middle would mean not paying any
     649instruction up to the first label emission.
     650Formally we require $o_0 \in \mathcal{L}$ (or equivalently
     651in $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\}$).
     652
     653Given two deterministic unstructured programming languages with their own
     654operational semantics, we say that a state $s_2$ of the second language
     655(weakly) simulates the state $s_1$ of the first iff the two unique weak traces
     656that originate from them are equal. If $s_1$ also (weakly) simulates $s_2$,
     657then the two states are weakly trace equivalent.
     658
     659 or, equivalently
     660because of determinism, that they are weakly bisimilar.
    632661
    633662
Note: See TracChangeset for help on using the changeset viewer.