\documentclass[bookmarksdepth=2,bookmarksopen,envcountsame]{llncs} \usepackage{hyperref} \usepackage{graphicx} \usepackage{color} \usepackage{listings} \usepackage{bcprules}%\bcprulessavespace \usepackage{verbatim} \usepackage{alltt} \usepackage{subcaption} \usepackage{listings} \usepackage{amssymb,amsmath} % \usepackage{amsmath} \usepackage{multicol} \providecommand{\eqref}[1]{(\ref{#1})} % NB: might be worth removing this if changing class in favour of % a built-in definition. %\newtheorem{theorem}{Theorem} % \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} {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record}, morekeywords={[2]if,then,else,forall,Prop,match,with,end,let}, } \lstdefinelanguage[mine]{C}[ANSI]{C}{ morekeywords={int8_t}, mathescape, escapechar=\% } \newcommand\LSTfont{\tt\fontsize{8}{8.2}\selectfont} \lstset{language=[mine]C,basicstyle=\LSTfont,breaklines=false, % keywordstyle=\color{red}\bfseries, % keywordstyle=[2]\color{blue}, % commentstyle=\color{green}, % stringstyle=\color{blue}, showspaces=false,showstringspaces=false, % xleftmargin=1em } \usepackage{tikz} \usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes} \makeatletter \pgfutil@ifundefined{pgf@arrow@code@implies}{% supply for lack of double arrow special arrow tip if it is not there% \pgfarrowsdeclare{implies}{implies}% {% \pgfarrowsleftextend{2.2pt}% \pgfarrowsrightextend{2.2pt}% }% {% \pgfsetdash{}{0pt} % do not dash% \pgfsetlinewidth{.33pt}% \pgfsetroundjoin % fix join% \pgfsetroundcap % fix cap% \pgfpathmoveto{\pgfpoint{-1.5pt}{2.5pt}}% \pgfpathcurveto{\pgfpoint{-.75pt}{1.5pt}}{\pgfpoint{0.5pt}{.5pt}}{\pgfpoint{2pt}{0pt}}% \pgfpathcurveto{\pgfpoint{0.5pt}{-.5pt}}{\pgfpoint{-.75pt}{-1.5pt}}{\pgfpoint{-1.5pt}{-2.5pt}}% \pgfusepathqstroke% }% }{}% \makeatother \tikzset{state/.style={inner sep = 0, outer sep = 2pt, draw, fill}, every node/.style={inner sep=2pt}, every on chain/.style = {inner sep = 0, outer sep = 2pt}, join all/.style = {every on chain/.append style={join}}, on/.style={on chain={#1}, state}, m/.style={execute at begin node=$, execute at end node=$}, node distance=3mm, is other/.style={circle, minimum size = 3pt, state}, other/.style={on, is other}, is jump/.style={diamond, minimum size = 6pt, state}, jump/.style={on, is jump}, is call/.style={regular polygon, regular polygon sides=3, minimum size=5pt, state}, call/.style={on=going below, is call, node distance=6mm, label=above left:$#1$}, is ret/.style={regular polygon, regular polygon sides=3, minimum size=5pt, shape border rotate=180, state}, ret/.style={on=going above, is ret, node distance=6mm}, chain/.style={start chain=#1 going left}, rev ar/.style={stealth-, thick}, ar/.style={-stealth, thick}, every join/.style={rev ar}, vcenter/.style={baseline={([yshift=-.5ex]current bounding box)}}, every picture/.style={thick}, double equal sign distance/.prefix style={double distance=1.5pt}, %% if already defined (newest version of pgf) it should be ignored%} implies/.style={double, -implies, thin, double equal sign distance, shorten <=5pt, shorten >=5pt}, new/.style={densely dashed}, newn/.style={solid, fill=white}, rel/.style={font=\scriptsize, fill=white, inner sep=2pt}, diag/.style={row sep={11mm,between origins}, column sep={11mm,between origins}, every node/.style={execute at begin node=$, execute at end node=$}, % every node/.style={draw, is other}, }, small vgap/.style={row sep={7mm,between origins}}, small hgap/.style={column sep={7mm,between origins}}, small gap/.style={small vgap, small hgap}, % for article, maybe temporary is jump/.style=is other, is call/.style=is other, is ret/.style=is other, } \def\L{\mathrel{\mathcal L}} \def\S{\mathrel{\mathcal S}} \def\R{\mathrel{\mathcal R}} \def\C{\mathrel{\mathcal C}} \def\LS{\mathrel{\mathcal{L_S}}} \def\Labels{\mathbb L} \def\Functions{\mathbb F} \newsavebox{\execbox} \savebox{\execbox}{\tikz[baseline=-.5ex]\draw [-stealth] (0,0) -- ++(1em, 0);} % \newcommand{\exec}{\ensuremath{\mathrel{\usebox{\execbox}}}} \newcommand{\exec}{\to} \let\ar\triangleright \renewcommand{\verb}{\lstinline[mathescape,basicstyle=\tt\selectfont, identifierstyle=\texttt]} \let\class\colon \let\andalso\quad \newcommand{\append}{\mathbin{@}} \newcommand{\iffdef}{\mathrel{:\Leftrightarrow}} \newcommand{\Deltacost}{\Delta\verb+cost+} \let\oldto\to \makeatletter \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}}} \let\To\implies % \let\MeasTo\rightsquigarrow \makeatother \begin{document} \pagestyle{plain} \title{Certification of the Preservation of Structure by a Compiler's Back-end Pass\thanks{The project CerCo acknowledges the financial support of the Future and Emerging Technologies (FET) programme within the Seventh Framework Programme for Research of the European Commission, under FET-Open grant number: 243881}} \author{Paolo Tranquilli \and Claudio Sacerdoti Coen} \institute{Department of Computer Science and Engineering, University of Bologna,\\\email{Paolo.Tranquilli@unibo.it}, \email{Claudio.SacerdotiCoen@unibo.it}} \maketitle \begin{abstract} The labelling approach is a technique to lift cost models for non-functional properties of programs from the object code to the source code. It is based on the preservation of the structure of the high level program in every intermediate language used by the compiler. Such structure is captured by observables that are added to the semantics and that needs to be preserved by the forward simulation proof of correctness of the compiler. Additional special observables are required for function calls. In this paper we present a generic forward simulation proof that preserves all these observables. The proof statement is based on a new mechanised semantics that traces the structure of execution when the language is unstructured. The generic semantics and simulation proof have been mechanised in the interactive theorem prover Matita. \end{abstract} \section{Introduction} The \emph{labelling approach} has been introduced in~\cite{easylabelling} as a technique to \emph{lift} cost models for non-functional properties of programs from the object code to the source code. Examples of non-functional properties are execution time, amount of stack/heap space consumed and energy required for communication. The basic premise of the approach is that it is impossible to provide a \emph{uniform} cost model for an high level language that is preserved \emph{precisely} by a compiler. For instance, two instances of an assignment $x = y$ in the source code can be compiled very differently according to the place (registers vs stack) where $x$ and $y$ are stored at the moment of execution. Therefore a precise cost model must assign a different cost to every occurrence, and the exact cost can only be known after compilation. According to the labelling approach, the compiler is free to compile and optimise the source code without any major restriction, but it must keep trace of what happens to basic blocks during the compilation. The cost model is then computed on the object code. It assigns a cost to every basic block. Finally, the compiler propagates back the cost model to the source level, assigning a cost to each basic block of the source code. Implementing the labelling approach in a certified compiler allows to reason formally on the high level source code of a program to prove non-functional properties that are granted to be preserved by the compiler itself. The trusted code base is then reduced to 1) the interactive theorem prover (or its kernel) used in the certification of the compiler and 2) the software used to certify the property on the source language, that can be itself certified further reducing the trusted code base. In~\cite{easylabelling} the authors provide an example of a simple certified compiler that implements the labelling approach for the imperative \verb+While+ language~\cite{while}, that does not have pointers and function calls. The labelling approach has been shown to scale to more interesting scenarios. In particular in~\cite{functionallabelling} it has been applied to a functional language and in~\cite{loopoptimizations} it has been shown that the approach can be slightly complicated to handle loop optimisations and, more generally, program optimisations that do not preserve the structure of basic blocks. On-going work also shows that the labelling approach is also compatible with the complex analyses required to obtain a cost model for object code on processors that implement advanced features like pipelining, superscalar architectures and caches. In the European Project CerCo (Certified Complexity\footnote{\url{http://cerco.cs.unibo.it}})~\cite{cerco} we are certifying a labelling approach based compiler for a large subset of C to 8051 object code. The compiler is moderately optimising and implements a compilation chain that is largely inspired to that of CompCert~\cite{compcert1,compcert2}. Compared to work done in~\cite{easylabelling}, the main novelty and source of difficulties is due to the presence of function calls. Surprisingly, the addition of function calls require a revisitation of the proof technique given in~\cite{easylabelling}. In particular, at the core of the labelling approach there is a forward simulation proof that, in the case of \verb+While+, is only minimally more complex than the proof required for the preservation of the functional properties only. In the case of a programming language with function calls, instead, it turns out that the forward simulation proof for the back-end languages, which are unstructured, must grant a whole new set of invariants. In this paper we present a formalisation in the Matita interactive theorem prover~\cite{matita1,matita2} of a generic version of the simulation proof required for unstructured languages. All back-end languages of the CerCo compiler are unstructured languages, so the proof covers half of the correctness of the compiler. The statement of the generic proof is based on a new semantics for imperative unstructured languages that is based on \emph{structured execution fragments} and that restores the preservation of structure in the observables of the semantics. The generic proof allows to almost completely split the part of the simulation that deals with functional properties only from the part that deals with the preservation of structure. The plan of this paper is the following. In Section~\ref{sec:labelling} we summarise the labelling method. In Section~\ref{extension} we scale the method to unstructured languages with function calls. In Section~\ref{sec:simulation} we give the necessary condition for the correctness of the compiler (forward simulation proof). Section~\ref{sec:formalization} sketches the formalisation of the datastructures and proofs in Matita. Conclusions and future works are in Section~\ref{sec:conclusions} \section{The labelling approach} \label{sec:labelling} % \subsection{A brief introduction to the labelling approach} We briefly explain the labelling approach as introduced in~\cite{easylabelling} on the example in \autoref{examplewhile}. The user wants to analyse the execution time of the program (the black lines in \autoref{subfig:example_input}). He compiles the program using a special compiler that first inserts in the code three label emission statements (\verb+EMIT $L_i$+) to mark the beginning of basic blocks (\autoref{subfig:example_input}); then the compiler compiles the code to machine code (\autoref{subfig:example_oc}), granting that the execution of the source and object code emits the same sequence of labels ($L_1; L_2; L_2; L_3$ in the example). This is achieved by keeping track of basic blocks during compilation, avoiding all optimisations that alter the control flow. The latter can be recovered with a more refined version of the labelling approach~\cite{loopoptimizations}, but in the present paper we stick to this simple variant for simplicity. Once the object code is produced, the compiler runs a static code analyser to associate to each label $L_1, \ldots, L_3$ the cost (in clock cycles) of the instructions that belong to the corresponding basic block. For example, the cost $k_1$ associated to $L_1$ is the number of cycles required to execute the block $I_3$ and \verb+COND $l_2$+, while the cost $k_2$ associated to $L_2$ counts the cycles required by the block $I_4$, \verb+GOTO $l_1$+ and \verb+COND $l_2$+. The compiler also guarantees that every executed instruction is in the scope of some code emission label, that each scope does not contain loops (to associate a finite cost), and that both branches of a conditional statement are followed by a code emission statement. Under these assumptions it is true that the total execution cost of the program $\Delta_t$ is equal to the sum over the sequence of emitted labels of the cost associated to every label: $\Delta_t = k(L_1; L_2; L_2; L_3) = k_1 + k_2 + k_2 + k_3$. Finally, the compiler emits an instrumented version of the source code (\autoref{subfig:example_instrument}) where label emission statements are replaced by increments of a global variable \verb+cost+ that, before every increment, holds the exact number of clock cycles spent by the microprocessor so far: the difference $\Deltacost$ between the final and initial value of the internal clock is $\Deltacost = k_1 + k_2 + k_2 + k_3 = \Delta_t$. Finally, the user can employ any available method (e.g. Hoare logic, invariant generators, abstract interpretation and automated provers) to certify that $\Deltacost$ never exceeds a certain bound~\cite{cerco}, which is now a functional property of the code. \vspace{-0.5cm} \begin{figure}[!h] \begin{subfigure}[t]{.32\linewidth} \begin{lstlisting}[moredelim={[is][\color{red}]{|}{|}}] |EMIT $L_1$;| $I_1$; for (i=0; i<2; i++) { |EMIT $L_2$;| $I_2$; } |EMIT $L_3$;| \end{lstlisting} \caption{The input program (black lines) with its labelling (red lines).} \label{subfig:example_input} \end{subfigure} \hfill \begin{subfigure}[t]{.23\linewidth} \begin{lstlisting} EMIT $L_1$ $I_3$ $l_1$:$\!$ COND $l_2$ EMIT $L_2$ $I_4$ GOTO $l_1$ $l_2$:$\!$ EMIT $L_3$ \end{lstlisting} \caption{The output labelled object code.} \label{subfig:example_oc} \end{subfigure} \hfill \begin{subfigure}[t]{.32\linewidth} \begin{lstlisting} cost += $k_1$; $I_1$; for (i=0; i<2; i++) { cost += $k_2$; $I_2$; } cost += $k_3$; \end{lstlisting} \caption{The output instrumented code.} \label{subfig:example_instrument} \end{subfigure} % \begin{verbatim} % EMIT L_1; EMIT L_1 cost += k_1; % I_1; I_3 I_1; % for (i=0; i<2; i++) { l_1: COND l_2 for (i=0; i<2; i++) { % EMIT L_2; EMIT L_2 cost += k_2; % I_2; I_4 I_2; % } GOTO l_1 } % EMIT L_3; l_2: EMIT L_3 cost += k_3; % \end{verbatim} \caption{The labelling approach applied to a simple program.\label{examplewhile}. The $I_i$ are sequences of instructions not containing jumps or loops. } \end{figure} \section{Extending the labelling approach to function calls} \label{extension} % Let's now consider a simple program written in C that contains a function pointer call inside the scope of the cost label $L_1$, in \autoref{subfig:call_input}. The labelling method works exactly as before, inserting code emission statements/\verb+cost+ variable increments at the beginning of every basic block and at the beginning of every function. The compiler still grants that the sequence of labels observed on the two programs are the same. A new difficulty appears when the compiler needs to statically analyse the object code to assign a cost to every label. What should the scope of the $L_1$ label be? After executing the $I_4$ block, the \verb+CALL+ statement passes control to a function that cannot be determined statically. Therefore the cost of executing the body must be paid by some other label (hence the requirement that every function starts with a code emission statement). What label should pay for the cost for the block $I_5$? The only reasonable answer is $L_1$, i.e. \emph{the scope of labels should extend to the next label emission statement or the end of the function, stepping over function calls}. % \begin{figure} {}\hfill \begin{subfigure}[t]{.45\linewidth} \centering \begin{lstlisting}[xleftmargin=20pt] void main() { EMIT $L_1$; $I_1$; (*f)(); $I_2$; } void g() { EMIT $L_2$; $I_3$; } \end{lstlisting} \caption{The input labelled C program.} \label{subfig:call_input} \end{subfigure} \hfill \begin{subfigure}[t]{.45\linewidth} \centering \begin{lstlisting}[xleftmargin=20pt] main: EMIT $L_1$ $I_4$ CALL $I_5$ RETURN g: EMIT $L_2$ $I_6$ RETURN \end{lstlisting} \caption{The output labelled object code.} \label{subfig:call_output} \end{subfigure} \hfill{} \caption{An example compilation of a simple program with a function pointer call.} \label{subfig:call_example} \end{figure} The latter definition of scope is adequate on the source level because C is a structured language that guarantees that every function call, if it returns, passes control to the first instruction that follows the call. However, this is not guaranteed for object code, the backend languages of a compiler and, more generally, for unstructured languages that use a writable control stack to store the return address of calls. For example, $I_6$ could increment by $1$ the return address on the stack so that the next \verb+RETURN+ would start at the second instruction of $I_5$. The compiler would still be perfectly correct if a random, dead code instruction was added after the \verb+CALL+ as the first instruction of $I_5$. More generally, \emph{there is no guarantee that a correct compiler that respects the functional behaviour of a program also respects the calling structure of the source code}. Without such an assumption, however, it may not be true that the execution cost of the program is the sum of the costs associated to the labels emitted. In our example, the cost of $I_5$ is paid by $L_1$, but in place of $I_5$ the processor could execute any other code after $g$ returns. Obviously, any reasonably written compiler produces object code that behaves as if the language was structured (i.e. by properly nesting function calls/returns and without tampering with the return addresses on the control 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{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 by our compiler are of that type. We call them \emph{structured} since their main property is to respect properties that hold for free on the source code because of structure. Moreover, in order to avoid proving too many preservation properties of our compiler, we drop the original requirements on the object code (all instructions must be in scope of some labels, no loops inside a scope, etc.) in favour of the corresponding requirement for structured runs (a structured run must start with a label emission, no instruction can be executed twice between two emissions, etc.). We will therefore proceed as follows. In the following section 1) we formally introduce the notion of structured execution fragment, which captures structured runs in the style of labelled transition systems; 2) we show that on the object code we can correctly compute the execution time of a structured run from the sequence of labels observed; 3) we show that on the source code we can correctly compute the execution time of a program if the compiler produces object code whose runs are weakly similar to the source code runs and structured. 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{sec:simulation} we present a refinement of forward simulation that grants all required correctness properties. All the definitions and theorems presented in the paper have been formalised in the interactive theorem prover Matita and are being used to certify the complexity preserving compiler developed in the CerCo project~\cite{cerco}. The formalisation heavily relies on algebraic and dependent types. In the first part of the paper we did not try to stay close to the formalisation. On the contrary, the definitions given in the paper are the result of a significant simplification effort for the sake of presentation and to make easier the re-implementation of the concepts in a proof assistant which is not based on the Calculus of Inductive Constructions. In any case the formalisation, briefly presented at the end of the paper, is heavily commented to allow the reader to understand the technical details of the formalisation. % @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ % % We briefly sketch here a simplified version of the labelling approach as % introduced in~\cite{easylabelling}. The simplification strengthens the % sufficient conditions given in~\cite{easylabelling} to allow a simpler % explanation. The simplified conditions given here are also used in the % CerCo compiler to simplify the proof. % % Let $\mathcal{P}$ be a programming language whose semantics is given in % terms of observables: a run of a program yields a finite or infinite % stream of observables. We also assume for the time being that function % calls are not available in $\mathcal{P}$. We want to associate a cost % model to a program $P$ written in $\mathcal{P}$. The first step is to % extend the syntax of $\mathcal{P}$ with a new construct $\verb+emit L+$ % where $L$ is a label distinct from all observables of $\mathcal{P}$. % The semantics of $\verb+emit L+$ is the emission of the observable % \verb+L+ that is meant to signal the beginning of a basic block. % % There exists an automatic procedure that injects into the program $P$ an % $\verb+emit L+$ at the beginning of each basic block, using a fresh % \verb+L+ for each block. In particular, the bodies of loops, both branches % of \verb+if-then-else+s and the targets of \verb+goto+s must all start % with an emission statement. % % Let now $C$ be a compiler from $\mathcal{P}$ to the object code $\mathcal{M}$, % that is organised in passes. Let $\mathcal{Q}_i$ be the $i$-th intermediate % language used by the compiler. We can easily extend every % intermediate language (and its semantics) with an $\verb+emit L+$ statement % as we did for $\mathcal{P}$. The same is possible for $\mathcal{M}$ too, with % the additional difficulty that the syntax of object code is given as a % sequence of bytes. The injection of an emission statement in the object code % can be done using a map that maps two consecutive code addresses with the % statement. The intended semantics is that, if $(pc_1,pc_2) \mapsto \verb+emit L+$ then the observable \verb+L+ is emitted after the execution of the % instruction stored at $pc_1$ and before the execution of the instruction % stored at $pc_2$. The two program counters are necessary because the % instruction stored at $pc_1$ can have multiple possible successors (e.g. % in case of a conditional branch or an indirect call). Dually, the instruction % stored at $pc_2$ can have multiple possible predecessors (e.g. if it is the % target of a jump). % % The compiler, to be functionally correct, must preserve the observational % equivalence, i.e. executing the program after each compiler pass should % yield the same stream of observables. After the injection of emission % statements, observables now capture both functional and non-functional % behaviours. % This correctness property is called in the literature a forward simulation % and is sufficient for correctness when the target language is % deterministic~\cite{compcert3}. % We also require a stronger, non-functional preservation property: after each % pass all basic blocks must start with an emission statement, and all labels % \verb+L+ must be unique. % % Now let $M$ be the object code obtained for the program $P$. Let us suppose % that we can statically inspect the code $M$ and associate to each basic block % a cost (e.g. the number of clock cycles required to execute all instructions % in the basic block, or an upper bound to that time). Every basic block is % labelled with an unique label \verb+L+, thus we can actually associate the % cost to \verb+L+. Let call it $k(\verb+L+)$. % % The function $k$ is defined as the cost model for the object code control % blocks. It can be equally used as well as the cost model for the source % control blocks. Indeed, if the semantics of $P$ is the stream % $L_1 L_2 \ldots$, then, because of forward simulation, the semantics of $M$ is % also $L_1 L_2 \ldots$ and its actual execution cost is $\Sigma_i k(L_i)$ because % every instruction belongs to a control block and every control block is % labelled. Thus it is correct to say that the execution cost of $P$ is also % $\Sigma_i k(L_i)$. In other words, we have obtained a cost model $k$ for % the blocks of the high level program $P$ that is preserved by compilation. % % How can the user profit from the high level cost model? Suppose, for instance, % that he wants to prove that the WCET of his program is bounded by $c$. It % is sufficient for him to prove that $\Sigma_i k(L_i) \leq c$, which is now % a purely functional property of the code. He can therefore use any technique % available to certify functional properties of the source code. % What is suggested in~\cite{easylabelling} is to actually instrument the % source code $P$ by replacing every label emission statement % $\verb+emit L+$ with the instruction $\verb+cost += k(L)+$ that increments % a global fresh variable \verb+cost+. The bound is now proved by establishing % the program invariant $\verb+cost+ \leq c$, which can be done for example % using the Frama-C~\cite{framaC} suite if the source code is some variant of % C. % % In order to extend the labelling approach to function calls we make % \verb+CALL f+ emit the observable \verb+f+ and \verb+RET+ emit a distinguished observable % \verb+ret+. % % For example the following execution history of the program in \autoref{fig:esempio} % $$I_1; \verb+CALL f+; \verb+COND l+; \verb+EMIT $L_2$+; I_3; \verb+RET+; I_2; \verb+RET+$$ % emits the trace % $$\verb+main+, \verb+f+$$ % \begin{figure} % \hfil % \begin{minipage}{.2\linewidth} % \begin{lstlisting} % main: $\!I_1$ % CALL f % $I_2$ % RET % \end{lstlisting} % \end{minipage} % \begin{minipage}{.1\linewidth} % \begin{lstlisting} % main % main % main % main % \end{lstlisting} % \end{minipage} % \hfil % \begin{minipage}{.2\linewidth} % \begin{lstlisting} % f: $\!$COND l % EMIT $L_2$ % RET % l: $\!$EMIT $L_3$ % $I_3$ % RET % \end{lstlisting} % \end{minipage} % \begin{minipage}{.1\linewidth} % \begin{lstlisting} % f % % $L_2$ % % $L_3$ % $L_3$ % \end{lstlisting} % \end{minipage} % \hfil{} % \caption{} % \label{fig:esempio} % \end{figure} % % % \subsection{Labelling function calls} % We now want to extend the labelling approach to support function calls. % On the high level, \emph{structured} programming language $\mathcal{P}$ there % is not much to change. % When a function is invoked, the current basic block is temporarily exited % and the basic block the function starts with take control. When the function % returns, the execution of the original basic block is resumed. Thus the only % significant change is that basic blocks can now be nested. Let \verb+E+ % be the label of the external block and \verb+I+ the label of a nested one. % Since the external starts before the internal, the semantics observed will be % \verb+E I+ and the cost associated to it on the source language will be % $k(\verb+E+) + k(\verb+I+)$, i.e. the cost of executing all instructions % in the block \verb+E+ first plus the cost of executing all the instructions in % the block \verb+I+. However, we know that some instructions in \verb+E+ are % executed after the last instruction in \verb+I+. This is actually irrelevant % because we are here assuming that costs are additive, so that we can freely % permute them\footnote{The additivity assumption fails on modern processors that have stateful subsystems, like caches and pipelines. The extension of the labelling approach to those systems is therefore non trivial and under development in the CerCo project.}. Note that, in the present discussion, we are assuming that % the function call terminates and yields back control to the basic block % \verb+E+. If the call diverges, the instrumentation % $\verb+cost += k(E)+$ executed at the beginning of \verb+E+ is still valid, % but just as an upper bound to the real execution cost: only precision is lost. % % Let now consider what happens when we move down the compilation chain to an % unstructured intermediate or final language. Here unstructured means that % the only control operators are conditional and unconditional jumps, function % calls and returns. Unlike a structured language, though, there is no guarantee % that a function will return control just after the function call point. % The semantics of the return statement, indeed, consists in fetching the % return address from some internal structure (typically the control stack) and % jumping directly to it. The code can freely manipulate the control stack to % make the procedure returns to whatever position. Indeed, it is also possible % to break the well nesting of function calls/returns. % % Is it the case that the code produced by a correct compiler must respect the % additional property that every function returns just after its function call % point? The answer is negative and the property is not implied by forward % simulation proofs. For instance, imagine to modify a correct compiler pass % by systematically adding one to the return address on the stack and by % putting a \verb+NOP+ (or any other instruction that takes one byte) after % every function call. The obtained code will be functionally indistinguishable, % and the added instructions will all be dead code. % % This lack of structure in the semantics badly interferes with the labelling % approach. The reason is the following: when a basic block labelled with % \verb+E+ contains a function call, it no longer makes any sense to associate % to a label \verb+E+ the sum of the costs of all the instructions in the block. % Indeed, there is no guarantee that the function will return into the block and % that the instructions that will be executed after the return will be the ones % we are paying for in the cost model. % % How can we make the labelling approach work in this scenario? We only see two % possible ways. The first one consists in injecting an emission statement after % every function call: basic blocks no longer contain function calls, but are now % terminated by them. This completely solves the problem and allows the compiler % to break the structure of function calls/returns at will. However, the % technique has several drawbacks. First of all, it greatly augments the number % of cost labels that are injected in the source code and that become % instrumentation statements. Thus, when reasoning on the source code to prove % non-functional properties, the user (or the automation tool) will have to handle % larger expressions. Second, the more labels are emitted, the more difficult it % becomes to implement powerful optimisations respecting the code structure. % Indeed, function calls are usually implemented in such a way that most registers % are preserved by the call, so that the static analysis of the block is not % interrupted by the call and an optimisation can involve both the code before % and after the function call. Third, instrumenting the source code may require % unpleasant modification of it. Take, for example, the code % \verb+f(g(x));+. We need to inject an emission statement/instrumentation % instruction just after the execution of \verb+g+. The only way to do that % is to rewrite the code as \verb+y = g(x); emit L; f(y);+ for some fresh % variable \verb+y+. It is pretty clear how in certain situations the obtained % code would be more obfuscated and then more difficult to manually reason on. % % For the previous reasons, in this paper and in the CerCo project we adopt a % different approach. We do not inject emission statements after every % function call. However, we want to propagate a strong additional invariant in % the forward simulation proof. The invariant is the propagation of the structure % of the original high level code, even if the target language is unstructured. % The structure we want to propagate, that will become more clear in the next % section, comprises 1) the property that every function should return just after % the function call point, which in turns imply well nesting of function calls; % 2) the property that every basic block starts with a code emission statement. % % In the original labelling approach of~\cite{easylabelling}, the second property % was granted syntactically as a property of the generated code. % In our revised approach, instead, we will impose the property on the runs: % it will be possible to generate code that does not respect the syntactic % property, as soon as all possible runs respect it. For instance, dead code will no longer % be required to have all basic blocks correctly la. The switch is suggested % from the fact that the first of the two properties --- that related to % function calls/returns --- can only be defined as property of runs, % not of the static code. The switch is % beneficial to the proof because the original proof was made of two parts: % the forward simulation proof and the proof that the static property was granted. % In our revised approach the latter disappears and only the forward simulation % is kept. % % In order to capture the structure semantics so that it is preserved % by a forward simulation argument, we need to make the structure observable % in the semantics. This is the topic of the next section. \subsection{Structured execution fragments} \label{sec:semantics} Let's consider a generic unstructured language already equipped with a small step structured operational semantics (SOS). We introduce a deterministic labelled transition system $(S,\Lambda,\to)$ that refines the SOS by observing function calls/returns and the beginning of basic blocks. $S$ is the set of states of the program and $\Lambda = \{ \tau, RET \} \cup \Labels \cup \Functions$ where $\Functions$ is the set of names of functions that can occur in the program, $\Labels$ is a set of labels disjoint from $\Functions$ and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$. Moreover there is an injective function $\ell : \Functions \to \Labels$ that tells the starting label of the body of each function, and $\ell(\Functions)\subseteq \Labels$ denotes the image of this function. The transition function is defined as $s_1 \to[o] s_2$ if $s_1$ moves to $s_2$ according to the SOS and $o = f \in \Functions$ if the function $f$ is called, $o = RET$ if a \verb+RETURN+ is executed, $o = L \in \Labels$ if an \verb+EMIT $L$+ is executed to signal the beginning of a basic block, and $o = \tau$ in all other cases. Because we assume the language to be deterministic, the label emitted can actually be computed simply observing $s_1$. Finally, $S$ is also endowed with a relation $s\ar s'$ ($s'$ \emph{follows} $s$) that holds when the instruction to be executed in $s'$ follows syntactically the one in $s$ in the source program. In the rest of the paper we write $s_0 \to^{*} s_n$ for the finite execution fragment $T = s_0 \to[o_0] s_1 \to[o_1] \ldots \to[o_{n-1}] s_n$ and, we call \emph{weak trace} of $T$ (denoted as $|T|$) the subsequence $o_{i_0} \ldots o_{i_m}$ of $o_0 \ldots o_{n-1}$ obtained dropping every internal action $\tau$. %Let $k$ be a cost model for observables actions that maps elements of %$\Lambda \setminus \{\tau\}$ to any commutative cost monoid %(e.g. natural numbers). We extend the domain of $k$ to executable fragments %by posing $k(T) = \Sigma_{o \in |T|} k(o)$. \paragraph{Structured execution fragments} Among all possible finite execution fragments we want to identify the ones that satisfy the requirements we sketched in the previous section. We say that an execution fragment $s_0 \to^{*} s_n$ is \emph{structured} (and we denote it as $s_0 \To s_n$) iff the following conditions are met. \begin{enumerate} \item For every $i$, if $s_i \to[f] s_{i+1}$ then there is a label $L$ and a $k\ge i+2$ such that $s_{i+1} \to[\ell(f)] s_{i+2} \To s_k \to[RET] s_{k+1}$, with $s_i \ar s_{k+1}$. In other words, $s_{i+1}$ must start execution with \verb+EMIT $\ell(f)$+ --- so that no instruction falls outside the scope of every label --- and then continue with a structured fragment returning control to the instruction immediately following the call. The condition also enforces convergence of every function call, which is necessary to bound the cost of the fragment. Note that non convergent programs may still have structured execution fragments that are worth measuring. For example, we can measure the reaction time of a server implemented as an unbounded loop whose body waits for an input, process it and performs an output before looping: the processing steps form a structured fragment. \item The number of $RET$'s in the fragment is equal to the number of calls performed. In combination with the previous condition, this ensures well-bracketing of function calls. \item \label{req3} For every $i$ and $f$, if $s_{i+1}\to[\ell(f)]s_{i+2}$ then $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{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 \verb+EMIT $L$+. This captures the requirement that every branch which is live code must start with a label emission. Otherwise, it would be possible to have conditional instructions whose branches are assigned different costs, making impossible to assign a single cost to the label whose scope contains the jump. \end{enumerate} One might wonder why $f$ and $\ell(f)$, that always appear in this order, are not collapsed into a single observable. This would simplify some aspects of the formalisation at the price of others. For example, we should add special cases when the fragment starts at the beginning of a function body (e.g. the one of \texttt{main}) because in that case nobody would have emitted the observable $\ell(f)$. We plan to compare the two approaches in the future. \paragraph{Measurable execution fragments and their cost prediction.} The first main theorem of CerCo deals with the object code. It states that the execution cost of certain execution fragments, that we call \emph{measurable fragments}, can be computed from their weak trace by choosing the cost model $k$ that assigns to any label the cost (in clock cycles) of the instructions in its scope, and $0$ to function calls and $RET$ observables. \begin{theorem} \label{thm:static} for all measurable fragment $M = s_0 \to^{*} s_n$,\\ $$\Delta_t := \verb+clock+_{s_n} - \verb+clock+_{s_0} = \Sigma_{o \in |M|} k(o)$$ \end{theorem} An execution fragment $s_0 \to^{*} s_n$ is measurable if it is structured (up to a possible final \texttt{RETURN}) and if it does not start or end in the middle of a basic block. Ending in the middle of a block would mean that the last label encountered would have pre-paid more instructions than the ones executed; starting in the middle would mean not paying any instruction up to the first label emission. Formally, $s_0 \to^{*} s_n$ is measurable iff $o_0 \in \Labels$ (or equivalently in $s_0$ the program must emit a label) and either $s_0 \To s_{n-1}$ and $s_{n-1}\to[RET]s_n$ or $s_0 \To s_n$ and $s_n$ must be a label emission statement. %\textbf{CSC: PROVA----------------------} % The theorem is proved by structural induction over the structured % trace, and is based on the invariant that % iff the function that computes the cost model has analysed the instruction % to be executed at $s_2$ after the one to be executed at $s_1$, and if % the structured trace starts with $s_1$, then eventually it will contain also % $s_2$. When $s_1$ is not a function call, the result holds trivially because % of the $s_1\exec s_2$ condition obtained by inversion on % the trace. The only non % trivial case is the one of function calls: the cost model computation function % does recursion on the first instruction that follows that function call; the % \verb+as_after_return+ condition of the \verb+tal_base_call+ and % \verb+tal_step_call+ grants exactly that the execution will eventually reach % this state. \paragraph{Weak similarity and cost invariance.} Given two deterministic unstructured programming languages with their own operational semantics, we say that two execution fragments are \emph{weakly trace equivalent} if their weak traces are equal. A compiler (pass) that preserves the program semantics also \emph{preserves weak traces and propagates measurability} iff for every measurable fragment $M_1 = s_1 \to^{*} s_1'$ of the source code, the corresponding execution fragment $M_2 = s_2 \to^{*} s_2'$ of the object code is measurable and $M_1$ and $M_2$ are weakly trace equivalent. The very intuitive notion of ``corresponding fragment'' is made clear in the forward simulation proof of preservation of the semantics of the program by saying that $s_2$ and $s_1$ are in a certain relation. Clearly the property holds for a compiler if it holds for each compiler pass. 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 propagates measurability. Thus, as prescribed by the CerCo's methodology~\cite{fopara}, it becomes possible to compute cost models on the object code, transfer it to the source code and then reason comfortably on the source code only. \begin{theorem}\label{thm:preservation} Given a compiler that preserves weak traces and propagates measurability, for all measurable execution fragment $M_1 = s_1 \to^{*} s_1'$ of the source code such that $M_2 = s_2 \to^{*} s_2'$ is the corresponding fragment of the object code, $$\Delta_t := \verb+clock+_{s_2'} - \verb+clock+_{s_2} = \Sigma_{o \in |M_2|} k(o) = \Sigma_{o \in |M_1|} k(o)$$ \end{theorem} \section{Proving the compiler correctness} \label{sec:simulation} Because of \autoref{thm:preservation}, to certify a compiler for the labelling approach we need to prove that it respects the functional semantics of the program, preserves weak traces and propagates measurability. We achieve this by proving the three properties independently for each compiler pass. The first property is standard and can be proved by means of a forward simulation argument (see for example~\cite{compcert3}) that runs like this. First a relation between the corresponding source and target states is defined. Then a lemma establishes a local simulation condition: given two states in relation, if the source one performs one step then the target one performs zero or more steps and the two resulting states are synchronised again according to the relation. No requirements are imposed on the intermediate target states. Finally, the lemma is iterated over the execution fragment to establish the final result. In principle, preservation of weak traces could be easily shown with the same argument (and also at the same time). Surprisingly, propagation of measurability cannot. What makes the standard forward simulation proof work is the fact that usually a compiler pass performs some kind of local or global analysis of the code followed by a compositional, order preserving translation of every instruction. In order to produce structured traces, however, code emission cannot be fully compositional any longer, and requirements need to be enforced on intermediate target states too. For example, consider~requirement \ref{req3} that asks every function body to start with a label emission statement. Some compiler passes must add preambles to functions, for example to take care of the parameter passing convention. In order to not violate the requirement, the preamble must be inserted after the label emission. In the forward simulation proof, however, function call steps in the source language are simulated by the new function call followed by the execution of the preamble, and only at the end of the preamble the reached states are again in the expected relation. In the meantime, however, the object code has already performed the label emission statement, that still needs to be executed in the source code, breaking forward simulation. Another reason why the standard argument breaks is due to the requirement that function calls should yield back control after the calling point. Some passes need to translate a function call to a function call followed by some instructions (for example to restore caller-saved registers in the pass that sets the parameter convention). In the forward simulation proof, these instructions are taken care of when simulating the \texttt{RETURN} step: the state just after the return in the source code is matched by the state $s_2$ after these steps in the object code. However, the aforementioned requirement does not involve $s_2$, but the intermediate state reached after the return in the object code. Therefore this requirement too cannot be enforced with the standard forward simulation argument. In this section we present now a modified forward simulation argument that can be used to prove at once that a compiler preserves the semantics of the program, its weak traces and that the compiler propagates measurability. % @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ % % The program semantics adopted in the traditional labelling approach is based % on labelled deductive systems. Given a set of observables $\mathcal{O}$ and % a set of states $\S$, the semantics of one deterministic execution % step is % defined as a function $S \to S \times O^*$ where $O^*$ is a (finite) stream of % observables. The semantics is then lifted compositionally to multiple (finite % or infinite) execution steps. % Finally, the semantics of a a whole program execution is obtained by forgetting % about the final state (if any), yielding a function $S \to O^*$ that given an % initial status returns the finite or infinite stream of observables in output. % % We present here a new definition of semantics where the structure of execution, % as defined in the previous section, is now observable. The idea is to replace % the stream of observables with a structured data type that makes explicit % function call and returns and that grants some additional invariants by % construction. The data structure, called \emph{structured traces}, is % defined inductively for terminating programs and coinductively for diverging % ones. In the paper we focus only on the inductive structure, i.e. we assume % that all programs that are given a semantics are total. The Matita formalisation % also shows the coinductive definitions. The semantics of a program is then % defined as a function that maps an initial state into a structured trace. % % In order to have a definition that works on multiple intermediate languages, % we abstract the type of structure traces over an abstract data type of % abstract statuses, which we aptly call $\verb+abstract_status+$. The fields % of this record are the following. % \begin{itemize} % \item \verb+S : Type[0]+, the type of states. % \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate stating % an execution step. We write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$. % \item \verb+as_classifier : S $\to$ classification+, a function tagging all % states with a class in % $\{\verb+cl_return,cl_jump,cl_call,cl_other+\}$, depending on the instruction % that is about to be executed (we omit tail-calls for simplicity). We will % use $s \class c$ as a shorthand for both $\verb+as_classifier+~s=c$ % (if $c$ is a classification) and $\verb+as_classifier+~s\in c$ % (if $c$ is a set of classifications). % \item \verb+as_label : S $\to$ option label+, telling whether the % next instruction to be executed in $s$ is a cost emission statement, % and if yes returning the associated cost label. Our shorthand for this function % will be $\ell$, and we will also abuse the notation by using $\ell~s$ as a % predicate stating that $s$ is labelled. % \item \verb+as_call_ident : ($\Sigma$s:S. s $\class$ cl_call) $\to$ label+, % telling the identifier of the function which is being called in a % \verb+cl_call+ state. We will use the shorthand $s\uparrow f$ for % $\verb+as_call_ident+~s = f$. % \item \verb+as_after_return : ($\Sigma$s:S. s $\class$ cl_call) $\to$ S $\to$ Prop+, % which holds on the \verb+cl_call+ state $s_1$ and a state $s_2$ when the % instruction to be executed in $s_2$ follows the function call to be % executed in (the witness of the $\Sigma$-type) $s_1$. We will use the notation % $s_1\ar s_2$ for this relation. % \end{itemize} % % % \begin{alltt} % % record abstract_status := \{ S: Type[0]; % % as_execute: S \(\to\) S \(\to\) Prop; as_classifier: S \(\to\) classification; % % as_label: S \(\to\) option label; as_called: (\(\Sigma\)s:S. c s = cl_call) \(\to\) label; % % as_after_return: (\(\Sigma\)s:S. c s = cl_call) \(\to\) S \(\to\) Prop \} % % \end{alltt} % % The inductive type for structured traces is actually made by three multiple % inductive types with the following semantics: % \begin{enumerate} % \item $(\verb+trace_label_return+~s_1~s_2)$ (shorthand $\verb+TLR+~s_1~s_2$) % is a trace that begins in % the state $s_1$ (included) and ends just before the state $s_2$ (excluded) % such that the instruction to be executed in $s_1$ is a label emission % statement and the one to be executed in the state before $s_2$ is a return % statement. Thus $s_2$ is the state after the return. The trace % may contain other label emission statements. It captures the structure of % the execution of function bodies: they must start with a cost emission % statement and must end with a return; they are obtained by concatenating % one or more basic blocks, all starting with a label emission % (e.g. in case of loops). % \item $(\verb+trace_any_label+~b~s_1~s_2)$ (shorthand $\verb+TAL+~b~s_1~s_2$) % is a trace that begins in % the state $s_1$ (included) and ends just before the state $s_2$ (excluded) % such that the instruction to be executed in $s_2$/in the state before % $s_2$ is either a label emission statement or % or a return, according to the boolean $b$. It must not contain % any label emission statement. It captures the notion of a suffix of a % basic block. % \item $(\verb+trace_label_label+~b~s_1~s_2)$ (shorthand $\verb+TLL+~b~s_1~s_2$ is the special case of % $\verb+TAL+~b~s_1~s_2)$ such that the instruction to be % executed in $s_1$ is a label emission statement. It captures the notion of % a basic block. % \end{enumerate} % % \begin{multicols}{3} % \infrule[\verb+tlr_base+] % {\verb+TLL+~true~s_1~s_2} % {\verb+TLR+~s_1~s_2} % % \infrule[\verb+tlr_step+] % {\verb+TLL+~false~s_1~s_2 \andalso % \verb+TLR+~s_2~s_3 % } % {\verb+TLR+~s_1~s_3} % % \infrule[\verb+tll_base+] % {\verb+TAL+~b~s_1~s_2 \andalso % \ell~s_1 % } % {\verb+TLL+~b~s_1~s_2} % \end{multicols} % % \infrule[\verb+tal_base_not_return+] % {s_1\exec s_2 \andalso % s_1\class\{\verb+cl_jump+, \verb+cl_other+\}\andalso % \ell~s_2 % } % {\verb+TAL+~false~s_1~s_2} % % \infrule[\verb+tal_base_return+] % {s_1\exec s_2 \andalso % s_1 \class \verb+cl_return+ % } % {\verb+TAL+~true~s_1~s_2} % % \infrule[\verb+tal_base_call+] % {s_1\exec s_2 \andalso % s_1 \class \verb+cl_call+ \andalso % s_1\ar s_3 \andalso % \verb+TLR+~s_2~s_3 \andalso % \ell~s_3 % } % {\verb+TAL+~false~s_1~s_3} % % \infrule[\verb+tal_step_call+] % {s_1\exec s_2 \andalso % s_1 \class \verb+cl_call+ \andalso % s_1\ar s_3 \andalso % \verb+TLR+~s_2~s_3 \andalso % \verb+TAL+~b~s_3~s_4 % } % {\verb+TAL+~b~s_1~s_4} % % \infrule[\verb+tal_step_default+] % {s_1\exec s_2 \andalso % \lnot \ell~s_2 \andalso % \verb+TAL+~b~s_2~s_3\andalso % s_1 \class \verb+cl_other+ % } % {\verb+TAL+~b~s_1~s_3} % \begin{comment} % \begin{verbatim} % inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝ % | tlr_base: % ∀status_before: S. % ∀status_after: S. % trace_label_label S ends_with_ret status_before status_after → % trace_label_return S status_before status_after % | tlr_step: % ∀status_initial: S. % ∀status_labelled: S. % ∀status_final: S. % trace_label_label S doesnt_end_with_ret status_initial status_labelled → % trace_label_return S status_labelled status_final → % trace_label_return S status_initial status_final % with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝ % | tll_base: % ∀ends_flag: trace_ends_with_ret. % ∀start_status: S. % ∀end_status: S. % trace_any_label S ends_flag start_status end_status → % as_costed S start_status → % trace_label_label S ends_flag start_status end_status % with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝ % (* Single steps within a function which reach a label. % Note that this is the only case applicable for a jump. *) % | tal_base_not_return: % ∀start_status: S. % ∀final_status: S. % as_execute S start_status final_status → % (as_classifier S start_status cl_jump ∨ % as_classifier S start_status cl_other) → % as_costed S final_status → % trace_any_label S doesnt_end_with_ret start_status final_status % | tal_base_return: % ∀start_status: S. % ∀final_status: S. % as_execute S start_status final_status → % as_classifier S start_status cl_return → % trace_any_label S ends_with_ret start_status final_status % (* A call followed by a label on return. *) % | tal_base_call: % ∀status_pre_fun_call: S. % ∀status_start_fun_call: S. % ∀status_final: S. % as_execute S status_pre_fun_call status_start_fun_call → % ∀H:as_classifier S status_pre_fun_call cl_call. % as_after_return S «status_pre_fun_call, H» status_final → % trace_label_return S status_start_fun_call status_final → % as_costed S status_final → % trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final % (* A call followed by a non-empty trace. *) % | tal_step_call: % ∀end_flag: trace_ends_with_ret. % ∀status_pre_fun_call: S. % ∀status_start_fun_call: S. % ∀status_after_fun_call: S. % ∀status_final: S. % as_execute S status_pre_fun_call status_start_fun_call → % ∀H:as_classifier S status_pre_fun_call cl_call. % as_after_return S «status_pre_fun_call, H» status_after_fun_call → % trace_label_return S status_start_fun_call status_after_fun_call → % ¬ as_costed S status_after_fun_call → % trace_any_label S end_flag status_after_fun_call status_final → % trace_any_label S end_flag status_pre_fun_call status_final % | tal_step_default: % ∀end_flag: trace_ends_with_ret. % ∀status_pre: S. % ∀status_init: S. % ∀status_end: S. % as_execute S status_pre status_init → % trace_any_label S end_flag status_init status_end → % as_classifier S status_pre cl_other → % ¬ (as_costed S status_init) → % trace_any_label S end_flag status_pre status_end. % \end{verbatim} % \end{comment} % A \verb+trace_label_return+ is isomorphic to a list of % \verb+trace_label_label+s that ends with a cost emission followed by a % return terminated \verb+trace_label_label+. % The interesting cases are those of $\verb+trace_any_label+~b~s_1~s_2$. % A \verb+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 % impose several invariants that are meant to impose a structure to the % otherwise unstructured execution. In particular, the following invariants are % imposed: % \begin{enumerate} % \item the trace is never empty; it ends with a return iff $b$ is % 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 % is always the beginning of a new basic block; as such it must start % with a cost emission statement % \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 of a subtrace for the % function body of type % $\verb+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 % the function call. The status $s_2$ is the one that follows the return % statement. The next instruction of $s_2$ must follow the function call % instruction. As a consequence, function calls are also well nested. % \end{enumerate} % % There are three mutual structural recursive functions, one for each of % \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation % $|\,.\,|$: the \emph{flattening} of the traces. These functions % allow to extract from a structured trace the list of emitted cost labels. % % We only show here the type of one % % of them: % % \begin{alltt} % % flatten_trace_label_return: % % \(\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{Structured traces similarity and cost prediction invariance.} % % A compiler pass maps source to object code and initial states to initial % states. The source code and initial state uniquely determine the structured % trace of a program, if it exists. The structured trace fails to exists iff % the structural conditions are violated by the program execution (e.g. a function % body does not start with a cost emission statement). Let us assume that the % target structured trace exists. % % What is the relation between the source and target structured traces? % In general, the two traces can be arbitrarily different. However, we are % interested only in those compiler passes that maps a trace $\tau_1$ to a trace % $\tau_2$ such that % \begin{equation}|\tau_1| = |\tau_2|.\label{th2}\end{equation} % The reason is that the combination of~\eqref{th1} with~\eqref{th2} yields the % corollary % \begin{equation}\label{th3} % \forall s_1,s_2. \forall \tau: \verb+TLR+~s_1~s_2.~ % \verb+clock+~s_2 - \verb+clock+~s_1 = % \Sigma_{\alpha \in |\tau_1|}\;k(\alpha) = % \Sigma_{\alpha \in |\tau_2|}\;k(\alpha). % \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~\eqref{th2}. % Therefore we introduce here a similarity relation between traces with % the same structure. Theorem~\verb+tlr_rel_to_traces_same_flatten+ % in the Matita formalisation shows that~\eqref{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 \verb+as_costed+ and that are classified as \verb+cl_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 % subtraces to concatenation of subtraces of the same length and starting with % the same emission statement, etc. % % In the formalisation 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 the inference rules shown in \autoref{fig:txx_rel} % for the sake of readability. We also omit from trace constructors all arguments, % but those that are traces or that % are used in the premises of the rules. By abuse of notation we denote all three % relations by infixing $\approx$. % % \begin{figure} % \begin{multicols}{2} % \infrule % {tll_1\approx tll_2 % } % {\verb+tlr_base+~tll_1 \approx \verb+tlr_base+~tll_2} % % \infrule % {tll_1 \approx tll_2 \andalso % tlr_1 \approx tlr_2 % } % {\verb+tlr_step+~tll_1~tlr_1 \approx \verb+tlr_step+~tll_2~tlr_2} % \end{multicols} % \vspace{3ex} % \begin{multicols}{2} % \infrule % {\ell~s_1 = \ell~s_2 \andalso % tal_1\approx tal_2 % } % {\verb+tll_base+~s_1~tal_1 \approx \verb+tll_base+~s_2~tal_2} % % \infrule % {tal_1\approx tal_2 % } % {\verb+tal_step_default+~tal_1 \approx tal_2} % \end{multicols} % \vspace{3ex} % \infrule % {} % {\verb+tal_base_not_return+\approx taa \append \verb+tal_base_not_return+} % \vspace{1ex} % \infrule % {} % {\verb+tal_base_return+\approx taa \append \verb+tal_base_return+} % \vspace{1ex} % \infrule % {tlr_1\approx tlr_2 \andalso % s_1 \uparrow f \andalso s_2\uparrow f % } % {\verb+tal_base_call+~s_1~tlr_1\approx taa \append \verb+tal_base_call+~s_2~tlr_2} % \vspace{1ex} % \infrule % {tlr_1\approx tlr_2 \andalso % s_1 \uparrow f \andalso s_2\uparrow f \andalso % \verb+tal_collapsable+~tal_2 % } % {\verb+tal_base_call+~s_1~tlr_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2)} % \vspace{1ex} % \infrule % {tlr_1\approx tlr_2 \andalso % s_1 \uparrow f \andalso s_2\uparrow f \andalso % \verb+tal_collapsable+~tal_1 % } % {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_base_call+~s_2~tlr_2)} % \vspace{1ex} % \infrule % {tlr_1 \approx tlr_2 \andalso % s_1 \uparrow f \andalso s_2\uparrow f\andalso % tal_1 \approx tal_2 \andalso % } % {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2} % \caption{The inference rule for the relation $\approx$.} % \label{fig:txx_rel} % \end{figure} % % % \begin{comment} % \begin{verbatim} % let rec tlr_rel S1 st1 st1' S2 st2 st2' % (tlr1 : trace_label_return S1 st1 st1') % (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝ % match tlr1 with % [ tlr_base st1 st1' tll1 ⇒ % match tlr2 with % [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2 % | _ ⇒ False % ] % | tlr_step st1 st1' st1'' tll1 tl1 ⇒ % match tlr2 with % [ tlr_step st2 st2' st2'' tll2 tl2 ⇒ % tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2 % | _ ⇒ False % ] % ] % and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2' % (tll1 : trace_label_label S1 fl1 st1 st1') % (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝ % match tll1 with % [ tll_base fl1 st1 st1' tal1 H ⇒ % match tll2 with % [ tll_base fl2 st2 st2 tal2 G ⇒ % as_label_safe … («?, H») = as_label_safe … («?, G») ∧ % tal_rel … tal1 tal2 % ] % ] % and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' % (tal1 : trace_any_label S1 fl1 st1 st1') % (tal2 : trace_any_label S2 fl2 st2 st2') % on tal1 : Prop ≝ % match tal1 with % [ tal_base_not_return st1 st1' _ _ _ ⇒ % fl2 = doesnt_end_with_ret ∧ % ∃st2mid,taa,H,G,K. % tal2 ≃ taa_append_tal ? st2 ??? taa % (tal_base_not_return ? st2mid st2' H G K) % | tal_base_return st1 st1' _ _ ⇒ % fl2 = ends_with_ret ∧ % ∃st2mid,taa,H,G. % tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa % (tal_base_return ? st2mid st2' H G) % | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ % fl2 = doesnt_end_with_ret ∧ % ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧ % ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. % (* we must allow a tal_base_call to be similar to a call followed % by a collapsable trace (trace_any_any followed by a base_not_return; % we cannot use trace_any_any as it disallows labels in the end as soon % as it is non-empty) *) % (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. % tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨ % ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. % ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'. % tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧ % tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2 % | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ % ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧ % ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. % (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. % tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧ % tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨ % ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. % ∃tl2 : trace_any_label ? fl2 st2mid'' st2'. % tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧ % tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2 % | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ % tal_rel … tl1 tal2 (* <- this makes it many to many *) % ]. % \end{verbatim} % \end{comment} % % % In the preceding rules, a $taa$ is an inhabitant of the % $\verb+trace_any_any+~s_1~s_2$ (shorthand $\verb+TAA+~s_1~s_2$), % an 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 \verb+TAL+'s that do not contain % any function call. Therefore it % is possible to concatenate (using ``$\append$'') a \verb+TAA+ to the % left of a \verb+TAL+. A \verb+TAA+ captures % a sequence of silent moves. % The \verb+tal_collapsable+ unary predicate over \verb+TAL+'s % holds when the argument does not contain any function call and it ends % with a label (not a return). The intuition is that after a function call we % can still perform a sequence of silent actions while remaining similar. % % As should be expected, even though the rules are asymmetric $\approx$ is in fact % an equivalence relation. % This argument enjoys the following remarkable properties: \begin{enumerate} \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 conditions we will present are sufficient to prove the intensional preservation needed to prove the compiler correct (\autoref{thm:main}). \end{enumerate} 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 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{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 $\S$ relation between states is the classical relation used in forward simulation proofs. It correlates the data of the states (e.g. registers, memory, etc.). The $\C$ relation correlates states that are about to execute calls. It allows to track the position in the target code of every call in the source code. % The $\L$ relation simply says that the two states are both label % emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$. % It allows to track the position in % 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 successor of a call state $s_1'$ that is $\C$-related to a call state $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 say states in $s_1\in S_1$ and $s_2\in S_2$ are label-related (marked $s_1\LS s_2$) if \begin{itemize} \item they both emit the same label $L$; \item if $L\in \ell(\Functions)$ then there is a state $s_2'$ such that $s_2\to[L]\to[\tau *]s_2'$ with $s_1\S s_2'$, otherwise if $L\notin\ell(\Functions)$ then $s_1\S s_2$. \end{itemize} \end{definition} We will require all pairs of states that return from related calls to be $\R$-related. This, in combination 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 emit). 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, as stated by the results that follow. \begin{figure} \centering % \begin{subfigure}{.475\linewidth} % \centering % \begin{tikzpicture}[every join/.style={ar}, join all, thick, % every label/.style=overlay, node distance=10mm] % \matrix [diag] (m) {% % \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\ % \node (s2) {}; & \node (t2) {}; \\ % }; % \node [above=0 of t1, overlay] {$\alpha$}; % {[-stealth] % \draw (s1) -- (t1); % \draw [new] (s2) -- node [above] {$*$} (t2); % } % \draw (s1) to node [rel] {$\S$} (s2); % \draw [new] (t1) to node [rel] {$\S,\L$} (t2); % \end{tikzpicture} % \caption{The \verb+cl_jump+ case.} % \label{subfig:cl_jump} % \end{subfigure} % & \centering \tikzset{diag/.append style= {every node/.append style={is other, text height=0,text depth=0,text width=0, text opacity=0} }, } \begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}] \matrix [diag] (m) {% \node (s1) {s_1}; & \node (t1) {s_1'};\\ \node (s2) {s_2}; & \node [newn] (t2) {s_2'}; \\ }; {[-stealth] \draw (s1) -- node [above] {$\tau$} (t1); \draw [new] (s2) -- node [above] {$\tau *$} (t2); } \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2); \end{tikzpicture} \qquad \begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}] \matrix [diag] (m) {% \node (s1) {s_1}; & \node (t1) {s_1'};\\ \node (s2) {s_2}; & \node [newn](mid) {s_a}; & \node [newn] (t2) {s_2'}; \\ }; {[-stealth] \draw (s1) -- node [above] {$L$} (t1); \draw [new] (s2) -- node [above] {$L$} (mid); \draw [new] (mid) -- node [above] {$\tau *$} (t2); } \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (t2); \end{tikzpicture} \text{ if $L\notin\ell(\Functions)$} \qquad \begin{tikzpicture}[baseline={([yshift=-.5ex]s2)}] \matrix [diag] (m) {% \node (s1) {s_1}; & \node (t1) {s_1'};\\ \node (s2) {s_2};\\ }; {[-stealth] \draw (s1) -- node [above] {$\ell(f)$} (t1); } \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S$} (s2); \end{tikzpicture} \\[10pt] \begin{tikzpicture} \matrix [diag, small vgap] (m) {% &\node (t1) {s_1'}; \\ \node (s1) {s_1}; \\ && \node [newn] (l1) {s_b}; & \node [newn] (l2) {s_c}; & \node [newn] (t2) {s_2'};\\ \node [newn] (s2) {s_2}; & \node [newn] (c) {s_a};\\ }; {[-stealth] \draw (s1) -- node [above left] {$f$} (t1); \draw [new] (s2) -- node [above] {$\tau *$} (c); \draw [new] (c) -- node [above left] {$f$} (l1); \draw [new] (l1) -- node [above] {$\ell(f)$} (l2); \draw [new] (l2) -- node [above] {$\tau *$} (t2); } \draw (s1) to [bend right] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); \draw [new] (s1) to [bend left] node [rel] {$\C$} (c); \end{tikzpicture} \qquad\qquad \begin{tikzpicture} \matrix [diag, small vgap] (m) {% \node (s1) {s_1}; \\ &\node (t1) {s_1'}; \\ \node (s2) {s_2}; & \node [newn] (c) {s_a};\\ && \node [newn] (r) {s_b}; & \node [newn] (t2) {s_2'}; \\ }; {[-stealth] \draw (s1) -- node [above right] {$RET$} (t1); \draw [new] (s2) -- node [above] {$\tau *$} (c); \draw [new] (c) -- node [below left] {$RET$} (r); \draw [new] (r) -- node [above] {$\tau *$} (t2); } \draw (s1) to [bend right] node [rel] {$\S$} (s2); \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S$} (t2); \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r); \end{tikzpicture} \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}[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}[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\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} % \centering % \begin{tabular}{@{}c@{}c@{}c@{}} % % \begin{subfigure}{.475\linewidth} % % \centering % % \begin{tikzpicture}[every join/.style={ar}, join all, thick, % % every label/.style=overlay, node distance=10mm] % % \matrix [diag] (m) {% % % \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\ % % \node (s2) {}; & \node (t2) {}; \\ % % }; % % \node [above=0 of t1, overlay] {$\alpha$}; % % {[-stealth] % % \draw (s1) -- (t1); % % \draw [new] (s2) -- node [above] {$*$} (t2); % % } % % \draw (s1) to node [rel] {$\S$} (s2); % % \draw [new] (t1) to node [rel] {$\S,\L$} (t2); % % \end{tikzpicture} % % \caption{The \verb+cl_jump+ case.} % % \label{subfig:cl_jump} % % \end{subfigure} % % & % \begin{subfigure}{.25\linewidth} % \centering % \begin{tikzpicture}[every join/.style={ar}, join all, thick, % every label/.style=overlay, node distance=10mm] % \matrix [diag] (m) {% % \node (s1) {}; & \node (t1) {};\\ % \node (s2) {}; & \node (t2) {}; \\ % }; % {[-stealth] % \draw (s1) -- (t1); % \draw [new] (s2) -- node [above] {$*$} (t2); % } % \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); % \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2); % \end{tikzpicture} % \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.} % \label{subfig:cl_other_jump} % \end{subfigure} % & % \begin{subfigure}{.375\linewidth} % \centering % \begin{tikzpicture}[every join/.style={ar}, join all, thick, % every label/.style=overlay, node distance=10mm] % \matrix [diag, small gap] (m) {% % &\node (t1) {}; \\ % \node (s1) [is call] {}; \\ % && \node (l) {}; & \node (t2) {};\\ % \node (s2) {}; & \node (c) [is call] {};\\ % }; % {[-stealth] % \draw (s1) -- node [above left] {$f$} (t1); % \draw [new] (s2) -- node [above] {$*$} (c); % \draw [new] (c) -- node [below right] {$f$} (l); % \draw [new] (l) -- node [above] {$*$} (t2); % } % \draw (s1) to [bend right] node [rel] {$\S$} (s2); % \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); % \draw [new] (t1) to [bend left] node [rel] {$\L$} (l); % \draw [new] (t1) to [bend right] node [rel] {$\C$} (c); % \end{tikzpicture} % \caption{The \verb+cl_call+ case.} % \label{subfig:cl_call} % \end{subfigure} % & % \begin{subfigure}{.375\linewidth} % \centering % \begin{tikzpicture}[every join/.style={ar}, join all, thick, % every label/.style=overlay, node distance=10mm] % \matrix [diag, small gap] (m) {% % \node (s1) [is ret] {}; \\ % &\node (t1) {}; \\ % \node (s2) {}; & \node (c) [is ret] {};\\ % && \node (r) {}; & \node (t2) {}; \\ % }; % {[-stealth] % \draw (s1) -- node [above right] {$RET$} (t1); % \draw [new] (s2) -- node [above] {$*$} (c); % \draw [new] (c) -- node [below left] {$RET$} (r); % \draw [new] (r) -- node [above] {$*$} (t2); % } % \draw (s1) to [bend right] node [rel] {$\S$} (s2); % \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2); % \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r); % \end{tikzpicture} % \caption{The \verb+cl_return+ case.} % \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.} % \label{fig:forwardsim} % \end{figure} % \paragraph{1-to-many forward simulation conditions.} % \begin{condition}[Cases \verb+cl_other+ and \verb+cl_jump+] % 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 $\verb+trace_any_any_free+~s_2~s_2'$ called $taaf$ % 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 \verb+as_costed+. % \end{condition} % % In the above condition depicted in \autoref{subfig:cl_other_jump}, % 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}[Case \verb+cl_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}[Case \verb+cl_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$, a % $\verb+TAAF+~s_b~s_2'$ called $taaf$ 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'$ and either % $taaf$ is non empty, or $\lnot \ell~s_a$. % \end{condition} % % 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. % % \begin{comment} % \begin{verbatim} % definition status_simulation ≝ % λS1 : abstract_status. % λS2 : abstract_status. % λsim_status_rel : status_rel S1 S2. % ∀st1,st1',st2.as_execute S1 st1 st1' → % sim_status_rel st1 st2 → % match as_classify … st1 with % [ None ⇒ True % | Some cl ⇒ % match cl with % [ cl_call ⇒ ∀prf. % (* % st1' ------------S----------\ % ↑ \ \ % st1 \--L--\ \ % | \ \ \ % S \-C-\ st2_after_call →taa→ st2' % | \ ↑ % st2 →taa→ st2_pre_call % *) % ∃st2_pre_call. % as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ % call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ % ∃st2_after_call,st2'. % ∃taa2 : trace_any_any … st2 st2_pre_call. % ∃taa2' : trace_any_any … st2_after_call st2'. % as_execute … st2_pre_call st2_after_call ∧ % sim_status_rel st1' st2' ∧ % label_rel … st1' st2_after_call % | cl_return ⇒ % (* % st1 % / ↓ % | st1'----------S,L------------\ % S \ \ % \ \-----R-------\ | % \ | | % st2 →taa→ st2_ret | | % ↓ / | % st2_after_ret →taaf→ st2' % % we also ask that st2_after_ret be not labelled if the taaf tail is % not empty % *) % ∃st2_ret,st2_after_ret,st2'. % ∃taa2 : trace_any_any … st2 st2_ret. % ∃taa2' : trace_any_any_free … st2_after_ret st2'. % (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ % as_classifier … st2_ret cl_return ∧ % as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ % ret_rel … sim_status_rel st1' st2_after_ret ∧ % label_rel … st1' st2' % | cl_other ⇒ % (* % st1 → st1' % | \ % S S,L % | \ % st2 →taaf→ st2' % % the taaf can be empty (e.g. tunnelling) but we ask it must not be the % case when both st1 and st1' are labelled (we would be able to collapse % labels otherwise) % *) % ∃st2'. % ∃taa2 : trace_any_any_free … st2 st2'. % (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ % sim_status_rel st1' st2' ∧ % label_rel … st1' st2' % | cl_jump ⇒ % (* just like cl_other, but with a hypothesis more *) % as_costed … st1' → % ∃st2'. % ∃taa2 : trace_any_any_free … st2 st2'. % (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ % sim_status_rel st1' st2' ∧ % label_rel … st1' st2' % ] % ]. % \end{verbatim} % \end{comment} % \paragraph{Main result: the 1-to-many forward simulation conditions % are sufficient to trace reconstruction} % % Let us assume that a relation set is given such that the 1-to-many % forward simulation conditions are satisfied. Under this assumption we % can prove the following three trace reconstruction theorems by mutual % structural induction over the traces given in input between the % $s_1$ and $s_1'$ states. % % 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. % % \begin{theorem}[\verb+status_simulation_produce_tlr+] % For every $s_1,s_1',s_{2_b},s_2$ s.t. % there is a $\verb+TLR+~s_1~s_1'$ called $tlr_1$ and a % $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and % $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t. % there is a $\verb+TLR+~s_{2_b}~s_{2_m}$ called $tlr_2$ and % there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$ % s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$, % and $tlr_1\approx tlr_2$ % and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and % $s_1' \R s_{2_m}$. % \end{theorem} % % The theorem states that a \verb+trace_label_return+ in the source code % together with a precomputed preamble of silent states % (the \verb+TAA+) in the target code induces a % similar \verb+trace_label_return+ in the target code which can be % followed by a sequence of silent states. 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 is necessary for compositionality, 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. % % Clearly similar results are also available for the other two types of structured % traces (in fact, they are all proved simultaneously by mutual induction). % \begin{theorem}[\verb+status_simulation_produce_tll+] % For every $s_1,s_1',s_{2_b},s_2$ s.t. % there is a $\verb+TLL+~b~s_1~s_1'$ called $tll_1$ and a % $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and % $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t. % \begin{itemize} % \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ % and a trace $\verb+TLL+~b~s_{2_b}~s_{2_m}$ called $tll_2$ % and a $\verb+TAAF+~s_{2_m}~s_2'$ called $taa_2$ s.t. % $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and % $s_1' \R s_{2_m}$ and % $tll_1\approx tll_2$ and % if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$; % \item else there exists $s_2'$ and a % $\verb+TLL+~b~s_{2_b}~s_2'$ called $tll_2$ such that % $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and % $tll_1\approx tll_2$. % \end{itemize} % \end{theorem} % % The statement is similar to the previous one: a source % \verb+trace_label_label+ and a given target preamble of silent states % in the target code induce a similar \verb+trace_label_label+ in the % target code, possibly followed by a sequence of silent moves that become the % preamble for the next \verb+trace_label_label+ translation. % % \begin{theorem}[\verb+status_simulation_produce_tal+] % For every $s_1,s_1',s_2$ s.t. % there is a $\verb+TAL+~b~s_1~s_1'$ called $tal_1$ and % $s_1 \S s_2$ % \begin{itemize} % \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$ % and a trace $\verb+TAL+~b~s_2~s_{2_m}$ called $tal_2$ and a % $\verb+TAAF+~s_{2_m}~s_2'$ called $taa_2$ s.t. % $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and % $s_1' \R s_{2_m}$ and % $tal_1 \approx tal_2$ and % if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$; % \item else there exists $s_2'$ and a % $\verb+TAL+~b~s_2~s_2'$ called $tal_2$ such that % either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and % $tal_1\approx tal_2$ % or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and % $\verb+tal_collapsable+~tal_1$ and $\lnot \ell~s_1$. % \end{itemize} % \end{theorem} % % The statement is also similar to the previous ones, but for the lack of % the target code preamble. \begin{comment} \begin{corollary} For every $s_1,s_1',s_2$ s.t. there is a $\verb+trace_label_return+~s_1~s_1'$ called $tlr_1$ and $s_1 (\L \cap \S) s_2$ there exists $s_{2_m},s_2'$ s.t. there is a $\verb+trace_label_return+~s_2~s_{2_m}$ called $tlr_2$ and there is a $\verb+trace_any_any_free+~s_{2_m}~s_2'$ called $taaf$ s.t. if $taaf$ is non empty then $\lnot (\verb+as_costed+~s_{2_m})$, and $\verb+tlr_rel+~tlr_1~tlr_2$ and $s_1' (\S \cap \L) s_2'$ and $s_1' \R s_{2_m}$. \end{corollary} \end{comment} \begin{comment} \begin{verbatim} status_simulation_produce_tlr S1 S2 R (* we start from this situation st1 →→→→tlr→→→→ st1' | \ L \---S--\ | \ st2_lab →taa→ st2 (the taa preamble is in general either empty or given by the preceding call) and we produce st1 →→→→tlr→→→→ st1' \\ / \ // R \-L,S-\ \\ | \ st2_lab →tlr→ st2_mid →taaf→ st2' *) st1 st1' st2_lab st2 (tlr1 : trace_label_return S1 st1 st1') (taa2_pre : trace_any_any S2 st2_lab st2) (sim_execute : status_simulation S1 S2 R) on tlr1 : R st1 st2 → label_rel … st1 st2_lab → ∃st2_mid.∃st2'. ∃tlr2 : trace_label_return S2 st2_lab st2_mid. ∃taa2 : trace_any_any_free … st2_mid st2'. (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧ R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧ tlr_rel … tlr1 tlr2 \end{verbatim} \end{comment} \section{The formalisation} \label{sec:formalization} As we already explained, for the sake of presentation we presented the formal content of our results departing from the actual Matita formalisation. In this section we explain the basis of the Matita development, heavily based on inductive definitions and dependent types. The development consists of 3369 lines of code and can be downloaded from \begin{center}\url{http://cerco.cs.unibo.it/attachment/wiki/WikiStart/CPP2013.tar.gz}\end{center} \paragraph*{The main differences.} The main points where the development diverges from the material presented in the previous sections are the following. \begin{itemize} \item Rather than having a generic notion of fragment and predicates of structuredness and measurability, we use inductive definitions and dependent types to provide data types that satisfy the conditions by construction. Among other things this turns the proof of \autoref{thm:preservation} into a matter of structural induction, when it would require additional lemmas otherwise. \item As we are dealing with a deterministic labelling transition system, we purposely blur the distinction between labelling the transitions and labelling the states originating them, and opt in general for the latter in the actual definitions. \item As object code cannot have a separate emission instruction, we allow any instruction to be labelled, which implies that labels can be emitted alongside other observable events. \item A small difference lies in the naming conventions. In this paper we went 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} (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 main definitions.} The notion of deterministic labelled transition system is captured in the development via the abstract data type called $\verb+abstract_status+$. The fields of this record are the following. \begin{itemize} \item \verb+S : Type[0]+, the type of states. \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate modelling the execution. As in the previous sections, we write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$. \item \verb+as_classifier : S $\to$ classification+, a function tagging all states with a class in $\{$\verb+cl_return,cl_jump,cl_call,cl_other+$\}$, depending on the instruction that is about to be executed (we omit tail-calls for simplicity). We will use $s \class c$ as a shorthand for both $\verb+as_classifier+~s=c$ (if $c$ is a classification) and $\verb+as_classifier+~s\in c$ (if $c$ is a set of classifications). This partly replaces the labelling of execution steps. \item \verb+as_label : S $\to$ option label+, telling whether the next instruction to be executed in $s$ is a cost emission statement, and if yes returning the associated cost label. Our shorthand for this function will be $L$, and we will also abuse the notation by using $L~s$ as a predicate stating that $s$ is labelled. \item \verb+as_call_ident : ($\Sigma$s:S. s $\class$ cl_call) $\to$ label+, telling the identifier of the function which is being called in a \verb+cl_call+ state. We will use the shorthand $s\uparrow f$ for $\verb+as_call_ident+~s = f$. \item \verb+as_after_return : ($\Sigma$s:S. s $\class$ cl_call) $\to$ S $\to$ Prop+, which holds on the \verb+cl_call+ state $s_1$ and a state $s_2$ when the instruction to be executed in $s_2$ follows the function call to be executed in (the witness of the $\Sigma$-type) $s_1$, i.e. when $s_1\ar s_2$. \end{itemize} % % % \begin{alltt} % % record abstract_status := \{ S: Type[0]; % % as_execute: S \(\to\) S \(\to\) Prop; as_classifier: S \(\to\) classification; % % as_label: S \(\to\) option label; as_called: (\(\Sigma\)s:S. c s = cl_call) \(\to\) label; % % as_after_return: (\(\Sigma\)s:S. c s = cl_call) \(\to\) S \(\to\) Prop \} % % \end{alltt} % The inductive type for structured traces is actually made by three multiple inductive types with the following semantics: \begin{enumerate} \item $(\verb+trace_label_return+~s_1~s_2)$ (shorthand $\verb+TLR+~s_1~s_2$) is in fact what we called a measurable fragment ending in a return step. % is a trace that begins in % the state $s_1$ (included) and ends just before the state $s_2$ (excluded) % such that the instruction to be executed in $s_1$ is a label emission % statement and the one to be executed in the state before $s_2$ is a return % statement. Thus $s_2$ is the state after the return. The trace % may contain other label emission statements. It captures the structure of % the execution of function bodies: they must start with a cost emission % statement and must end with a return; they are obtained by concatenating % one or more basic blocks, all starting with a label emission % (e.g. in case of loops). \item $(\verb+trace_label_label+~b~s_1~s_2)$ (shorthand $\verb+TLL+~b~s_1~s_2$) models basic blocks. It is the special case of a measurable fragment containing only its first label emission. \item $(\verb+trace_any_label+~b~s_1~s_2)$ (shorthand $\verb+TAL+~b~s_1~s_2$) is a structured fragment, possibly with a return step appended to it, that does not contain any label apart possibly from the first state. \end{enumerate} The above definition summarise the formal rules shown in \autoref{fig:traces}. \begin{figure} \begin{multicols}{3} \infrule[\verb+tlr_base+] {\verb+TLL+~true~s_1~s_2} {\verb+TLR+~s_1~s_2} \infrule[\verb+tlr_step+] {\verb+TLL+~false~s_1~s_2 \andalso \verb+TLR+~s_2~s_3 } {\verb+TLR+~s_1~s_3} \infrule[\verb+tll_base+] {\verb+TAL+~b~s_1~s_2 \andalso L~s_1 } {\verb+TLL+~b~s_1~s_2} \end{multicols} \infrule[\verb+tal_base_not_return+] {s_1\exec s_2 \andalso s_1\class\{\verb+cl_jump+, \verb+cl_other+\}\andalso L~s_2 } {\verb+TAL+~false~s_1~s_2} \infrule[\verb+tal_base_return+] {s_1\exec s_2 \andalso s_1 \class \verb+cl_return+ } {\verb+TAL+~true~s_1~s_2} \infrule[\verb+tal_base_call+] {s_1\exec s_2 \andalso s_1 \class \verb+cl_call+ \andalso s_1\ar s_3 \andalso \verb+TLR+~s_2~s_3 \andalso L~s_3 } {\verb+TAL+~false~s_1~s_3} \infrule[\verb+tal_step_call+] {s_1\exec s_2 \andalso s_1 \class \verb+cl_call+ \andalso s_1\ar s_3 \andalso \verb+TLR+~s_2~s_3 \andalso \verb+TAL+~b~s_3~s_4 } {\verb+TAL+~b~s_1~s_4} \infrule[\verb+tal_step_default+] {s_1\exec s_2 \andalso \lnot L~s_2 \andalso \verb+TAL+~b~s_2~s_3\andalso s_1 \class \verb+cl_other+ } {\verb+TAL+~b~s_1~s_3} \caption{The rules forming the inductive definitions of structured traces.} \label{fig:traces} \end{figure} \begin{comment} \begin{verbatim} inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝ | tlr_base: ∀status_before: S. ∀status_after: S. trace_label_label S ends_with_ret status_before status_after → trace_label_return S status_before status_after | tlr_step: ∀status_initial: S. ∀status_labelled: S. ∀status_final: S. trace_label_label S doesnt_end_with_ret status_initial status_labelled → trace_label_return S status_labelled status_final → trace_label_return S status_initial status_final with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝ | tll_base: ∀ends_flag: trace_ends_with_ret. ∀start_status: S. ∀end_status: S. trace_any_label S ends_flag start_status end_status → as_costed S start_status → trace_label_label S ends_flag start_status end_status with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝ (* Single steps within a function which reach a label. Note that this is the only case applicable for a jump. *) | tal_base_not_return: ∀start_status: S. ∀final_status: S. as_execute S start_status final_status → (as_classifier S start_status cl_jump ∨ as_classifier S start_status cl_other) → as_costed S final_status → trace_any_label S doesnt_end_with_ret start_status final_status | tal_base_return: ∀start_status: S. ∀final_status: S. as_execute S start_status final_status → as_classifier S start_status cl_return → trace_any_label S ends_with_ret start_status final_status (* A call followed by a label on return. *) | tal_base_call: ∀status_pre_fun_call: S. ∀status_start_fun_call: S. ∀status_final: S. as_execute S status_pre_fun_call status_start_fun_call → ∀H:as_classifier S status_pre_fun_call cl_call. as_after_return S «status_pre_fun_call, H» status_final → trace_label_return S status_start_fun_call status_final → as_costed S status_final → trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final (* A call followed by a non-empty trace. *) | tal_step_call: ∀end_flag: trace_ends_with_ret. ∀status_pre_fun_call: S. ∀status_start_fun_call: S. ∀status_after_fun_call: S. ∀status_final: S. as_execute S status_pre_fun_call status_start_fun_call → ∀H:as_classifier S status_pre_fun_call cl_call. as_after_return S «status_pre_fun_call, H» status_after_fun_call → trace_label_return S status_start_fun_call status_after_fun_call → ¬ as_costed S status_after_fun_call → trace_any_label S end_flag status_after_fun_call status_final → trace_any_label S end_flag status_pre_fun_call status_final | tal_step_default: ∀end_flag: trace_ends_with_ret. ∀status_pre: S. ∀status_init: S. ∀status_end: S. as_execute S status_pre status_init → trace_any_label S end_flag status_init status_end → as_classifier S status_pre cl_other → ¬ (as_costed S status_init) → trace_any_label S end_flag status_pre status_end. \end{verbatim} \end{comment} The equivalent of $|T|$ on fragments can be easily defined by mutual recursion on the three types of traces defined in \autoref{fig:traces}. \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 \tikzset{diag/.append style= {every node/.append style={is other, text height=0,text depth=0,text width=0, text opacity=0} }, } \begin{tabular}{@{}c@{}c@{}c@{}} % \begin{subfigure}{.475\linewidth} % \centering % \begin{tikzpicture}[every join/.style={ar}, join all, thick, % every label/.style=overlay, node distance=10mm] % \matrix [diag] (m) {% % \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\ % \node (s2) {}; & \node (t2) {}; \\ % }; % \node [above=0 of t1, overlay] {$\alpha$}; % {[-stealth] % \draw (s1) -- (t1); % \draw [new] (s2) -- node [above] {$*$} (t2); % } % \draw (s1) to node [rel] {$\S$} (s2); % \draw [new] (t1) to node [rel] {$\S,\L$} (t2); % \end{tikzpicture} % \caption{The \verb+cl_jump+ case.} % \label{subfig:cl_jump} % \end{subfigure} % & \begin{subfigure}[b]{.25\linewidth} \centering \begin{tikzpicture}[every join/.style={ar}, join all, thick, every label/.style=overlay, node distance=10mm] \matrix [diag] (m) {% \node (s1) {}; & \node (t1) {};\\ \node (s2) {}; & \node [newn] (t2) {}; \\ }; {[-stealth] \draw (s1) -- (t1); \draw [new] (s2) -- node [above] {$*$} (t2); } \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2); \end{tikzpicture} \caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.} \label{subfig:cl_other_jump} \end{subfigure} & \begin{subfigure}[b]{.375\linewidth} \centering \begin{tikzpicture}[every join/.style={ar}, join all, thick, every label/.style=overlay, node distance=10mm] \matrix [diag, small gap] (m) {% &\node (t1) {}; \\ \node (s1) {}; \\ && \node [newn] (l) {}; & \node [newn] (t2) {};\\ \node (s2) {}; & \node [newn] (c) {};\\ }; {[-stealth] \draw (s1) -- node [above left] {$f$} (t1); \draw [new] (s2) -- node [above] {$*$} (c); \draw [new] (c) -- node [below right] {$f$} (l); \draw [new] (l) -- node [above] {$*$} (t2); } \draw (s1) to [bend right] node [rel] {$\S$} (s2); \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2); \draw [new] (t1) to [bend left] node [rel] {$\L$} (l); \draw [new] (s1) to [bend left] node [rel] {$\C$} (c); \end{tikzpicture} \caption{The \verb+cl_call+ case.\\\vspace{3.1ex}} \label{subfig:cl_call} \end{subfigure} & \begin{subfigure}[b]{.375\linewidth} \centering \begin{tikzpicture}[every join/.style={ar}, join all, thick, every label/.style=overlay, node distance=10mm] \matrix [diag, small gap] (m) {% \node (s1) {}; \\ &\node (t1) {}; \\ \node (s2) {}; & \node [newn] (c) {};\\ && \node [newn] (r) {}; & \node [newn] (t2) {}; \\ }; {[-stealth] \draw (s1) -- (t1); \draw [new] (s2) -- node [above] {$*$} (c); \draw [new] (c) -- (r); \draw [new] (r) -- node [above] {$*$} (t2); } \draw (s1) to [bend right] node [rel] {$\S$} (s2); \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2); \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r); \end{tikzpicture} \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.} \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 execution fragments, 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 only at the weak execution traces of the object code. 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 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 reduce the requirements of the proofs, with % This would still require a form of structured % execution fragments, stating that both returns and calls are always followed % by a label emission. the downside of polluting 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 % \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation % $|\,.\,|$: the \emph{flattening} of the traces. These functions % allow to extract from a structured trace the list of emitted cost labels. % We only show here the type of one % of them: % \begin{alltt} % flatten_trace_label_return: % \(\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{Structured traces similarity and cost prediction invariance.} % % A compiler pass maps source to object code and initial states to initial % states. The source code and initial state uniquely determine the structured % trace of a program, if it exists. The structured trace fails to exists iff % the structural conditions are violated by the program execution (e.g. a function % body does not start with a cost emission statement). Let us assume that the % target structured trace exists. % % What is the relation between the source and target structured traces? % In general, the two traces can be arbitrarily different. However, we are % interested only in those compiler passes that maps a trace $\tau_1$ to a trace % $\tau_2$ such that % \begin{equation}|\tau_1| = |\tau_2|.\label{th2}\end{equation} % The reason is that the combination of~\eqref{th1} with~\eqref{th2} yields the % corollary % \begin{equation}\label{th3} % \forall s_1,s_2. \forall \tau: \verb+TLR+~s_1~s_2.~ % \verb+clock+~s_2 - \verb+clock+~s_1 = % \Sigma_{\alpha \in |\tau_1|}\;k(\alpha) = % \Sigma_{\alpha \in |\tau_2|}\;k(\alpha). % \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~\eqref{th2}. % Therefore we introduce here a similarity relation between traces with % the same structure. Theorem~\verb+tlr_rel_to_traces_same_flatten+ % in the Matita formalisation shows that~\eqref{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 \verb+as_costed+ and that are classified as \verb+cl_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 % subtraces to concatenation of subtraces of the same length and starting with % the same emission statement, etc. % % In the formalisation 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 the inference rules shown in \autoref{fig:txx_rel} % for the sake of readability. We also omit from trace constructors all arguments, % but those that are traces or that % are used in the premises of the rules. By abuse of notation we denote all three % relations by infixing $\approx$. % % \begin{figure} % \begin{multicols}{2} % \infrule % {tll_1\approx tll_2 % } % {\verb+tlr_base+~tll_1 \approx \verb+tlr_base+~tll_2} % % \infrule % {tll_1 \approx tll_2 \andalso % tlr_1 \approx tlr_2 % } % {\verb+tlr_step+~tll_1~tlr_1 \approx \verb+tlr_step+~tll_2~tlr_2} % \end{multicols} % \vspace{3ex} % \begin{multicols}{2} % \infrule % {L~s_1 = L~s_2 \andalso % tal_1\approx tal_2 % } % {\verb+tll_base+~s_1~tal_1 \approx \verb+tll_base+~s_2~tal_2} % % \infrule % {tal_1\approx tal_2 % } % {\verb+tal_step_default+~tal_1 \approx tal_2} % \end{multicols} % \vspace{3ex} % \infrule % {} % {\verb+tal_base_not_return+\approx taa \append \verb+tal_base_not_return+} % \vspace{1ex} % \infrule % {} % {\verb+tal_base_return+\approx taa \append \verb+tal_base_return+} % \vspace{1ex} % \infrule % {tlr_1\approx tlr_2 \andalso % s_1 \uparrow f \andalso s_2\uparrow f % } % {\verb+tal_base_call+~s_1~tlr_1\approx taa \append \verb+tal_base_call+~s_2~tlr_2} % \vspace{1ex} % \infrule % {tlr_1\approx tlr_2 \andalso % s_1 \uparrow f \andalso s_2\uparrow f \andalso % \verb+tal_collapsable+~tal_2 % } % {\verb+tal_base_call+~s_1~tlr_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2)} % \vspace{1ex} % \infrule % {tlr_1\approx tlr_2 \andalso % s_1 \uparrow f \andalso s_2\uparrow f \andalso % \verb+tal_collapsable+~tal_1 % } % {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_base_call+~s_2~tlr_2)} % \vspace{1ex} % \infrule % {tlr_1 \approx tlr_2 \andalso % s_1 \uparrow f \andalso s_2\uparrow f\andalso % tal_1 \approx tal_2 \andalso % } % {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2} % \caption{The inference rule for the relation $\approx$.} % \label{fig:txx_rel} % \end{figure} % % % \begin{comment} % \begin{verbatim} % let rec tlr_rel S1 st1 st1' S2 st2 st2' % (tlr1 : trace_label_return S1 st1 st1') % (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝ % match tlr1 with % [ tlr_base st1 st1' tll1 ⇒ % match tlr2 with % [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2 % | _ ⇒ False % ] % | tlr_step st1 st1' st1'' tll1 tl1 ⇒ % match tlr2 with % [ tlr_step st2 st2' st2'' tll2 tl2 ⇒ % tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2 % | _ ⇒ False % ] % ] % and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2' % (tll1 : trace_label_label S1 fl1 st1 st1') % (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝ % match tll1 with % [ tll_base fl1 st1 st1' tal1 H ⇒ % match tll2 with % [ tll_base fl2 st2 st2 tal2 G ⇒ % as_label_safe … («?, H») = as_label_safe … («?, G») ∧ % tal_rel … tal1 tal2 % ] % ] % and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' % (tal1 : trace_any_label S1 fl1 st1 st1') % (tal2 : trace_any_label S2 fl2 st2 st2') % on tal1 : Prop ≝ % match tal1 with % [ tal_base_not_return st1 st1' _ _ _ ⇒ % fl2 = doesnt_end_with_ret ∧ % ∃st2mid,taa,H,G,K. % tal2 ≃ taa_append_tal ? st2 ??? taa % (tal_base_not_return ? st2mid st2' H G K) % | tal_base_return st1 st1' _ _ ⇒ % fl2 = ends_with_ret ∧ % ∃st2mid,taa,H,G. % tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa % (tal_base_return ? st2mid st2' H G) % | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ % fl2 = doesnt_end_with_ret ∧ % ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧ % ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. % (* we must allow a tal_base_call to be similar to a call followed % by a collapsable trace (trace_any_any followed by a base_not_return; % we cannot use trace_any_any as it disallows labels in the end as soon % as it is non-empty) *) % (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. % tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨ % ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. % ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'. % tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧ % tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2 % | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ % ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧ % ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. % (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. % tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧ % tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨ % ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. % ∃tl2 : trace_any_label ? fl2 st2mid'' st2'. % tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧ % tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2 % | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ % tal_rel … tl1 tal2 (* <- this makes it many to many *) % ]. % \end{verbatim} % \end{comment} % % % In the preceding rules, a $taa$ is an inhabitant of the % $\verb+trace_any_any+~s_1~s_2$ (shorthand $\verb+TAA+~s_1~s_2$), % an 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 \verb+TAL+'s that do not contain % any function call. Therefore it % is possible to concatenate (using ``$\append$'') a \verb+TAA+ to the % left of a \verb+TAL+. A \verb+TAA+ captures % a sequence of silent moves. % The \verb+tal_collapsable+ unary predicate over \verb+TAL+'s % holds when the argument does not contain any function call and it ends % with a label (not a return). The intuition is that after a function call we % can still perform a sequence of silent actions while remaining similar. % % As should be expected, even though the rules are asymmetric $\approx$ is in fact % an equivalence relation. \bibliographystyle{splncs03} \bibliography{ccexec} % \appendix % \section{Notes for the reviewers} % % The results described in the paper are part of a larger formalisation % (the certification of the CerCo compiler). At the moment of the submission % we need to single out from the CerCo formalisation the results presented here. % Before the 16-th of February we will submit an attachment that contains the % minimal subset of the CerCo formalisation that allows to prove those results. % At that time it will also be possible to measure exactly the size of the % formalisation described here. At the moment a rough approximation suggests % about 2700 lines of Matita code. % % We will also attach the development version of the interactive theorem % prover Matita that compiles the submitted formalisation. Another possibility % is to backport the development to the last released version of the system % to avoid having to re-compile Matita from scratch. % % The programming and certification style used in the formalisation heavily % exploit dependent types. Dependent types are used: 1) to impose invariants % by construction on the data types and operations (e.g. a traces from a state % $s_1$ to a state $s_2$ can be concatenad to a trace from a state % $s_2'$ to a state $s_3$ only if $s_2$ is convertible with $s_2'$); 2) % to state and prove the theorems by using the Russell methodology of % Matthieu Sozeau\footnote{Subset Coercions in Coq in TYPES'06. Matthieu Sozeau. Thorsten Altenkirch and Conor McBride (Eds). Volume 4502 of Lecture Notes in Computer Science. Springer, 2007, pp.237-252. % }, better known in the Coq world as ``\verb+Program+'' and reimplemented in a simpler way in Matita using coercion propagations\footnote{Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi: A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Logical Methods in Computer Science 8(1) (2012)}. However, no result presented depends % mandatorily on dependent types: it should be easy to adapt the technique % and results presented in the paper to HOL. % % Finally, Matita and Coq are based on minor variations of the Calculus of % (Co)Inductive Constructions. These variations do not affect the CerCo % formalisation. Therefore a porting of the proofs and ideas to Coq would be % rather straightforward. \end{document}