# Changeset 3366

Ignore:
Timestamp:
Jun 17, 2013, 6:48:16 PM (4 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r3360 \documentclass[bookmarksdepth=2,bookmarksopen]{llncs} \documentclass[bookmarksdepth=2,bookmarksopen,envcountsame]{llncs} \usepackage{hyperref} \usepackage{graphicx} % a built-in 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} \def\R{\mathrel{\mathcal R}} \def\C{\mathrel{\mathcal C}} \def\LS{\mathrel{\mathcal{L_S}}} \def\Labels{\mathbb L} \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 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} 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 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. \subsection{Structured traces} \label{semantics} \label{sec:semantics} Let's consider a generic unstructured language already equipped with a $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 \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)$$ 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 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 \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. % 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 1-to-many 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 1-to-many 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 1-to-many 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 1-to-many 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 non-functional 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. % 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 $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 label-related (marked $s_1\L s_2$) if (marked $s_1\LS s_2$) if \begin{itemize} \item they both emit the same label $L$; $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 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 \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} \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 FET-Open 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 non-functional 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 re-proving 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 Frama-C. 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 \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. 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} \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 % \end{subfigure} % & \begin{subfigure}{.25\linewidth} \begin{subfigure}[b]{.25\linewidth} \centering \begin{tikzpicture}[every join/.style={ar}, join all, thick, \end{subfigure} & \begin{subfigure}{.375\linewidth} \begin{subfigure}[b]{.375\linewidth} \centering \begin{tikzpicture}[every join/.style={ar}, join all, thick, \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, \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 label-emitting 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 FET-Open 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 non-functional 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 re-proving 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 Frama-C. 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 1-to-many 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