Index: /Papers/itp2013/ccexec.tex
===================================================================
 /Papers/itp2013/ccexec.tex (revision 2624)
+++ /Papers/itp2013/ccexec.tex (revision 2625)
@@ 354,5 +354,8 @@
as \texttt{cl\_other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds
if the next instruction to be executed in $s_2$ follows the function call
to be executed in (the witness of the $\Sigma$type) $s_1$.
+to be executed in (the witness of the $\Sigma$type) $s_1$. The two functions
+\texttt{as\_label} and \texttt{as\_cost\_ident} are used to extract the
+cost label/function call target from states whose next instruction is
+a cost emission/function call statement.
@@ 518,8 +521,7 @@
\end{comment}
A \texttt{trace\_label\_return} is isomorphic to a list of
\texttt{trace\_label\_label}s that end with a cost emission followed by a
\texttt{trace\_label\_label} that ends with a return.

The interesting cases are those of $(\texttt{trace\_any\_label}~b~s_1~s_2)$.
+\texttt{trace\_label\_label}s that ends with a cost emission followed by a
+return terminated \texttt{trace\_label\_label}.
+The interesting cases are those of $\texttt{trace\_any\_label}~b~s_1~s_2$.
A \texttt{trace\_any\_label} is a sequence of steps built by a syntax directed
definition on the classification of $s_1$. The constructors of the datatype
@@ 529,5 +531,5 @@
\begin{enumerate}
\item the trace is never empty; it ends with a return iff $b$ is
 true (\texttt{ends\_with\_ret})
+ true
\item a jump must always be the last instruction of the trace, and it must
be followed by a cost emission statement; i.e. the target of a jump
@@ 536,6 +538,7 @@
\item a cost emission statement can never occur inside the trace, only in
the status immediately after
 \item the trace for a function call step is made from a subtrace of type
 $(\texttt{trace\_label\_return}~s_1~s_2)$, possibly followed by the
+ \item the trace for a function call step is made of a subtrace for the
+ function body of type
+ $\texttt{trace\_label\_return}~s_1~s_2$, possibly followed by the
rest of the trace for this basic block. The subtrace represents the
function execution. Being an inductive datum, it grants totality of
@@ 549,15 +552,13 @@
instruction is a cost emission statement. We only show here the type of one
of them:
\begin{verbatim}
+\begin{alltt}
flatten_trace_label_return:
 (S: abstract_status)
 (start_status: S) (final_status: S)
 (the_trace: trace_label_return S start_status final_status)
 on the_trace: list (as_cost_label S)
\end{verbatim}
+ \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\).
+ trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S)
+\end{alltt}
\paragraph{Cost prediction on structured traces}
The first main theorem of CerCo about structured traces
+The first main theorem of CerCo about traces
(theorem \texttt{compute\_max\_trace\_label\_return\_cost\_ok\_with\_trace})
holds for the
@@ 565,6 +566,10 @@
of the structured traces to the concrete status of object code programs.
Simplifying a bit, it states that
$\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.
 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
