Ignore:
Timestamp:
Feb 6, 2013, 8:14:38 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r2622 r2625  
    354354as \texttt{cl\_other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds
    355355if the next instruction to be executed in $s_2$ follows the function call
    356 to be executed in (the witness of the $\Sigma$-type) $s_1$.
     356to be executed in (the witness of the $\Sigma$-type) $s_1$. The two functions
     357\texttt{as\_label} and \texttt{as\_cost\_ident} are used to extract the
     358cost label/function call target from states whose next instruction is
     359a cost emission/function call statement.
    357360
    358361
     
    518521\end{comment}
    519522A \texttt{trace\_label\_return} is isomorphic to a list of
    520 \texttt{trace\_label\_label}s that end with a cost emission followed by a
    521 \texttt{trace\_label\_label} that ends with a return.
    522 
    523 The interesting cases are those of $(\texttt{trace\_any\_label}~b~s_1~s_2)$.
     523\texttt{trace\_label\_label}s that ends with a cost emission followed by a
     524return terminated \texttt{trace\_label\_label}.
     525The interesting cases are those of $\texttt{trace\_any\_label}~b~s_1~s_2$.
    524526A \texttt{trace\_any\_label} is a sequence of steps built by a syntax directed
    525527definition on the classification of $s_1$. The constructors of the datatype
     
    529531\begin{enumerate}
    530532 \item the trace is never empty; it ends with a return iff $b$ is
    531        true (\texttt{ends\_with\_ret})
     533       true
    532534 \item a jump must always be the last instruction of the trace, and it must
    533535       be followed by a cost emission statement; i.e. the target of a jump
     
    536538 \item a cost emission statement can never occur inside the trace, only in
    537539       the status immediately after
    538  \item the trace for a function call step is made from a subtrace of type
    539        $(\texttt{trace\_label\_return}~s_1~s_2)$, possibly followed by the
     540 \item the trace for a function call step is made of a subtrace for the
     541       function body of type
     542       $\texttt{trace\_label\_return}~s_1~s_2$, possibly followed by the
    540543       rest of the trace for this basic block. The subtrace represents the
    541544       function execution. Being an inductive datum, it grants totality of
     
    549552instruction is a cost emission statement. We only show here the type of one
    550553of them:
    551 \begin{verbatim}
     554\begin{alltt}
    552555flatten_trace_label_return:
    553   (S: abstract_status)
    554     (start_status: S) (final_status: S)
    555       (the_trace: trace_label_return S start_status final_status)
    556         on the_trace: list (as_cost_label S)
    557 \end{verbatim}
     556 \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\).
     557  trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S)
     558\end{alltt}
    558559
    559560\paragraph{Cost prediction on structured traces}
    560561
    561 The first main theorem of CerCo about structured traces
     562The first main theorem of CerCo about traces
    562563(theorem \texttt{compute\_max\_trace\_label\_return\_cost\_ok\_with\_trace})
    563564holds for the
     
    565566of the structured traces to the concrete status of object code programs.
    566567Simplifying a bit, it states that
    567 $\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.
    568   clock~s_2 = clock~s_1 + \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau} k(L(s))$ where $L$ maps a labelled state to its emitted label, and the
     568\begin{equation}\label{th1}
     569\begin{array}{l}\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~
     570  \texttt{clock}~s_2 = \texttt{clock}~s_1 + \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau)}\;k(\mathcal{L}(s))
     571\end{array}
     572\end{equation}
     573where $\mathcal{L}$ maps a labelled state to its emitted label, and the
    569574cost model $k$ is statically computed from the object code
    570575by associating to each label \texttt{L} the sum of the cost of the instructions
     
    597602interested only in those compiler passes that maps a trace $\tau_1$ to a trace
    598603$\tau_2$ such that
    599 \begin{displaymath}(\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2)\label{condition1}\end{displaymath}
    600 The reason is that when this happens we obviously have the
    601 following corollary to the previous theorem:
    602 $$\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.
    603   clock~s_2 - clock~s_1 = \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau_1} k(L(s)) = \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau_2} k(L(s))$$
    604 The corollary states that the actual execution time of the program can be computed equally well on the source or target language. Thus it becomes possible to
     604\begin{equation}\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2\label{condition1}\label{th2}\end{equation}
     605The reason is that the combination of~\ref{th1} with~\ref{th2} yields the
     606corollary
     607\begin{equation}\begin{array}{l}\label{th3}
     608\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~~~~\;
     609  clock~s_2 - clock~s_1\\~ = \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau_1)}\;k(\mathcal{L}(s))\\~ = \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau_2)}\;k(\mathcal{L}(s))
     610\end{array}\end{equation}
     611This corollary states that the actual execution time of the program can be computed equally well on the source or target language. Thus it becomes possible to
    605612transfer the cost model from the target to the source code and reason on the
    606613source code only.
    607614
    608615We are therefore interested in conditions stronger than~\ref{condition1}.
    609 Therefore we introduce here a similarity relation between traces that captures
    610 the fact that two traces have the same structure and that
    611 implies~\ref{condition1} (theorem \texttt{tlr\_rel\_to\_traces\_same\_flatten}). Two traces are similar when one can be obtained from
    612 the other by erasing or inserting steps classified as \texttt{other} into the
    613 \texttt{trace\_any\_label} blocks of the trace. In particular,
     616Therefore we introduce here a similarity relation between traces with
     617the same structure. Theorem~\texttt{tlr\_rel\_to\_traces\_same\_flatten}
     618in the Matita formalization shows that~\ref{th2} holds for every pair
     619$(\tau_1,\tau_2)$ of similar traces.
     620
     621Intuitively, two traces are similar when one can be obtained from
     622the other by erasing or inserting silent steps, i.e. states that are
     623not \texttt{as\_costed} and that are classified as \texttt{other}.
     624Silent steps do not alter the structure of the traces.
     625In particular,
    614626the relation maps function calls to function calls to the same function,
    615627label emission statements to emissions of the same label, concatenation of
     
    617629the same emissione statement, etc.
    618630
    619 The similarity relation definition if simple, but it involves a large
    620 number of cases. In the formalization, we define
    621 $(\texttt{tlr\_rel}~tlr_1~tlr_2)$ by structural recursion on $tlr_1$ and pattern
    622 matching over $tlr_2$. Here we turn
     631In the formalization the three similarity relations --- one for each trace
     632kind --- are defined by structural recursion on the first trace and pattern
     633matching over the second. Here we turn
    623634the definition into inference rules for the sake of readability. We also
    624635omit from trace constructors all arguments, but those that are traces or that
     
    756767
    757768In the preceding rules, a $taa$ is an inhabitant of the
    758 $(\texttt{trace\_any\_any}~s_1~s_2)$ inductive data type whose definition
    759 we do not give in the paper for lack of space. It is the type of valid
     769$\texttt{trace\_any\_any}~s_1~s_2$ inductive data type whose definition
     770is not in the paper for lack of space. It is the type of valid
    760771prefixes (even empty ones) of \texttt{trace\_any\_label}s that do not contain
    761772any function call. Therefore it
    762773is possible to concatenate (using ``$@$'') a \texttt{trace\_any\_any} to the
    763 left of a \texttt{trace\_any\_label}. The intuition is that two traces are
    764 similar if one of them can perform more silent (non observables) moves,
    765 whose sequences are here represented by \texttt{trace\_any\_any}.
     774left of a \texttt{trace\_any\_label}. A \texttt{trace\_any\_any} captures
     775a sequence of silent moves.
    766776
    767777The \texttt{tal\_collapsable} unary predicate over \texttt{trace\_any\_label}s
     
    788798forward simulation is the existence of a relation $R$ over states such that
    789799if $s_1 R s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
    790 $s_1' \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the
     800$s_2 \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the
    791801one and multi step transition relations $\to^n$ with the existence of
    792802a structured trace between the two states, and we need to add the request that
     
    801811in the general case. To understand why, consider the case of a function call
    802812and the pass that fixes the parameter passing conventions. A function
    803 call in the source code takes in input an arbitrary number of pseudo-registers (the actual parameters to pass) and returns an arbitrary number of pseudo-registers (where the result is stored). A function call in the target call has no
     813call in the source code takes in input an arbitrary number of pseudo-registers (the actual parameters to pass) and returns an arbitrary number of pseudo-registers (where the result is stored). A function call in the target language has no
    804814input nor output parameters. The pass must add explicit code before and after
    805815the function call to move the pseudo-registers content from/to the hardware
     
    850860 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and
    851861 $\texttt{as\_execute}~s_1~s_1'$, and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ or $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ and
    852 $(\texttt{as\_costed}~s_1')$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
     862$\texttt{as\_costed}~s_1'$, there exists an $s_2'$ and a $\texttt{trace\_any\_any\_free}~s_2~s_2'$ called $taaf$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
    853863$taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}.
    854864\end{condition}
    855865
    856 In the above condition, a $(\texttt{trace\_any\_any\_free}~s_1~s_2)$ is an
     866In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ is an
    857867inductive type of structured traces that do not contain function calls or
    858868cost emission statements. Differently from a \texttt{trace\_any\_any}, the
     
    867877
    868878\begin{condition}[Case \texttt{cl\_call}]
    869  For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
    870  $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $taa_1$ of type
    871 $(\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type
    872 $(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
     879 For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$ and
     880 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a
     881$\texttt{trace\_any\_any}~s_2~s_b$, and a
     882$\texttt{trace\_any\_any\_free}~s_a~s_2'$ such that:
    873883$s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of
    874 the two call states are the same, $s_1 \mathcal{C} s_b$, the predicate
    875 $(\texttt{as\_execute}~s_b~s_a)$ holds, $s_1' \mathcal{L} s_b$ and
     884the two call states are the same, $s_1 \mathcal{C} s_b$,
     885$\texttt{as\_execute}~s_b~s_a$ holds, $s_1' \mathcal{L} s_b$ and
    876886$s_1' \mathcal{S} s_2'$.
    877887\end{condition}
Note: See TracChangeset for help on using the changeset viewer.