Changeset 3346
 Timestamp:
 Jun 12, 2013, 2:50:49 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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