+\begin{equation}\label{th1}
+\begin{array}{l}\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~
+ \texttt{clock}~s_2 = \texttt{clock}~s_1 + \Sigma_{s \in (\texttt{flatten\_trace\_label\_return}~\tau)}\;k(\mathcal{L}(s))
+\end{array}
+\end{equation}
+where $\mathcal{L}$ maps a labelled state to its emitted label, and the
cost model $k$ is statically computed from the object code
by associating to each label \texttt{L} the sum of the cost of the instructions
@@ 597,19 +602,26 @@
interested only in those compiler passes that maps a trace $\tau_1$ to a trace
$\tau_2$ such that
\begin{displaymath}(\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2)\label{condition1}\end{displaymath}
The reason is that when this happens we obviously have the
following corollary to the previous theorem:
$$\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.
 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))$$
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
+\begin{equation}\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2\label{condition1}\label{th2}\end{equation}
+The reason is that the combination of~\ref{th1} with~\ref{th2} yields the
+corollary
+\begin{equation}\begin{array}{l}\label{th3}
+\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.\\~~~~~\;
+ 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))
+\end{array}\end{equation}
+This 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
transfer the cost model from the target to the source code and reason on the
source code only.
We are therefore interested in conditions stronger than~\ref{condition1}.
Therefore we introduce here a similarity relation between traces that captures
the fact that two traces have the same structure and that
implies~\ref{condition1} (theorem \texttt{tlr\_rel\_to\_traces\_same\_flatten}). Two traces are similar when one can be obtained from
the other by erasing or inserting steps classified as \texttt{other} into the
\texttt{trace\_any\_label} blocks of the trace. In particular,
+Therefore we introduce here a similarity relation between traces with
+the same structure. Theorem~\texttt{tlr\_rel\_to\_traces\_same\_flatten}
+in the Matita formalization shows that~\ref{th2} holds for every pair
+$(\tau_1,\tau_2)$ of similar traces.
+
+Intuitively, two traces are similar when one can be obtained from
+the other by erasing or inserting silent steps, i.e. states that are
+not \texttt{as\_costed} and that are classified as \texttt{other}.
+Silent steps do not alter the structure of the traces.
+In particular,
the relation maps function calls to function calls to the same function,
label emission statements to emissions of the same label, concatenation of
@@ 617,8 +629,7 @@
the same emissione statement, etc.
The similarity relation definition if simple, but it involves a large
number of cases. In the formalization, we define
$(\texttt{tlr\_rel}~tlr_1~tlr_2)$ by structural recursion on $tlr_1$ and pattern
matching over $tlr_2$. Here we turn
+In the formalization the three similarity relations  one for each trace
+kind  are defined by structural recursion on the first trace and pattern
+matching over the second. Here we turn
the definition into inference rules for the sake of readability. We also
omit from trace constructors all arguments, but those that are traces or that
@@ 756,12 +767,11 @@
In the preceding rules, a $taa$ is an inhabitant of the
$(\texttt{trace\_any\_any}~s_1~s_2)$ inductive data type whose definition
we do not give in the paper for lack of space. It is the type of valid
+$\texttt{trace\_any\_any}~s_1~s_2$ inductive data type whose definition
+is not in the paper for lack of space. It is the type of valid
prefixes (even empty ones) of \texttt{trace\_any\_label}s that do not contain
any function call. Therefore it
is possible to concatenate (using ``$@$'') a \texttt{trace\_any\_any} to the
left of a \texttt{trace\_any\_label}. The intuition is that two traces are
similar if one of them can perform more silent (non observables) moves,
whose sequences are here represented by \texttt{trace\_any\_any}.
+left of a \texttt{trace\_any\_label}. A \texttt{trace\_any\_any} captures
+a sequence of silent moves.
The \texttt{tal\_collapsable} unary predicate over \texttt{trace\_any\_label}s
@@ 788,5 +798,5 @@
forward simulation is the existence of a relation $R$ over states such that
if $s_1 R s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
$s_1' \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the
+$s_2 \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the
one and multi step transition relations $\to^n$ with the existence of
a structured trace between the two states, and we need to add the request that
@@ 801,5 +811,5 @@
in the general case. To understand why, consider the case of a function call
and the pass that fixes the parameter passing conventions. A function
call in the source code takes in input an arbitrary number of pseudoregisters (the actual parameters to pass) and returns an arbitrary number of pseudoregisters (where the result is stored). A function call in the target call has no
+call in the source code takes in input an arbitrary number of pseudoregisters (the actual parameters to pass) and returns an arbitrary number of pseudoregisters (where the result is stored). A function call in the target language has no
input nor output parameters. The pass must add explicit code before and after
the function call to move the pseudoregisters content from/to the hardware
@@ 850,9 +860,9 @@
For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and
$\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
$(\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
+$\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
$taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}.
\end{condition}
In the above condition, a $(\texttt{trace\_any\_any\_free}~s_1~s_2)$ is an
+In the above condition, a $\texttt{trace\_any\_any\_free}~s_1~s_2$ is an
inductive type of structured traces that do not contain function calls or
cost emission statements. Differently from a \texttt{trace\_any\_any}, the
@@ 867,11 +877,11 @@
\begin{condition}[Case \texttt{cl\_call}]
 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
 $\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
$(\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type
$(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
+ For all $s_1,s_1',s_2$ s.t. $s_1 \mathcal{S} s_1'$ and
+ $\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
+$\texttt{trace\_any\_any}~s_2~s_b$, and a
+$\texttt{trace\_any\_any\_free}~s_a~s_2'$ such that:
$s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of
the two call states are the same, $s_1 \mathcal{C} s_b$, the predicate
$(\texttt{as\_execute}~s_b~s_a)$ holds, $s_1' \mathcal{L} s_b$ and
+the two call states are the same, $s_1 \mathcal{C} s_b$,
+$\texttt{as\_execute}~s_b~s_a$ holds, $s_1' \mathcal{L} s_b$ and
$s_1' \mathcal{S} s_2'$.
\end{condition}