Index: /Papers/itp2013/ccexec2.tex
===================================================================
 /Papers/itp2013/ccexec2.tex (revision 3365)
+++ /Papers/itp2013/ccexec2.tex (revision 3366)
@@ 1,3 +1,3 @@
\documentclass[bookmarksdepth=2,bookmarksopen]{llncs}
+\documentclass[bookmarksdepth=2,bookmarksopen,envcountsame]{llncs}
\usepackage{hyperref}
\usepackage{graphicx}
@@ 18,5 +18,17 @@
% a builtin definition.
%\newtheorem{theorem}{Theorem}
\newtheorem{condition}{Condition}
+% \usepackage{aliascnt} %% this will make autoref give correct names
+% \def\mynewtheorem#1[#2]#3{%
+% \newaliascnt{#1}{#2}%
+% \newtheorem{#1}[#1]{#3}%
+% \aliascntresetthe{#1}%
+% \expandafter\def\csname #1autorefname\endcsname{#3}%
+% }
+% \let\proof\relax
+% \let\endproof\relax
+% \usepackage{amsthm}
+% theorem environments
+% \theoremstyle{definition}
+\spnewtheorem{condition}[theorem]{Condition}{\bfseries}{}
\lstdefinelanguage{coq}
@@ 108,4 +120,5 @@
\def\R{\mathrel{\mathcal R}}
\def\C{\mathrel{\mathcal C}}
+\def\LS{\mathrel{\mathcal{L_S}}}
\def\Labels{\mathbb L}
@@ 131,8 +144,8 @@
\def\to{\@ifnextchar[{\new@to}{\oldto}}
\def\new@to[#1]{\xrightarrow{#1}}
\def\st@ck#1[#2]{\stackrel{#2}{#1}}
\def\defst@ck#1#2{\def#1{\@ifnextchar[{\st@ck#2}{#2}}}
\defst@ck\To\implies
\defst@ck\MeasTo\rightsquigarrow
+% \def\st@ck#1[#2]{\stackrel{#2}{#1}}
+% \def\defst@ck#1#2{\def#1{\@ifnextchar[{\st@ck#2}{#2}}}
+\let\To\implies
+% \let\MeasTo\rightsquigarrow
\makeatother
@@ 229,14 +242,14 @@
part that deals with the preservation of structure.
The plan of this paper is the following. In Section~\ref{labelling} we
+The plan of this paper is the following. In Section~\ref{sec:labelling} we
sketch the labelling method and the problems derived from the application
to languages with function calls. In Section~\ref{semantics} we introduce
+to languages with function calls. In Section~\ref{sec:semantics} we introduce
a generic description of an unstructured imperative language and the
corresponding structured traces (the novel semantics). In
Section~\ref{simulation} we describe the forward simulation proof.
Conclusions and future works are in Section~\ref{conclusions}
+Section~\ref{sec:simulation} we describe the forward simulation proof.
+Conclusions and future works are in Section~\ref{sec:conclusions}
\section{The labelling approach}
\label{labelling}
+\label{sec:labelling}
% \subsection{A brief introduction to the labelling approach}
We briefly explain the labelling approach as introduced in~\cite{easylabelling}
@@ 417,5 +430,5 @@
stack). This property, however, is a property of the runs of object code
programs, and not a property of the object code that can be easily statically
verified (as the ones required in \autoref{labelling} in absence of function calls).
+verified (as the ones required in \autoref{sec:labelling} in absence of function calls).
Therefore, we now need to single out those runs whose cost behaviour can be
statically predicted, and we need to prove that every run of programs generated
@@ 440,5 +453,5 @@
The proof of correctness of such a compiler is harder than a traditional
proof of preservation of functional properties, and a standard forward
simulation argument does not work. In \autoref{simulation} we present
+simulation argument does not work. In \autoref{sec:simulation} we present
a refinement of forward simulation that grants all required correctness
properties.
@@ 695,5 +708,5 @@
\subsection{Structured traces}
\label{semantics}
+\label{sec:semantics}
Let's consider a generic unstructured language already equipped with a
@@ 763,5 +776,5 @@
$s_i\to[f]s_{i+1}$. This is a technical condition needed to ensure that a
label associated with a function is only used at the beginning of its
 body. Its use will become clear in~\autoref{simulation}.
+ body. Its use will become clear in~\autoref{sec:simulation}.
\item For every $i$, if the instruction to be executed in $s_i$ is a
conditional branch, then there is an $L$ such that $s_{i+1} \to[L] s_{i+2}$ or, equivalently, that $s_{i+1}$ must start execution with an
@@ 788,5 +801,5 @@
\begin{theorem}
 \label{static}
+ \label{thm:static}
for all measurable fragment $T = s_0 \to^{*} s_n$,\\
$$\Delta_t := \verb+clock+_{s_n}  \verb+clock+_{s_0} = \Sigma_{o \in T} k(o)$$
@@ 835,5 +848,5 @@
holds for each compiler pass.
Having proved in~\autoref{static} that the statically computed cost model is
+Having proved in~\autoref{thm:static} that the statically computed cost model is
accurate for the object code, we get as a corollary that it is also accurate
for the source code if the compiler preserves weak traces and
@@ 842,5 +855,5 @@
on the source code only.
\begin{theorem}\label{preservation}
+\begin{theorem}\label{thm:preservation}
Given a compiler that preserves weak traces and propagates measurability,
for all measurable execution fragment $T_1 = s_1 \to^{*} s_1'$ of the source
@@ 852,6 +865,6 @@
\section{Proving the compiler correctness}
\label{simulation}
Because of \autoref{preservation}, to certify a compiler for the labelling
+\label{sec:simulation}
+Because of \autoref{thm:preservation}, to certify a compiler for the labelling
approach we need to both prove that it respects the functional semantics of the
program, and that it preserves weak traces and propagates measurability.
@@ 1373,34 +1386,30 @@
% As should be expected, even though the rules are asymmetric $\approx$ is in fact
% an equivalence relation.

@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@

Therefore we now introduce an abstract notion of relation set between abstract
statuses and an abstract notion of 1tomany forward simulation conditions.
These two definitions enjoy the following remarkable properties:
+%
+This argument enjoys the following remarkable properties:
\begin{enumerate}
 \item they are generic enough to accommodate all passes of the CerCo compiler
 \item the conjunction of the 1tomany forward simulation conditions are
+ \item it is generic enough to accommodate all passes of the CerCo compiler;
+ \item the requested conditions are
just slightly stricter than the statement of a 1tomany forward
 simulation in the classical case. In particular, they only require
 the construction of very simple forms of structured traces made of
 silent states only.
 \item they allow to prove our main result of the paper: the 1tomany
 forward simulation conditions are sufficient to prove the trace
 reconstruction theorem
+ simulation in the classical case;
+% . In particular, they only require
+% the construction of very simple forms of structured traces made of
+% silent states only.
+ \item they allow to prove our main result of the paper: the conditions we will
+ present are sufficient to prove the intensional preservation needed to prove
+ the compiler correct (\autoref{thm:main}).
\end{enumerate}

Point 3. is the important one. First of all it means that we have reduced
the complex problem of trace reconstruction to a much simpler one that,
+The last point is the important one. First of all it means that we have reduced
+the complex problem of preserving the structure of fragments to a much simpler one that,
moreover, can be solved with slight adaptations of the forward simulation proof
that is performed for a compiler that only cares about functional properties.
Therefore we have successfully splitted as much as possible the proof of
+Therefore we have successfully split as much as possible the proof of
preservation of functional properties from that of nonfunctional ones.
@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
+% @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
\paragraph{Relation sets.}
Let $S_1$ and $S_2$ be two deterministic labelled transition systems as described
in \autoref{semantics}. We introduce now the four relations $\mathcal{S,C,R,L}\subseteq S_1\times S_2$
+in \autoref{sec:semantics}. We introduce now the four relations $\mathcal{S,C,R,L}\subseteq S_1\times S_2$
between states of the two systems. The first two are abstract and must be instantiated
by every pass. The remaining two are derived.
@@ 1418,4 +1427,6 @@
% the target code of every cost emitting statement in the source code.
+\begin{definition}[$\R$ and $\LS$]
+\label{def:R_LS}
Two states
$s_1$ and $s_2$ are $\R$related if every time $s_1$ is the
@@ 1423,10 +1434,7 @@
$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally:
$$s_1\R s_2 \iffdef \forall s_1',s_2'.s_1'\C s_2' \to s_1'\ar s_1 \to s_2' \ar s_2.$$
We will require all pairs of states that return from related calls to be
$\R$related. This, in combinantion with a dual requirement on function calls,
will grant that calls return exactly where they are supposed to be.
We say states in $s_1\in S_1$ and $s_2\in S_2$ are labelrelated
(marked $s_1\L s_2$) if
+(marked $s_1\LS s_2$) if
\begin{itemize}
\item they both emit the same label $L$;
@@ 1435,6 +1443,10 @@
$s_1\S s_2'$, otherwise if $L\notin\ell(\Functions)$ then $s_1\S s_2$.
\end{itemize}
This relation captures the fact that synchronisation on labels can be decoupled from
``semantic synchronisation'' (in particular at the start of functions). $s_1\L s_2$
+\end{definition}
+We will require all pairs of states that return from related calls to be
+$\R$related. This, in combinantion with a dual requirement on function calls,
+will grant that calls return exactly where they are supposed to be.
+On the other hand the $\LS$ relation captures the fact that synchronisation on labels can be decoupled from
+``semantic synchronisation'' (in particular at the start of functions). $s_1\LS s_2$
tells that the two state are synchronised as to labels, and $s_2$ will eventually
synchronise semantically using only silent execution steps (apart from the very first
@@ 1443,6 +1455,5 @@
Given the relations $\S$ and $\C$, \autoref{fig:forwardsim} defines a set of
local simulation conditions that are sufficient to grant the correctness of
the compiler.

+the compiler, as stated by the results that follow.
\begin{figure}
\centering
@@ 1550,22 +1561,29 @@
\draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
\end{tikzpicture}
\caption{Local simulation conditions. Each one states that the existence of
states in~XXX such that the dashed relations holds is implied by the assumptions
drawn as solid lines.}
+\caption{Local simulation conditions. Each one states that the assumptions
+ drawn solid imply the existence of the white states and the dashed relations.}
\label{fig:forwardsim}
\end{figure}

\begin{lemma}
+%
+\begin{lemma}[Preservation of structured fragments]
If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
$T_1=s_1\To s_1'$ is a structured fragment not starting with a $\ell(f)$ emission,
and $s_1\S s_2$, then there is $T_2=s_2\To s_2'$ with $T\approx T'$ and $s_1'\S s_2'$.
\end{lemma}
\begin{theorem}
+\begin{theorem}[Preservation of measurable fragments]
+\label{thm:main}
If $S_1$, $S_2$, $\S$ and $\C$ satisfy the diagrams in \autoref{fig:forwardsim},
$M_1:s_1\MeasTo s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that
$s_1\L s_2$, then there is $M_2:s_2\MeasTo s_2'$ with $M_1\approx M_2$. Moreover,
+$M_1 = s_1\to^* s_1'$ is a measurable fragment of $S_1$ and $s_2$ is such that
+$s_1\LS s_2$, then there is a measurable $M_2 = s_2\to^* s_2'$ with $M_1=M_2$. Moreover,
there is a state $s_2''$ with $s_2'\to[\tau *]s_2''$ and $s_1'\S s_2''$.
\end{theorem}
@@@@@@@@@@@@@@@@@@@@@@@
+In particular, the above theorem
+applied to the \verb+main+ function of the program together with an assumption
+stating that initial states are $\LS$related shows that
+for each measurable execution of the source code,
+the compiled code produces a measurable execution with the same observables.
+Combined with \autoref{thm:static} and by proving the conditions in
+\autoref{fig:forwardsim} for every pass, the compiler is proved correct.
+
% \begin{figure}
@@ 1952,91 +1970,4 @@
\end{verbatim}
\end{comment}

\section{Conclusions and future works}
AGGIUNGERE DISCORSO SU APPROCCIO ALTERNATIVO: LABEL DOPO OGNI CALL. COMUNQUE
CON TRACCE STRUTTURATE, MA DIVERSAMENTE
\label{conclusions}
The labelling approach is a technique to implement compilers that induce on
the source code a non uniform cost model determined from the object code
produced. The cost model assigns a cost to each basic block of the program.
The main theorem of the approach says that there is an exact
correspondence between the sequence of basic blocks started in the source
and object code, and that no instruction in the source or object code is
executed outside a basic block. Thus the cost of object code execution
can be computed precisely on the source.

In this paper we scaled the labelling approach to cover a programming language
with function calls. This introduces new difficulties when the language
is unstructured, i.e. it allows function calls to return anywhere in the code,
destroying the hope of a static prediction of the cost of basic blocks.
We restored static predictability by introducing a new semantics for unstructured
programs that single outs well structured executions. The latter are represented
by structured traces, a generalisation of streams of observables that capture
several structural invariants of the execution, like well nesting of functions
or the fact that every basic block must start with a code emission statement.
We showed that structured traces are sufficiently well behaved to statically compute a precise cost model on the object code.

We also proved that the cost model computed on the object code is also valid
on the source code if the compiler respects two requirements: the weak execution
traces of the source and target code must be the same and the object
code execution fragments are structured.

To prove that a compiler respects the requirement we extended the notion
of forward simulation proof for a labelled transition system to grant
preservation of structured fragments. If the source language of the compiler
is structured, all its execution fragments are, allowing to deduce from
preservation of structure that object code fragments are structured too.

Finally, we identified measurable execution fragments that are those whose
execution time (once compiled) can be exactly computed looking at the object
code weak execution traces only. A final instrumentation pass on the source
code can then be used to turn the non functional property of having a certain
cost into the functional property of granting that a certain global variable
incremented at the beginning of every block according to the induced cost model
has a certain value.

All results presented in the paper are part of a larger certification of a
C compiler which is based on the labelling approach. The certification, done
in Matita, is the main deliverable of the FETOpen Certified Complexity (CerCo).

The short term future work consists in the completion of the certification of
the CerCo compiler exploiting the main theorem of this paper.

\paragraph{Related works.}
CerCo is the first project that explicitly tries to induce a
precise cost model on the source code in order to establish nonfunctional
properties of programs on an high level language. Traditional certifications
of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation
of the functional properties.

Usually forward simulations take the following form: for each transition
from $s_1$ to $s_2$ in the source code, there exists an equivalent sequence of
transitions in the target code of length $n$. The number $n$ of transition steps
in the target code can just be the witness of the existential statement.
An equivalent alternative when the proof of simulation is constructive consists
in providing an explicit function, called \emph{clock function} in the
literature~\cite{clockfunctions}, that computes $n$ from $s_1$. Every clock
function constitutes then a cost model for the source code, in the spirit of
what we are doing in CerCo. However, we believe our solution to be superior
in the following respects: 1) the machinery of the labelling approach is
insensible to the resource being measured. Indeed, any cost model computed on
the object code can be lifted to the source code (e.g. stack space used,
energy consumed, etc.) simply reproving an analogue of~\autoref{static}.
For example, in CerCo we transported to the source level not only the execution
time cost model, but also the amount of stack used by function calls.
On the contrary, clock functions only talk about
number of transition steps. In order to extend the approach with clock functions
to other resources, additional functions must be introduced. Moreover, the
additional functions would be handled differently in the proof.
2) the cost models induced by the labelling approach have a simple presentation.
In particular, they associate a number to each basic block. More complex
models can be induced when the approach is scaled to cover, for instance,
loop optimisations~\cite{loopoptimizations}, but the costs are still meant to
be easy to understand and manipulate in an interactive theorem prover or
in FramaC.
On the contrary, a clock function is a complex function of the state $s_1$
which, as a function, is an opaque object that is difficult to reify as
source code in order to reason on it.

\section{The formalisation}
As we already explained, for the sake of presentation we explained the formal
@@ 2050,5 +1981,5 @@
\item Rather than having a generic notion of fragment and a predicate of
structuredness and measurability, we use inductive definitions internalising
 the conditions. Among other things this turns the proof of \autoref{preservation} a matter of
+ the conditions. Among other things this turns the proof of \autoref{thm:preservation} a matter of
structural induction, when it would require more complex induction schemes
otherwise.
@@ 2061,5 +1992,6 @@
with the tradition of labelled transition systems and named sequences of states
and steps \emph{execution fragments}. In the development we named our structures
 \emph{traces}. In the remainder of this section we will use both names.
+ \emph{traces} (that usually refer to the sequence of emitted labels only).
+ In the remainder of this section we will use both names.
\end{itemize}
@@ 2269,4 +2201,25 @@
\paragraph{The forward simulation result.}
+In the formalisation, the equivalent conditions of those
+depicted in \autoref{fig:forwardsim} can be seen in \autoref{fig:forwardsim'}.
+Again we must produce for each pass the relations $\S$ and $\C$. Another derived
+relation is $\L$, which holds for states $s_1$ and $s_2$ when $L~s_1=L~s_2$.
+%
+Some details are skipped in the figure regarding the nature of the repeated steps depicted with
+an asterisk.
+There are three kinds of iterated steps without
+calls nor returns involved in the conditions:
+\begin{itemize}
+ \item sequences where all states strictly after the first one are unlabelled;
+ these are what can be safely prepended to \verb+TAL+'s, and are modelled
+ by the inductive definition \verb+trace_any_any+ (\verb+TAA+) in the formalisation;
+ \item sequences where all ``internal'' states strictly after the first and before the last
+ are unlabelled; these are \verb+trace_any_any_free+ in the formalisation (\verb+TAAF+, which
+ is just a \verb+TAA+ followed by a step);
+ \item sequences where all states strictly before the last are unlabelled that we
+ will call here \verb+trace_any_any_right+ (\verb+TAAR+); in the formalisation
+ these are in fact \verb+TAAF+'s with an additional condition.
+\end{itemize}
+%
\begin{figure}
\centering
@@ 2298,5 +2251,5 @@
% \end{subfigure}
% &
\begin{subfigure}{.25\linewidth}
+\begin{subfigure}[b]{.25\linewidth}
\centering
\begin{tikzpicture}[every join/.style={ar}, join all, thick,
@@ 2317,5 +2270,5 @@
\end{subfigure}
&
\begin{subfigure}{.375\linewidth}
+\begin{subfigure}[b]{.375\linewidth}
\centering
\begin{tikzpicture}[every join/.style={ar}, join all, thick,
@@ 2338,9 +2291,9 @@
\draw [new] (s1) to [bend left] node [rel] {$\C$} (c);
\end{tikzpicture}
\caption{The \verb+cl_call+ case.}
+\caption{The \verb+cl_call+ case.\\\vspace{3.1ex}}
\label{subfig:cl_call}
\end{subfigure}
&
\begin{subfigure}{.375\linewidth}
+\begin{subfigure}[b]{.375\linewidth}
\centering
\begin{tikzpicture}[every join/.style={ar}, join all, thick,
@@ 2362,15 +2315,215 @@
\draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
\end{tikzpicture}
\caption{The \verb+cl_return+ case.}
+\caption{The \verb+cl_return+ case.\\\vspace{3.1ex}}
\label{subfig:cl_return}
\end{subfigure}
\end{tabular}
\caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.
 Dashed lines
 and arrows indicates how the diagrams must be closed when solid relations
 are present.
 DA CAMBIARE: $\L$ va in conflitto con l'altra definizione}
\label{fig:forwardsim}
+\caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.}
+\label{fig:forwardsim'}
\end{figure}
+This prolification of different types of fragments is a downside of shifting
+labelling from steps to states.
+The actual conditions are as follows.
+%
+\begin{condition}[\verb+cl_other+ and \verb+cl_jump+, \autoref{subfig:cl_other_jump}]
+\label{cond:other}
+ For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
+ $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or
+ both $s_1\class\verb+cl_other+$ and $\ell~s_1'$,
+ there exists an $s_2'$ and a $taaf:\verb+trace_any_any_free+~s_2~s_2'$
+ such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
+ $taaf$ is non empty, or one among $s_1$ and $s_1'$ is not labelled.
+ The last condition is needed to prevent the collapsing of two
+ labelemitting consecutive states.
+\end{condition}
+
+% In the above condition depicted in ,
+% a $\verb+trace_any_any_free+~s_1~s_2$ (which from now on
+% will be shorthanded as \verb+TAAF+) is an
+% inductive type of structured traces that do not contain function calls or
+% cost emission statements. Differently from a \verb+TAA+, the
+% instruction to be executed in the lookahead state $s_2$ may be a cost emission
+% statement.
+%
+% The intuition of the condition is that one step can be replaced with zero or more steps if it
+% preserves the relation between the data and if the two final statuses are
+% labelled in the same way. Moreover, we must take special care of the empty case
+% to avoid collapsing two consecutive states that emit a label, missing one of the two emissions.
+%
+\begin{condition}[\verb+cl_call+, \autoref{subfig:cl_call}]
+\label{cond:call}
+ For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and
+ $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a
+$\verb+TAA+~s_2~s_a$, and a
+$\verb+TAAF+~s_b~s_2'$ such that:
+$s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of
+the two call states are the same, $s_1 \C s_a$,
+$s_a\exec s_b$, $s_1' \L s_b$ and
+$s_1' \S s_2'$.
+\end{condition}
+
+% The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a
+% sequence of silent actions before and after the function call itself.
+% The old and new call states must be $\C$related, the old and new
+% states at the beginning of the function execution must be $\L$related
+% and, finally, the two initial and final states must be $\S$related
+% as usual.
+
+\begin{condition}[\verb+cl_return+, \autoref{subfig:cl_return}]
+\label{cond:return}
+ For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$,
+ $s_1\exec s_1'$ and $s_1 \class \verb+cl_return+$, there exists $s_a, s_b, s_2'$, a
+$\verb+TAA+~s_2~s_a$ and a
+$\verb+TAAR+~s_b~s_2'$ such that:
+$s_a\class\verb+cl_return+$,
+$s_a\exec s_b$,
+$s_1' \R s_b$ and
+$s_1' \mathrel{{\S} \cap {\L}} s_2'$.
+\end{condition}
+
+\paragraph{Main result.}
+Let us assume that $\S$ and $\C$ are given such that
+Conditions~\ref{cond:other}, \ref{cond:call} and~\ref{cond:return}
+are satisfied. If we reword the
+relation $\LS$ of \autoref{def:R_LS} by defining
+$$s_1\LS s_2\iffdef s_1\L s_2\wedge \exists s_2', taa:\verb+TAA+~s_2~s_2'. s_1\S s_2',$$
+we can prove the trace reconstruction theorem,
+which is the analogue of \autoref{thm:main}.
+%
+\begin{theorem}[\verb+status_simulation_produce_tlr+]
+\label{thm:main'}
+For every $s_1,s_1',s_2$ s.t.
+$s_1\LS s_2$ and there is a $tlr_1:\verb+TLR+~s_1~s_1'$,
+then there exist $s_2'$ and $tlr_2:\verb+TLR+~s_2~s_2'$
+with $tlr_1=tlr_2$. Moreover there are $s_2''$ and
+a $\verb+TAAR+~s_2'~s_2''$ with $s_2'\mathrel{{\S}\cap{\L}} s_2''$.
+\end{theorem}
+% In particular, the \verb+status_simulation_produce_tlr+ theorem
+% applied to the \verb+main+ function of the program and equal
+% $s_{2_b}$ and $s_2$ states shows that, for every initial state in the
+% source code that induces a structured trace in the source code,
+% the compiled code produces a similar structured trace.
+The theorem states that a \verb+trace_label_return+ in the source code
+together with a precomputed preamble of silent states
+(hidden in the definition of $\LS$) in the target code induces a
+similar \verb+trace_label_return+ in the target code.
+% Note that the statement does not
+% require the produced \verb+trace_label_return+ to start with the
+% precomputed preamble, even if this is likely to be the case in concrete
+% implementations.
+The preamble in input and the postamble in output are necessary for compositionality,
+and follow directly from the the fact that points semantically related
+may not correspond to points where the same observable events are fired, in particular
+cost labels and $RET$'s that mark the borders of measurability.
+
+The proof proceeds by mutual structural induction on the traces involved.
+In the actual formalisation, in place of $tlr_1=tlr_2$ we use a
+recursively defined simulation relation between traces that implies the required
+equality.
+
+\section{Conclusions and future works}
+\label{sec:conclusions}
+The labelling approach is a technique to implement compilers that induce on
+the source code a non uniform cost model determined from the object code
+produced. The cost model assigns a cost to each basic block of the program.
+The main theorem of the approach says that there is an exact
+correspondence between the sequence of basic blocks started in the source
+and object code, and that no instruction in the source or object code is
+executed outside a basic block. Thus the cost of object code execution
+can be computed precisely on the source.
+
+In this paper we scaled the labelling approach to cover a programming language
+with function calls. This introduces new difficulties when the language
+is unstructured, i.e. it allows function calls to return anywhere in the code,
+destroying the hope of a static prediction of the cost of basic blocks.
+We restored static predictability by introducing a new semantics for unstructured
+programs that single outs well structured executions. The latter are represented
+by structured traces, a generalisation of streams of observables that capture
+several structural invariants of the execution, like well nesting of functions
+or the fact that every basic block must start with a code emission statement.
+We showed that structured traces are sufficiently well behaved to statically compute a precise cost model on the object code.
+
+We also proved that the cost model computed on the object code is also valid
+on the source code if the compiler respects two requirements: the weak execution
+traces of the source and target code must be the same and the object
+code execution fragments are structured.
+
+To prove that a compiler respects the requirement we extended the notion
+of forward simulation proof for a labelled transition system to grant
+preservation of structured fragments. If the source language of the compiler
+is structured, all its execution fragments are, allowing to deduce from
+preservation of structure that object code fragments are structured too.
+
+Finally, we identified measurable execution fragments that are those whose
+execution time (once compiled) can be exactly computed looking at the object
+code weak execution traces only. A final instrumentation pass on the source
+code can then be used to turn the non functional property of having a certain
+cost into the functional property of granting that a certain global variable
+incremented at the beginning of every block according to the induced cost model
+has a certain value.
+
+All results presented in the paper are part of a larger certification of a
+C compiler which is based on the labelling approach. The certification, done
+in Matita, is the main deliverable of the FETOpen Certified Complexity (CerCo).
+
+The short term objective consists in the completion of the certification of
+the CerCo compiler exploiting the main theorem of this paper. An alternative approach
+to the same problem that we would like to investigate consists in labelling
+every instruction that follows a call. This would still require a form of structured
+execution fragments, stating that no only calls but also returns are always followed
+by an emission. The main downside is the pollution of the instrumented code
+with many cost annotations.
+
+\paragraph{Related works.}
+CerCo is the first project that explicitly tries to induce a
+precise cost model on the source code in order to establish nonfunctional
+properties of programs on an high level language. Traditional certifications
+of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation
+of the functional properties.
+
+Usually forward simulations take the following form: for each transition
+from $s_1$ to $s_2$ in the source code, there exists an equivalent sequence of
+transitions in the target code of length $n$. The number $n$ of transition steps
+in the target code can just be the witness of the existential statement.
+An equivalent alternative when the proof of simulation is constructive consists
+in providing an explicit function, called \emph{clock function} in the
+literature~\cite{clockfunctions}, that computes $n$ from $s_1$. Every clock
+function constitutes then a cost model for the source code, in the spirit of
+what we are doing in CerCo. However, we believe our solution to be superior
+in the following respects: 1) the machinery of the labelling approach is
+insensible to the resource being measured. Indeed, any cost model computed on
+the object code can be lifted to the source code (e.g. stack space used,
+energy consumed, etc.) simply reproving an analogue of~\autoref{thm:static}.
+For example, in CerCo we transported to the source level not only the execution
+time cost model, but also the amount of stack used by function calls.
+On the contrary, clock functions only talk about
+number of transition steps. In order to extend the approach with clock functions
+to other resources, additional functions must be introduced. Moreover, the
+additional functions would be handled differently in the proof.
+2) the cost models induced by the labelling approach have a simple presentation.
+In particular, they associate a number to each basic block. More complex
+models can be induced when the approach is scaled to cover, for instance,
+loop optimisations~\cite{loopoptimizations}, but the costs are still meant to
+be easy to understand and manipulate in an interactive theorem prover or
+in FramaC.
+On the contrary, a clock function is a complex function of the state $s_1$
+which, as a function, is an opaque object that is difficult to reify as
+source code in order to reason on it.
+
+% e.g.
+% because the 1tomany forward simulation conditions allow in the
+% case of function calls to execute a preamble of silent instructions just after
+% the function call.
+
+% Similarly to the call condition, to simulate a return we can perform a
+% sequence of silent actions before and after the return statement itself,
+% as depicted in \autoref{subfig:cl_return}.
+% The old and the new statements after the return must be $\R$related,
+% to grant that they returned to corresponding calls.
+% The two initial and final states must be $\S$related
+% as usual and, moreover, they must exhibit the same labels. Finally, when
+% the suffix is non empty we must take care of not inserting a new
+% unmatched cost emission statement just after the return statement.
+
% There are three mutual structural recursive functions, one for each of