source: Papers/itp-2013/ccexec2.tex @ 3347

Last change on this file since 3347 was 3347, checked in by tranquil, 6 years ago

andato avanti...

File size: 89.9 KB
Line 
1\documentclass[bookmarksdepth=2,bookmarksopen]{llncs}
2\usepackage{hyperref}
3\usepackage{graphicx}
4\usepackage{color}
5\usepackage{listings}
6\usepackage{bcprules}%\bcprulessavespace
7\usepackage{verbatim}
8\usepackage{alltt}
9\usepackage{subcaption}
10\usepackage{listings}
11\usepackage{amssymb,amsmath}
12% \usepackage{amsmath}
13\usepackage{multicol}
14
15\providecommand{\eqref}[1]{(\ref{#1})}
16
17% NB: might be worth removing this if changing class in favour of
18% a built-in definition.
19%\newtheorem{theorem}{Theorem}
20\newtheorem{condition}{Condition}
21
22\lstdefinelanguage{coq}
23  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
24   morekeywords={[2]if,then,else,forall,Prop,match,with,end,let},
25  }
26
27\lstdefinelanguage[mine]{C}[ANSI]{C}{
28  morekeywords={int8_t},
29  mathescape,
30  escapechar=\%
31}
32
33\newcommand\LSTfont{\tt\fontsize{8}{8.2}\selectfont}
34
35\lstset{language=[mine]C,basicstyle=\LSTfont,breaklines=false,
36%         keywordstyle=\color{red}\bfseries,
37%         keywordstyle=[2]\color{blue},
38%         commentstyle=\color{green},
39%         stringstyle=\color{blue},
40        showspaces=false,showstringspaces=false,
41%         xleftmargin=1em
42        }
43
44\usepackage{tikz}
45\usetikzlibrary{positioning,calc,patterns,chains,shapes.geometric,scopes}
46\makeatletter
47\pgfutil@ifundefined{pgf@arrow@code@implies}{% supply for lack of double arrow special arrow tip if it is not there%
48  \pgfarrowsdeclare{implies}{implies}%
49  {%
50  \pgfarrowsleftextend{2.2pt}%
51  \pgfarrowsrightextend{2.2pt}%
52  }%
53  {%
54    \pgfsetdash{}{0pt} % do not dash%
55    \pgfsetlinewidth{.33pt}%
56    \pgfsetroundjoin   % fix join%
57    \pgfsetroundcap    % fix cap%
58    \pgfpathmoveto{\pgfpoint{-1.5pt}{2.5pt}}%
59    \pgfpathcurveto{\pgfpoint{-.75pt}{1.5pt}}{\pgfpoint{0.5pt}{.5pt}}{\pgfpoint{2pt}{0pt}}%
60    \pgfpathcurveto{\pgfpoint{0.5pt}{-.5pt}}{\pgfpoint{-.75pt}{-1.5pt}}{\pgfpoint{-1.5pt}{-2.5pt}}%
61    \pgfusepathqstroke%
62  }%
63}{}%
64\makeatother
65
66\tikzset{state/.style={inner sep = 0, outer sep = 2pt, draw, fill},
67         every node/.style={inner sep=2pt},
68         every on chain/.style = {inner sep = 0, outer sep = 2pt},
69         join all/.style = {every on chain/.append style={join}},
70         on/.style={on chain={#1}, state},
71         m/.style={execute at begin node=$, execute at end node=$},
72         node distance=3mm,
73         is other/.style={circle, minimum size = 3pt, state},
74         other/.style={on, is other},
75         is jump/.style={diamond, minimum size = 6pt, state},
76         jump/.style={on, is jump},
77         is call/.style={regular polygon, regular polygon sides=3, minimum size=5pt, state},
78         call/.style={on=going below, is call, node distance=6mm, label=above left:$#1$},
79         is ret/.style={regular polygon, regular polygon sides=3, minimum size=5pt, shape border rotate=180, state},
80         ret/.style={on=going above, is ret, node distance=6mm},
81         chain/.style={start chain=#1 going left},
82         rev ar/.style={stealth-, thick},
83         ar/.style={-stealth, thick},
84         every join/.style={rev ar},
85         labelled/.style={fill=white, label=above:$#1$},
86         vcenter/.style={baseline={([yshift=-.5ex]current bounding box)}},
87         every picture/.style={thick},
88         double equal sign distance/.prefix style={double distance=1.5pt}, %% if already defined (newest version of pgf) it should be ignored%}
89         implies/.style={double, -implies, thin, double equal sign distance, shorten <=5pt, shorten >=5pt},
90         new/.style={densely dashed},
91         rel/.style={font=\scriptsize, fill=white, inner sep=2pt},
92         diag/.style={row sep={11mm,between origins},
93                      column sep={11mm,between origins},
94                      every node/.style={draw, is other}},
95         small vgap/.style={row sep={7mm,between origins}},
96         small gap/.style={row sep={7mm,between origins},column sep={7mm,between origins}},
97         % for article, maybe temporary
98         is jump/.style=is other,
99         is call/.style=is other,
100         is ret/.style=is other,
101}
102
103\def\L{\mathrel{\mathcal L}}
104\def\S{\mathrel{\mathcal S}}
105\def\R{\mathrel{\mathcal R}}
106\def\C{\mathrel{\mathcal C}}
107
108\def\Labels{\mathbb L}
109\def\Functions{\mathbb F}
110
111\newsavebox{\execbox}
112\savebox{\execbox}{\tikz[baseline=-.5ex]\draw [-stealth] (0,0) -- ++(1em, 0);}
113\newcommand{\exec}{\ensuremath{\mathrel{\usebox{\execbox}}}}
114\let\ar\triangleright
115\renewcommand{\verb}{\lstinline[mathescape,basicstyle=\tt\selectfont]}
116
117\let\class\triangleright
118\let\andalso\quad
119
120\newcommand{\append}{\mathbin{@}}
121\newcommand{\iffdef}{\mathrel{:\Leftrightarrow}}
122\newcommand{\Deltacost}{\Delta\verb+cost+}
123
124\let\oldto\to
125\makeatletter
126\def\to{\@ifnextchar[{\new@to}{\oldto}}
127\def\new@to[#1]{\xrightarrow{#1}}
128\def\To{\@ifnextchar[{\new@To}{\implies}}
129\def\new@To[#1]{\stackrel{#1}{\implies}}
130\makeatother
131
132
133\begin{document}
134\pagestyle{plain}
135
136\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
137Emerging Technologies (FET) programme within the Seventh Framework
138Programme for Research of the European Commission, under FET-Open grant
139number: 243881}}
140\author{Paolo Tranquilli \and Claudio Sacerdoti Coen}
141\institute{Department of Computer Science and Engineering, University of Bologna,\\\email{Paolo.Tranquilli@unibo.it}, \email{Claudio.SacerdotiCoen@unibo.it}}
142\maketitle
143\begin{abstract}
144The labelling approach is a technique to lift cost models for non-functional
145properties of programs from the object code to the source code. It is based
146on the preservation of the structure of the high level program in every
147intermediate language used by the compiler. Such structure is captured by
148observables that are added to the semantics and that needs to be preserved
149by the forward simulation proof of correctness of the compiler. Additional
150special observables are required for function calls. In this paper we
151present a generic forward simulation proof that preserves all these observables.
152The proof statement is based on a new mechanised semantics that traces the
153structure of execution when the language is unstructured. The generic semantics
154and simulation proof have been mechanised in the interactive theorem prover
155Matita.
156\end{abstract}
157
158\section{Introduction}
159The \emph{labelling approach} has been introduced in~\cite{easylabelling} as
160a technique to \emph{lift} cost models for non-functional properties of programs
161from the object code to the source code. Examples of non-functional properties
162are execution time, amount of stack/heap space consumed and energy required for
163communication. The basic idea of the approach is that it is impossible to
164provide a \emph{uniform} cost model for an high level language that is preserved
165\emph{precisely} by a compiler. For instance, two instances of an assignment
166$x = y$ in the source code can be compiled very differently according to the
167place (registers vs stack) where $x$ and $y$ are stored at the moment of
168execution. Therefore a precise cost model must assign a different cost
169to every occurrence, and the exact cost can only be known after compilation.
170
171According to the labelling approach, the compiler is free to compile and optimise
172the source code without any major restriction, but it must keep trace
173of what happens to basic blocks during the compilation. The cost model is
174then computed on the object code. It assigns a cost to every basic block.
175Finally, the compiler propagates back the cost model to the source level,
176assigning a cost to each basic block of the source code.
177
178Implementing the labelling approach in a certified compiler
179allows to reason formally on the high level source code of a program to prove
180non-functional properties that are granted to be preserved by the compiler
181itself. The trusted code base is then reduced to 1) the interactive theorem
182prover (or its kernel) used in the certification of the compiler and
1832) the software used to certify the property on the source language, that
184can be itself certified further reducing the trusted code base.
185In~\cite{easylabelling} the authors provide an example of a simple
186certified compiler that implements the labelling approach for the
187imperative \verb+While+ language~\cite{while}, that does not have
188pointers and function calls.
189
190The labelling approach has been shown to scale to more interesting scenarios.
191In particular in~\cite{functionallabelling} it has been applied to a functional
192language and in~\cite{loopoptimizations} it has been shown that the approach
193can be slightly complicated to handle loop optimisations and, more generally,
194program optimisations that do not preserve the structure of basic blocks.
195On-going work also shows that the labelling approach is also compatible with
196the complex analyses required to obtain a cost model for object code
197on processors that implement advanced features like pipelining, superscalar
198architectures and caches.
199
200In 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
2018051 object code. The compiler is
202moderately optimising and implements a compilation chain that is largely
203inspired 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
204of function calls. Surprisingly, the addition of function calls require a
205revisitation of the proof technique given in~\cite{easylabelling}. In
206particular, at the core of the labelling approach there is a forward
207simulation proof that, in the case of \verb+While+, is only minimally
208more complex than the proof required for the preservation of the
209functional properties only. In the case of a programming language with
210function calls, instead, it turns out that the forward simulation proof for
211the back-end languages must grant a whole new set of invariants.
212
213In this paper we present a formalisation in the Matita interactive theorem
214prover~\cite{matita1,matita2} of a generic version of the simulation proof required for unstructured
215languages. All back-end languages of the CerCo compiler are unstructured
216languages, so the proof covers half of the correctness of the compiler.
217The statement of the generic proof is based on a new semantics
218for imperative unstructured languages that is based on \emph{structured
219traces} and that restores the preservation of structure in the observables of
220the semantics. The generic proof allows to almost completely split the
221part of the simulation that deals with functional properties only from the
222part that deals with the preservation of structure.
223
224The plan of this paper is the following. In Section~\ref{labelling} we
225sketch the labelling method and the problems derived from the application
226to languages with function calls. In Section~\ref{semantics} we introduce
227a generic description of an unstructured imperative language and the
228corresponding structured traces (the novel semantics). In
229Section~\ref{simulation} we describe the forward simulation proof.
230Conclusions and future works are in Section~\ref{conclusions}
231
232\section{The labelling approach}
233\label{labelling}
234% \subsection{A brief introduction to the labelling approach}
235We briefly explain the labelling approach on the example in \autoref{examplewhile}.
236The user wants to analyse the execution time of the program (the black lines in
237\autoref{subfig:example_input}). He compiles the program using
238a special compiler that first inserts in the code three label emission
239statements (\verb+EMIT L_i+) to mark the beginning of basic blocks;
240then the compiler compiles the code to machine code (\autoref{subfig:example_oc}),
241granting that the execution of the source and object
242code emits the same sequence of labels ($L_1; L_2; L_2; L_3$ in the example).
243This is achieved by keeping track of basic blocks during compilation, avoiding
244all optimizations that alter the control flow. The latter can be recovered with
245a more refined version of the labelling approach~\cite{tranquill}, but in the
246present paper we stick to this simple variant for simplicity. Once the object
247code is produced, the compiler runs a static code analyzer to associate to
248each label $L_1, \ldots, L_3$ the cost (in clock cycles) of the instructions
249that belong to the corresponding basic block. For example, the cost $k_1$
250associated to $L_1$ is the number of cycles required to execute the block
251$I_3$ and \verb+COND l_2+, while the cost $k_2$ associated to $L_2$ counts the
252cycles required by the block $I_4$ and \verb+GOTO l_1+. The compiler also guarantees
253that every executed instruction is in the scope of some code emission label,
254that each scope does not contain loops (to associate a finite cost), and that
255both branches of a conditional statement are followed by a code emission
256statement. Under these assumptions it is true that the total execution cost
257of the program $\Delta_t$ is equal to the sum over the sequence of emitted
258labels of the cost associated to every label:
259$\Delta_t = k(L_1; L_2; L_2; L_3) = k_1 + k_2 + k_2 + k_3$.
260Finally, the compiler emits an instrumented version of the source code
261(\autoref{subfig:example_instrument}) where label emission statements are replaced
262by increments of a global variable \verb+cost+ that, before every increment, holds the
263exact number of clock cycles spent by the microprocessor so far:
264the difference $\Deltacost$ between the final and initial value of the
265internal clock is $\Deltacost = k_1 + k_2 + k_2 + k_3 = \Delta_t$. Finally, the
266user can employ any available method (e.g. Hoare logic, invariant generators,
267abstract interpretation and automated provers) to certify that $\Deltacost$
268never exceeds a certain bound~\cite{cerco}, which is now a functional property
269of the code.
270\begin{figure}
271\begin{subfigure}[t]{.32\linewidth}
272\begin{lstlisting}[moredelim={[is][\color{red}]{|}{|}}]
273|EMIT L_1;|
274$I_1$;
275for (i=0; i<2; i++) {
276  |EMIT L_2;|
277  $I_2$;
278}
279|EMIT L_3;|
280\end{lstlisting}
281\caption{The input program (black lines) with its labelling (red lines).}
282\label{subfig:example_input}
283\end{subfigure}
284\hfill
285\begin{subfigure}[t]{.23\linewidth}
286\begin{lstlisting}
287     EMIT L_1
288     $I_3$
289l_1: COND l_2
290     EMIT L_2
291     $I_4$
292     GOTO l_1
293l_2: EMIT L_3
294\end{lstlisting}
295\caption{The output labelled object code.}
296\label{subfig:example_oc}
297\end{subfigure}
298\hfill
299\begin{subfigure}[t]{.32\linewidth}
300\begin{lstlisting}
301cost += $k_1$;
302$I_1$;
303for (i=0; i<2; i++) {
304cost += $k_2$;
305  $I_2$;
306}
307cost += $k_3$;           
308\end{lstlisting}
309\caption{The output instrumented code.}
310\label{subfig:example_instrument}
311\end{subfigure}
312% \begin{verbatim}
313% EMIT L_1;                         EMIT L_1         cost += k_1;
314% I_1;                              I_3              I_1;
315% for (i=0; i<2; i++) {        l_1: COND l_2         for (i=0; i<2; i++) {
316%   EMIT L_2;                       EMIT L_2           cost += k_2;           
317%   I_2;                            I_4                I_2;               
318%  }                                GOTO l_1          }                   
319% EMIT L_3;                    l_2: EMIT L_3         cost += k_3;           
320% \end{verbatim}
321\caption{The labelling approach applied to a simple program.\label{examplewhile}. The $I_i$ are sequences of instructions not containing jumps or loops. }
322\end{figure}
323
324\subsection{The labelling approach in presence of calls}
325%
326Let's now consider a simple program written in C that contains a function
327pointer call inside the scope of the cost label $L_1$, in \autoref{subfig:call_input}.
328The labelling method works exactly as before, inserting
329code emission statements/\verb+cost+ variable increments at the beginning
330of every basic block and at the beginning of every function. The compiler
331still grants that the sequence of labels observed on the two programs are
332the same. A new difficulty appears when the compiler needs to statically
333analyze the object code to assign a cost to every label. What should the scope
334of the $L_1$ label be? After executing the $I_4$ block, the \verb+CALL+
335statement passes control to a function that cannot be determined statically.
336Therefore the cost of executing the body must be paid by some other label
337(hence the requirement that every function starts with a code emission
338statement). What label should pay for the cost for the block $I_5$? The only
339reasonable answer is $L_1$, i.e. \emph{the scope of labels should extend to the
340next label emission statement or the end of the function, stepping over function calls}.
341%
342\begin{figure}
343{}\hfill
344\begin{subfigure}[t]{.45\linewidth}
345\centering
346\begin{lstlisting}[xleftmargin=20pt]
347void main() {
348  EMIT L_1;
349  $I_1$;
350  (*f)();
351  $I_2$;
352}
353void g() {
354  EMIT L_2;
355  $I_3$;
356}
357\end{lstlisting}
358\caption{The input labelled C program.}
359\label{subfig:call_input}
360\end{subfigure}
361\hfill
362\begin{subfigure}[t]{.45\linewidth}
363\centering
364\begin{lstlisting}[xleftmargin=20pt]
365main:
366  EMIT L_1
367  $I_4$
368  CALL
369  $I_5$
370  RETURN
371g:
372  EMIT L_2
373  $I_6$
374  RETURN
375\end{lstlisting}
376\caption{The output labelled object code.}
377\label{subfig:call_output}
378\end{subfigure}
379\hfill{}
380\caption{An example compilation of a simple program with a function pointer
381         call.}
382\label{subfig:call_example}
383\end{figure}
384
385The latter definition of scope is adeguate on the source level because
386C is a structured language that guarantees that every function call, if it
387returns, passes control to the first instruction that follows the call. However,
388this is not guaranteed for object code, the backend languages of a compiler
389and, more generally, for unstructured
390languages that use a writable control stack to store the return address of
391calls. For example, $I_6$ could increment by $1$ the return address on the
392stack so that the next \verb+RETURN+ would start at the second instruction
393of $I_5$. The compiler would still be perfectly correct if a random, dead
394code instruction was also added just after each \verb+CALL+. More generally,
395\emph{there is no guarantee that a correct compiler that respects the functional
396behaviour of a program also respects the calling structure of the source code}.
397Without such an assumption, however, it may not be true that the execution cost
398of the program is the sum of the costs associated to the labels emitted. In our
399example, 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.
400
401Obviously, any reasonably written compiler produces object code that behaves
402as if the language was structured (i.e. by properly nesting function
403calls/returns and without tampering with the return addresses on the control
404stack). This property, however, is a property of the runs of object code
405programs, and not a property of the object code that can be easily statically
406verified (as the ones we required for the basic labelling method).
407Therefore, we now need to single out those runs whose cost behaviour can be
408statically predicted, and we need to prove that every run of programs generated
409by our compiler are of that type. We call them \emph{structured} since their
410main property is to respect properties that hold for free on the source code
411because of structure. Moreover, in order to avoid proving
412too many preservation properties of our compiler, we drop the original
413requirements on the object code (all instructons must be in scope of some labels,
414no loops inside a scope, etc.) in favour of the corresponding requirement
415for structured runs (a structured run must start with a label emission, no
416instruction can be executed twice between two emissions, etc.).
417
418We will therefore proceed as follows. In the following section
4191) we formally introduce the notion of
420structured trace, which captures structured runs in the style of labelled
421transition systems; 2) we show that on the object code we can correctly
422compute the execution time of a structured run from the sequence of labels
423observed; 3) we give unstructured languages a semantics in terms of structured
424traces; 4) we show that on the source code we can correctly compute the
425execution time of a program if the compiler produces object code whose
426runs are weakly similar to the source code runs.
427
428The notion of weak bisimulation for structured traces is a global property
429which is hard to prove formally and much more demanding than the simple forward
430simulation required for proofs of preservation of functional properties.
431Therefore in \autoref{simulation} we will present a set of local simulation
432conditions that refine the corresponding conditions for forward simulation and
433that are sufficient to grant the production of weakly similar traces.
434
435All the definitions and theorems presented in the paper have been formalized
436in the interactive theorem prover Matita and are being used to certify
437the complexity preserving compiler developed in the CerCo project~\cite{cerco}.
438The formalization can be
439found at~\ref{YYY} and it heavily relies on algebraic and dependent types for
440both structured traces and the definition of weak similarity. In the paper
441we did not try to stay close to the formalization. On the contrary,
442the definitions given in the paper are the result of a significant
443simplification effort for
444the sake of presentation and to make easier the re-implementation of the
445concepts in a proof assistant which is not based on the Calculus of Inductive
446Constructions. In any case the formalization is heavily commented to allow the
447reader to understand the technical details of the formalization.
448
449
450% @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
451%
452% We briefly sketch here a simplified version of the labelling approach as
453% introduced in~\cite{easylabelling}. The simplification strengthens the
454% sufficient conditions given in~\cite{easylabelling} to allow a simpler
455% explanation. The simplified conditions given here are also used in the
456% CerCo compiler to simplify the proof.
457%
458% Let $\mathcal{P}$ be a programming language whose semantics is given in
459% terms of observables: a run of a program yields a finite or infinite
460% stream of observables. We also assume for the time being that function
461% calls are not available in $\mathcal{P}$. We want to associate a cost
462% model to a program $P$ written in $\mathcal{P}$. The first step is to
463% extend the syntax of $\mathcal{P}$ with a new construct $\verb+emit L+$
464% where $L$ is a label distinct from all observables of $\mathcal{P}$.
465% The semantics of $\verb+emit L+$ is the emission of the observable
466% \verb+L+ that is meant to signal the beginning of a basic block.
467%
468% There exists an automatic procedure that injects into the program $P$ an
469% $\verb+emit L+$ at the beginning of each basic block, using a fresh
470% \verb+L+ for each block. In particular, the bodies of loops, both branches
471% of \verb+if-then-else+s and the targets of \verb+goto+s must all start
472% with an emission statement.
473%
474% Let now $C$ be a compiler from $\mathcal{P}$ to the object code $\mathcal{M}$,
475% that is organised in passes. Let $\mathcal{Q}_i$ be the $i$-th intermediate
476% language used by the compiler. We can easily extend every
477% intermediate language (and its semantics) with an $\verb+emit L+$ statement
478% as we did for $\mathcal{P}$. The same is possible for $\mathcal{M}$ too, with
479% the additional difficulty that the syntax of object code is given as a
480% sequence of bytes. The injection of an emission statement in the object code
481% can be done using a map that maps two consecutive code addresses with the
482% 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
483% instruction stored at $pc_1$ and before the execution of the instruction
484% stored at $pc_2$. The two program counters are necessary because the
485% instruction stored at $pc_1$ can have multiple possible successors (e.g.
486% in case of a conditional branch or an indirect call). Dually, the instruction
487% stored at $pc_2$ can have multiple possible predecessors (e.g. if it is the
488% target of a jump).
489%
490% The compiler, to be functionally correct, must preserve the observational
491% equivalence, i.e. executing the program after each compiler pass should
492% yield the same stream of observables. After the injection of emission
493% statements, observables now capture both functional and non-functional
494% behaviours.
495% This correctness property is called in the literature a forward simulation
496% and is sufficient for correctness when the target language is
497% deterministic~\cite{compcert3}.
498% We also require a stronger, non-functional preservation property: after each
499% pass all basic blocks must start with an emission statement, and all labels
500% \verb+L+ must be unique.
501%
502% Now let $M$ be the object code obtained for the program $P$. Let us suppose
503% that we can statically inspect the code $M$ and associate to each basic block
504% a cost (e.g. the number of clock cycles required to execute all instructions
505% in the basic block, or an upper bound to that time). Every basic block is
506% labelled with an unique label \verb+L+, thus we can actually associate the
507% cost to \verb+L+. Let call it $k(\verb+L+)$.
508%
509% The function $k$ is defined as the cost model for the object code control
510% blocks. It can be equally used as well as the cost model for the source
511% control blocks. Indeed, if the semantics of $P$ is the stream
512% $L_1 L_2 \ldots$, then, because of forward simulation, the semantics of $M$ is
513% also $L_1 L_2 \ldots$ and its actual execution cost is $\Sigma_i k(L_i)$ because
514% every instruction belongs to a control block and every control block is
515% labelled. Thus it is correct to say that the execution cost of $P$ is also
516% $\Sigma_i k(L_i)$. In other words, we have obtained a cost model $k$ for
517% the blocks of the high level program $P$ that is preserved by compilation.
518%
519% How can the user profit from the high level cost model? Suppose, for instance,
520% that he wants to prove that the WCET of his program is bounded by $c$. It
521% is sufficient for him to prove that $\Sigma_i k(L_i) \leq c$, which is now
522% a purely functional property of the code. He can therefore use any technique
523% available to certify functional properties of the source code.
524% What is suggested in~\cite{easylabelling} is to actually instrument the
525% source code $P$ by replacing every label emission statement
526% $\verb+emit L+$ with the instruction $\verb+cost += k(L)+$ that increments
527% a global fresh variable \verb+cost+. The bound is now proved by establishing
528% the program invariant $\verb+cost+ \leq c$, which can be done for example
529% using the Frama-C~\cite{framaC} suite if the source code is some variant of
530% C.
531%
532% In order to extend the labelling approach to function calls we make
533% \verb+CALL f+ emit the observable \verb+f+ and \verb+RET+ emit a distinguished observable
534% \verb+ret+.
535%
536% For example the following execution history of the program in \autoref{fig:esempio}
537% $$I_1; \verb+CALL f+; \verb+COND l+; \verb+EMIT $\ell_2$+; I_3; \verb+RET+; I_2; \verb+RET+$$
538% emits the trace
539% $$\verb+main+, \verb+f+$$
540% \begin{figure}
541% \hfil
542% \begin{minipage}{.2\linewidth}
543% \begin{lstlisting}
544% main: $\!I_1$
545%       CALL f
546%       $I_2$
547%       RET
548% \end{lstlisting}
549% \end{minipage}
550% \begin{minipage}{.1\linewidth}
551% \begin{lstlisting}
552% main
553% main
554% main
555% main
556% \end{lstlisting}
557% \end{minipage}
558% \hfil
559% \begin{minipage}{.2\linewidth}
560% \begin{lstlisting}
561% f: $\!$COND l
562%    EMIT $\ell_2$
563%    RET
564% l: $\!$EMIT $\ell_3$
565%    $I_3$
566%    RET
567% \end{lstlisting}
568% \end{minipage}
569% \begin{minipage}{.1\linewidth}
570% \begin{lstlisting}
571% f
572%
573% $\ell_2$
574%
575% $\ell_3$
576% $\ell_3$
577% \end{lstlisting}
578% \end{minipage}
579% \hfil{}
580% \caption{}
581% \label{fig:esempio}
582% \end{figure}
583%
584%
585% \subsection{Labelling function calls}
586% We now want to extend the labelling approach to support function calls.
587% On the high level, \emph{structured} programming language $\mathcal{P}$ there
588% is not much to change.
589% When a function is invoked, the current basic block is temporarily exited
590% and the basic block the function starts with take control. When the function
591% returns, the execution of the original basic block is resumed. Thus the only
592% significant change is that basic blocks can now be nested. Let \verb+E+
593% be the label of the external block and \verb+I+ the label of a nested one.
594% Since the external starts before the internal, the semantics observed will be
595% \verb+E I+ and the cost associated to it on the source language will be
596% $k(\verb+E+) + k(\verb+I+)$, i.e. the cost of executing all instructions
597% in the block \verb+E+ first plus the cost of executing all the instructions in
598% the block \verb+I+. However, we know that some instructions in \verb+E+ are
599% executed after the last instruction in \verb+I+. This is actually irrelevant
600% because we are here assuming that costs are additive, so that we can freely
601% 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
602% the function call terminates and yields back control to the basic block
603% \verb+E+. If the call diverges, the instrumentation
604% $\verb+cost += k(E)+$ executed at the beginning of \verb+E+ is still valid,
605% but just as an upper bound to the real execution cost: only precision is lost.
606%
607% Let now consider what happens when we move down the compilation chain to an
608% unstructured intermediate or final language. Here unstructured means that
609% the only control operators are conditional and unconditional jumps, function
610% calls and returns. Unlike a structured language, though, there is no guarantee
611% that a function will return control just after the function call point.
612% The semantics of the return statement, indeed, consists in fetching the
613% return address from some internal structure (typically the control stack) and
614% jumping directly to it. The code can freely manipulate the control stack to
615% make the procedure returns to whatever position. Indeed, it is also possible
616% to break the well nesting of function calls/returns.
617%
618% Is it the case that the code produced by a correct compiler must respect the
619% additional property that every function returns just after its function call
620% point? The answer is negative and the property is not implied by forward
621% simulation proofs. For instance, imagine to modify a correct compiler pass
622% by systematically adding one to the return address on the stack and by
623% putting a \verb+NOP+ (or any other instruction that takes one byte) after
624% every function call. The obtained code will be functionally indistinguishable,
625% and the added instructions will all be dead code.
626%
627% This lack of structure in the semantics badly interferes with the labelling
628% approach. The reason is the following: when a basic block labelled with
629% \verb+E+ contains a function call, it no longer makes any sense to associate
630% to a label \verb+E+ the sum of the costs of all the instructions in the block.
631% Indeed, there is no guarantee that the function will return into the block and
632% that the instructions that will be executed after the return will be the ones
633% we are paying for in the cost model.
634%
635% How can we make the labelling approach work in this scenario? We only see two
636% possible ways. The first one consists in injecting an emission statement after
637% every function call: basic blocks no longer contain function calls, but are now
638% terminated by them. This completely solves the problem and allows the compiler
639% to break the structure of function calls/returns at will. However, the
640% technique has several drawbacks. First of all, it greatly augments the number
641% of cost labels that are injected in the source code and that become
642% instrumentation statements. Thus, when reasoning on the source code to prove
643% non-functional properties, the user (or the automation tool) will have to handle
644% larger expressions. Second, the more labels are emitted, the more difficult it
645% becomes to implement powerful optimisations respecting the code structure.
646% Indeed, function calls are usually implemented in such a way that most registers
647% are preserved by the call, so that the static analysis of the block is not
648% interrupted by the call and an optimisation can involve both the code before
649% and after the function call. Third, instrumenting the source code may require
650% unpleasant modification of it. Take, for example, the code
651% \verb+f(g(x));+. We need to inject an emission statement/instrumentation
652% instruction just after the execution of \verb+g+. The only way to do that
653% is to rewrite the code as \verb+y = g(x); emit L; f(y);+ for some fresh
654% variable \verb+y+. It is pretty clear how in certain situations the obtained
655% code would be more obfuscated and then more difficult to manually reason on.
656%
657% For the previous reasons, in this paper and in the CerCo project we adopt a
658% different approach. We do not inject emission statements after every
659% function call. However, we want to propagate a strong additional invariant in
660% the forward simulation proof. The invariant is the propagation of the structure
661%  of the original high level code, even if the target language is unstructured.
662% The structure we want to propagate, that will become more clear in the next
663% section, comprises 1) the property that every function should return just after
664% the function call point, which in turns imply well nesting of function calls;
665% 2) the property that every basic block starts with a code emission statement.
666%
667% In the original labelling approach of~\cite{easylabelling}, the second property
668% was granted syntactically as a property of the generated code.
669% In our revised approach, instead, we will impose the property on the runs:
670% it will be possible to generate code that does not respect the syntactic
671% property, as soon as all possible runs respect it. For instance, dead code will no longer
672% be required to have all basic blocks correctly la. The switch is suggested
673% from the fact that the first of the two properties --- that related to
674% function calls/returns --- can only be defined as property of runs,
675% not of the static code. The switch is
676% beneficial to the proof because the original proof was made of two parts:
677% the forward simulation proof and the proof that the static property was granted.
678% In our revised approach the latter disappears and only the forward simulation
679% is kept.
680%
681% In order to capture the structure semantics so that it is preserved
682% by a forward simulation argument, we need to make the structure observable
683% in the semantics. This is the topic of the next section.
684
685\section{Structured traces}
686\label{semantics}
687
688Let's consider a generic unstructured language already equipped with a
689small step structured operational semantics (SOS). We introduce a
690deterministic labelled transition system~\cite{LTS} $(S,s_{\mathrm{init}},\Lambda,\to)$
691that refines the
692SOS by observing function calls and the beginning of basic blocks.
693$S$ is the set of states of the program, $s_\mathrm{init}$ the initial state and
694$\Lambda = \{ \tau, RET \} \cup \Labels \cup \Functions$
695where $\Functions$ is the set of names of functions that can occur in the
696program, $\Labels$ is a set of labels disjoint from $\Functions$
697and $\tau$ and $RET$ do not belong to $\Functions \cup \Labels$.
698The transition function is defined as $s_1 \to[o] s_2$ if
699$s_1$ moves to $s_2$ according to the SOS; moreover $o = f \in \Functions$ if
700the function $f$ is called, $o = RET$ if a \verb+RETURN+ is executed,
701$o = L \in \Labels$ if an \verb+EMIT $L$+ is executed to signal the
702beginning of a basic block, and $o = \tau$ in all other cases.
703Because we assume the language to be deterministic, the label emitted can
704actually be computed simply observing $s_1$. Finally, $S$ is also endowed with
705a relation $s\ar s'$ ($s'$ \emph{follows} $s$) when the instruction to be executed
706in $s'$ is just after the one in $s$.
707
708Among all possible finite execution fragments we want to
709identify the ones that satisfy the requirements we sketched in the previous
710section. We say that an execution fragment
711$s_0 \to[o_0] s_1 \to[o_1] \ldots \to[o_n] s_n$
712is \emph{structured} (marking it as $s_0 \To s_n$) iff the following conditions
713are met.
714\begin{enumerate}
715 \item For every $i$, if $s_i \to[f] s_{i+1}$ then there is a
716   label $L$ and a $k\ge i+2$ such that
717    $s_{i+1} \to[L] s_{i+2} \To s_k \to[RET] s_{k+1}$, with
718    $s_i \ar s_{k+1}$.
719   In other words, $s_{i+1}$ must start execution with an \verb+EMIT $L$+
720   and then continue with a structured fragment returning control
721   to the instruction immediately following the call.
722   This captures the requirements that the body of function calls always start
723   with a label emission statement, and every function
724   call must converge yielding back control just after it.
725 \item The number of $RET$'s in the fragment is equal to the number of
726   calls, i.e.\ the number of observables in $\Functions$. This, together with
727   the above condition, captures the well-bracketing of the fragment with
728   respect to function calls.
729 \item For every $i$, if the instruction to be executed in $s_i$ is a
730   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
731   \verb+EMIT $L$+. This captures the requirement that every branch which is
732   live code must start with a label emission.
733\end{enumerate}
734
735Let $T = s_0 \stackrel{o_0}{\to} s_1 \ldots \stackrel{o_n}{\to} s_{n+1}$ be an
736execution fragment. The \emph{weak trace} $|T|$ associated to $T$ is the
737subsequence $o_{i_0} \ldots o_{i_m}$ of $o_0 \ldots o_n$ obtained dropping
738every internal action $\tau$.
739
740Let $k$ be a cost model that maps observables actions to any commutative cost
741monoid (e.g. natural numbers). We extend the domain of $k$ to weak traces
742by posing $k(\mathcal{T}) = \Sigma_{o \in \mathcal{T}} k(o)$.
743
744The labelling approach is based on the idea that the execution cost of
745certain execution fragments, that we call \emph{measurable fragments}, can be
746computed from their weak trace by choosing a $k$ that assigns to any label
747the cost of the instructions in its scope.
748A structured fragment
749$T = s_0 \To s_n$ is
750measurable if it does not start or end in the middle of a basic block.
751Ending in the middle of a block would mean having pre-paid more instructions
752than the ones executed, and starting in the middle would mean not paying any
753instruction up to the first label emission.
754Formally we require $o_0 \in \Labels$ (or equivalently
755in $s_0$ the program must emit a label) and either
756$s_{n-1}\to[RET]s_n$ or $s_n$ must be a label emission statement
757(i.e.\ $s_n \to[L] s_{n+1}$).
758
759Given two deterministic unstructured programming languages with their own
760operational semantics, we say that a state $s_2$ of the second language
761(weakly) simulates the state $s_1$ of the first iff the two unique weak traces
762that originate from them are equal. If $s_1$ also (weakly) simulates $s_2$,
763then the two states are weakly trace equivalent.
764
765 or, equivalently
766because of determinism, that they are weakly bisimilar.
767% @@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
768%
769% The program semantics adopted in the traditional labelling approach is based
770% on labelled deductive systems. Given a set of observables $\mathcal{O}$ and
771% a set of states $\S$, the semantics of one deterministic execution
772% step is
773% defined as a function $S \to S \times O^*$ where $O^*$ is a (finite) stream of
774% observables. The semantics is then lifted compositionally to multiple (finite
775% or infinite) execution steps.
776% Finally, the semantics of a a whole program execution is obtained by forgetting
777% about the final state (if any), yielding a function $S \to O^*$ that given an
778% initial status returns the finite or infinite stream of observables in output.
779%
780% We present here a new definition of semantics where the structure of execution,
781% as defined in the previous section, is now observable. The idea is to replace
782% the stream of observables with a structured data type that makes explicit
783% function call and returns and that grants some additional invariants by
784% construction. The data structure, called \emph{structured traces}, is
785% defined inductively for terminating programs and coinductively for diverging
786% ones. In the paper we focus only on the inductive structure, i.e. we assume
787% that all programs that are given a semantics are total. The Matita formalisation
788% also shows the coinductive definitions. The semantics of a program is then
789% defined as a function that maps an initial state into a structured trace.
790%
791% In order to have a definition that works on multiple intermediate languages,
792% we abstract the type of structure traces over an abstract data type of
793% abstract statuses, which we aptly call $\verb+abstract_status+$. The fields
794% of this record are the following.
795% \begin{itemize}
796%  \item \verb+S : Type[0]+, the type of states.
797%  \item \verb+as_execute : S $\to$ S $\to$ Prop+, a binary predicate stating
798%  an execution step. We write $s_1\exec s_2$ for $\verb+as_execute+~s_1~s_2$.
799%  \item \verb+as_classifier : S $\to$ classification+, a function tagging all
800%  states with a class in
801%  $\{\verb+cl_return,cl_jump,cl_call,cl_other+\}$, depending on the instruction
802%  that is about to be executed (we omit tail-calls for simplicity). We will
803%  use $s \class c$ as a shorthand for both $\verb+as_classifier+~s=c$
804%  (if $c$ is a classification) and $\verb+as_classifier+~s\in c$
805%  (if $c$ is a set of classifications).
806%  \item \verb+as_label : S $\to$ option label+, telling whether the
807%  next instruction to be executed in $s$ is a cost emission statement,
808%  and if yes returning the associated cost label. Our shorthand for this function
809%  will be $\ell$, and we will also abuse the notation by using $\ell~s$ as a
810%  predicate stating that $s$ is labelled.
811%  \item \verb+as_call_ident : ($\Sigma$s:S. s $\class$ cl_call) $\to$ label+,
812%  telling the identifier of the function which is being called in a
813%  \verb+cl_call+ state. We will use the shorthand $s\uparrow f$ for
814%  $\verb+as_call_ident+~s = f$.
815%  \item \verb+as_after_return : ($\Sigma$s:S. s $\class$ cl_call) $\to$ S $\to$ Prop+,
816%  which holds on the \verb+cl_call+ state $s_1$ and a state $s_2$ when the
817%  instruction to be executed in $s_2$ follows the function call to be
818%  executed in (the witness of the $\Sigma$-type) $s_1$. We will use the notation
819%  $s_1\ar s_2$ for this relation.
820% \end{itemize}
821%
822% % \begin{alltt}
823% % record abstract_status := \{ S: Type[0];
824% %  as_execute: S \(\to\) S \(\to\) Prop;   as_classifier: S \(\to\) classification;
825% %  as_label: S \(\to\) option label;    as_called: (\(\Sigma\)s:S. c s = cl_call) \(\to\) label;
826% %  as_after_return: (\(\Sigma\)s:S. c s = cl_call) \(\to\) S \(\to\) Prop \}
827% % \end{alltt}
828%
829% The inductive type for structured traces is actually made by three multiple
830% inductive types with the following semantics:
831% \begin{enumerate}
832%  \item $(\verb+trace_label_return+~s_1~s_2)$ (shorthand $\verb+TLR+~s_1~s_2$)
833%    is a trace that begins in
834%    the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
835%    such that the instruction to be executed in $s_1$ is a label emission
836%    statement and the one to be executed in the state before $s_2$ is a return
837%    statement. Thus $s_2$ is the state after the return. The trace
838%    may contain other label emission statements. It captures the structure of
839%    the execution of function bodies: they must start with a cost emission
840%    statement and must end with a return; they are obtained by concatenating
841%    one or more basic blocks, all starting with a label emission
842%    (e.g. in case of loops).
843%  \item $(\verb+trace_any_label+~b~s_1~s_2)$ (shorthand $\verb+TAL+~b~s_1~s_2$)
844%    is a trace that begins in
845%    the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
846%    such that the instruction to be executed in $s_2$/in the state before
847%    $s_2$ is either a label emission statement or
848%    or a return, according to the boolean $b$. It must not contain
849%    any label emission statement. It captures the notion of a suffix of a
850%    basic block.
851%  \item $(\verb+trace_label_label+~b~s_1~s_2)$ (shorthand $\verb+TLL+~b~s_1~s_2$ is the special case of
852%    $\verb+TAL+~b~s_1~s_2)$ such that the instruction to be
853%    executed in $s_1$ is a label emission statement. It captures the notion of
854%    a basic block.
855% \end{enumerate}
856%
857% \begin{multicols}{3}
858% \infrule[\verb+tlr_base+]
859%  {\verb+TLL+~true~s_1~s_2}
860%  {\verb+TLR+~s_1~s_2}
861%
862% \infrule[\verb+tlr_step+]
863%  {\verb+TLL+~false~s_1~s_2 \andalso
864%   \verb+TLR+~s_2~s_3
865%  }
866%  {\verb+TLR+~s_1~s_3}
867%
868% \infrule[\verb+tll_base+]
869%  {\verb+TAL+~b~s_1~s_2 \andalso
870%   \ell~s_1
871%  }
872%  {\verb+TLL+~b~s_1~s_2}
873% \end{multicols}
874%
875% \infrule[\verb+tal_base_not_return+]
876%  {s_1\exec s_2 \andalso
877%   s_1\class\{\verb+cl_jump+, \verb+cl_other+\}\andalso
878%   \ell~s_2
879%  }
880%  {\verb+TAL+~false~s_1~s_2}
881%
882% \infrule[\verb+tal_base_return+]
883%  {s_1\exec s_2 \andalso
884%   s_1 \class \verb+cl_return+
885%  }
886%  {\verb+TAL+~true~s_1~s_2}
887%
888% \infrule[\verb+tal_base_call+]
889%  {s_1\exec s_2 \andalso
890%   s_1 \class \verb+cl_call+ \andalso
891%   s_1\ar s_3 \andalso
892%   \verb+TLR+~s_2~s_3 \andalso
893%   \ell~s_3
894%  }
895%  {\verb+TAL+~false~s_1~s_3}
896%
897% \infrule[\verb+tal_step_call+]
898%  {s_1\exec s_2 \andalso
899%   s_1 \class \verb+cl_call+ \andalso
900%   s_1\ar s_3 \andalso
901%   \verb+TLR+~s_2~s_3 \andalso
902%   \verb+TAL+~b~s_3~s_4
903%  }
904%  {\verb+TAL+~b~s_1~s_4}
905%
906% \infrule[\verb+tal_step_default+]
907%  {s_1\exec s_2 \andalso
908%   \lnot \ell~s_2 \andalso
909%   \verb+TAL+~b~s_2~s_3\andalso
910%   s_1 \class \verb+cl_other+
911%  }
912%  {\verb+TAL+~b~s_1~s_3}
913% \begin{comment}
914% \begin{verbatim}
915% inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
916%   | tlr_base:
917%       ∀status_before: S.
918%       ∀status_after: S.
919%         trace_label_label S ends_with_ret status_before status_after →
920%         trace_label_return S status_before status_after
921%   | tlr_step:
922%       ∀status_initial: S.
923%       ∀status_labelled: S.
924%       ∀status_final: S.
925%         trace_label_label S doesnt_end_with_ret status_initial status_labelled →
926%         trace_label_return S status_labelled status_final →
927%           trace_label_return S status_initial status_final
928% with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
929%   | tll_base:
930%       ∀ends_flag: trace_ends_with_ret.
931%       ∀start_status: S.
932%       ∀end_status: S.
933%         trace_any_label S ends_flag start_status end_status →
934%         as_costed S start_status →
935%           trace_label_label S ends_flag start_status end_status
936% with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
937%   (* Single steps within a function which reach a label.
938%      Note that this is the only case applicable for a jump. *)
939%   | tal_base_not_return:
940%       ∀start_status: S.
941%       ∀final_status: S.
942%         as_execute S start_status final_status →
943%         (as_classifier S start_status cl_jump ∨
944%          as_classifier S start_status cl_other) →
945%         as_costed S final_status →
946%           trace_any_label S doesnt_end_with_ret start_status final_status
947%   | tal_base_return:
948%       ∀start_status: S.
949%       ∀final_status: S.
950%         as_execute S start_status final_status →
951%         as_classifier S start_status cl_return →
952%           trace_any_label S ends_with_ret start_status final_status
953%   (* A call followed by a label on return. *)
954%   | tal_base_call:
955%       ∀status_pre_fun_call: S.
956%       ∀status_start_fun_call: S.
957%       ∀status_final: S.
958%         as_execute S status_pre_fun_call status_start_fun_call →
959%         ∀H:as_classifier S status_pre_fun_call cl_call.
960%           as_after_return S «status_pre_fun_call, H» status_final →
961%           trace_label_return S status_start_fun_call status_final →
962%           as_costed S status_final →
963%             trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
964%   (* A call followed by a non-empty trace. *)
965%   | tal_step_call:
966%       ∀end_flag: trace_ends_with_ret.
967%       ∀status_pre_fun_call: S.
968%       ∀status_start_fun_call: S.
969%       ∀status_after_fun_call: S.
970%       ∀status_final: S.
971%         as_execute S status_pre_fun_call status_start_fun_call →
972%         ∀H:as_classifier S status_pre_fun_call cl_call.
973%           as_after_return S «status_pre_fun_call, H» status_after_fun_call →
974%           trace_label_return S status_start_fun_call status_after_fun_call →
975%           ¬ as_costed S status_after_fun_call →
976%           trace_any_label S end_flag status_after_fun_call status_final →
977%             trace_any_label S end_flag status_pre_fun_call status_final
978%   | tal_step_default:
979%       ∀end_flag: trace_ends_with_ret.
980%       ∀status_pre: S.
981%       ∀status_init: S.
982%       ∀status_end: S.
983%         as_execute S status_pre status_init →
984%         trace_any_label S end_flag status_init status_end →
985%         as_classifier S status_pre cl_other →
986%         ¬ (as_costed S status_init) →
987%           trace_any_label S end_flag status_pre status_end.
988% \end{verbatim}
989% \end{comment}
990% A \verb+trace_label_return+ is isomorphic to a list of
991% \verb+trace_label_label+s that ends with a cost emission followed by a
992% return terminated \verb+trace_label_label+.
993% The interesting cases are those of $\verb+trace_any_label+~b~s_1~s_2$.
994% A \verb+trace_any_label+ is a sequence of steps built by a syntax directed
995% definition on the classification of $s_1$. The constructors of the datatype
996% impose several invariants that are meant to impose a structure to the
997% otherwise unstructured execution. In particular, the following invariants are
998% imposed:
999% \begin{enumerate}
1000%  \item the trace is never empty; it ends with a return iff $b$ is
1001%        true
1002%  \item a jump must always be the last instruction of the trace, and it must
1003%        be followed by a cost emission statement; i.e. the target of a jump
1004%        is always the beginning of a new basic block; as such it must start
1005%        with a cost emission statement
1006%  \item a cost emission statement can never occur inside the trace, only in
1007%        the status immediately after
1008%  \item the trace for a function call step is made of a subtrace for the
1009%        function body of type
1010%        $\verb+trace_label_return+~s_1~s_2$, possibly followed by the
1011%        rest of the trace for this basic block. The subtrace represents the
1012%        function execution. Being an inductive datum, it grants totality of
1013%        the function call. The status $s_2$ is the one that follows the return
1014%        statement. The next instruction of $s_2$ must follow the function call
1015%        instruction. As a consequence, function calls are also well nested.
1016% \end{enumerate}
1017%
1018% There are three mutual structural recursive functions, one for each of
1019% \verb+TLR+, \verb+TLL+ and \verb+TAL+, for which we use the same notation
1020% $|\,.\,|$: the \emph{flattening} of the traces. These functions
1021% allow to extract from a structured trace the list of emitted cost labels.
1022% %  We only show here the type of one
1023% % of them:
1024% % \begin{alltt}
1025% % flatten_trace_label_return:
1026% %  \(\forall\)S: abstract_status. \(\forall\)\(s_1,s_2\).
1027% %   trace_label_return \(s_1\) \(s_2\) \(\to\) list (as_cost_label S)
1028% % \end{alltt}
1029%
1030% \paragraph{Cost prediction on structured traces.}
1031%
1032% The first main theorem of CerCo about traces
1033% (theorem \verb+compute_max_trace_label_return_cost_ok_with_trace+)
1034% holds for the
1035% instantiation
1036% of the structured traces to the concrete status of object code programs.
1037% Simplifying a bit, it states that
1038% \begin{equation}\label{th1}
1039% \begin{array}{l}\forall s_1,s_2. \forall \tau: \verb+TLR+~s_1~s_2.~
1040%   \verb+clock+~s_2 = \verb+clock+~s_1 +
1041%   \Sigma_{\alpha \in |\tau|}\;k(\alpha)
1042% \end{array}
1043% \end{equation}
1044% where the cost model $k$ is statically computed from the object code
1045% by associating to each label $\alpha$ the sum of the cost of the instructions
1046% in the basic block that starts at $\alpha$ and ends before the next labelled
1047% instruction. The theorem is proved by structural induction over the structured
1048% trace, and is based on the invariant that
1049% iff the function that computes the cost model has analysed the instruction
1050% to be executed at $s_2$ after the one to be executed at $s_1$, and if
1051% the structured trace starts with $s_1$, then eventually it will contain also
1052% $s_2$. When $s_1$ is not a function call, the result holds trivially because
1053% of the $s_1\exec s_2$ condition obtained by inversion on
1054% the trace. The only non
1055% trivial case is the one of function calls: the cost model computation function
1056% does recursion on the first instruction that follows that function call; the
1057% \verb+as_after_return+ condition of the \verb+tal_base_call+ and
1058% \verb+tal_step_call+ grants exactly that the execution will eventually reach
1059% this state.
1060%
1061% \paragraph{Structured traces similarity and cost prediction invariance.}
1062%
1063% A compiler pass maps source to object code and initial states to initial
1064% states. The source code and initial state uniquely determine the structured
1065% trace of a program, if it exists. The structured trace fails to exists iff
1066% the structural conditions are violated by the program execution (e.g. a function
1067% body does not start with a cost emission statement). Let us assume that the
1068% target structured trace exists.
1069%
1070% What is the relation between the source and target structured traces?
1071% In general, the two traces can be arbitrarily different. However, we are
1072% interested only in those compiler passes that maps a trace $\tau_1$ to a trace
1073% $\tau_2$ such that
1074% \begin{equation}|\tau_1| = |\tau_2|.\label{th2}\end{equation}
1075% The reason is that the combination of~\eqref{th1} with~\eqref{th2} yields the
1076% corollary
1077% \begin{equation}\label{th3}
1078% \forall s_1,s_2. \forall \tau: \verb+TLR+~s_1~s_2.~
1079%   \verb+clock+~s_2 - \verb+clock+~s_1 =
1080%   \Sigma_{\alpha \in |\tau_1|}\;k(\alpha) =
1081%   \Sigma_{\alpha \in |\tau_2|}\;k(\alpha).
1082% \end{equation}
1083% 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
1084% transfer the cost model from the target to the source code and reason on the
1085% source code only.
1086%
1087% We are therefore interested in conditions stronger than~\eqref{th2}.
1088% Therefore we introduce here a similarity relation between traces with
1089% the same structure. Theorem~\verb+tlr_rel_to_traces_same_flatten+
1090% in the Matita formalisation shows that~\eqref{th2} holds for every pair
1091% $(\tau_1,\tau_2)$ of similar traces.
1092%
1093% Intuitively, two traces are similar when one can be obtained from
1094% the other by erasing or inserting silent steps, i.e. states that are
1095% not \verb+as_costed+ and that are classified as \verb+cl_other+.
1096% Silent steps do not alter the structure of the traces.
1097% In particular,
1098% the relation maps function calls to function calls to the same function,
1099% label emission statements to emissions of the same label, concatenation of
1100% subtraces to concatenation of subtraces of the same length and starting with
1101% the same emission statement, etc.
1102%
1103% In the formalisation the three similarity relations --- one for each trace
1104% kind --- are defined by structural recursion on the first trace and pattern
1105% matching over the second. Here we turn
1106% the definition into the inference rules shown in \autoref{fig:txx_rel}
1107% for the sake of readability. We also omit from trace constructors all arguments,
1108% but those that are traces or that
1109% are used in the premises of the rules. By abuse of notation we denote all three
1110% relations by infixing $\approx$.
1111%
1112% \begin{figure}
1113% \begin{multicols}{2}
1114% \infrule
1115%  {tll_1\approx tll_2
1116%  }
1117%  {\verb+tlr_base+~tll_1 \approx \verb+tlr_base+~tll_2}
1118%
1119% \infrule
1120%  {tll_1 \approx tll_2 \andalso
1121%   tlr_1 \approx tlr_2
1122%  }
1123%  {\verb+tlr_step+~tll_1~tlr_1 \approx \verb+tlr_step+~tll_2~tlr_2}
1124% \end{multicols}
1125% \vspace{3ex}
1126% \begin{multicols}{2}
1127% \infrule
1128%  {\ell~s_1 = \ell~s_2 \andalso
1129%   tal_1\approx tal_2
1130%  }
1131%  {\verb+tll_base+~s_1~tal_1 \approx \verb+tll_base+~s_2~tal_2}
1132%
1133% \infrule
1134%  {tal_1\approx tal_2
1135%  }
1136%  {\verb+tal_step_default+~tal_1 \approx tal_2}
1137% \end{multicols}
1138% \vspace{3ex}
1139% \infrule
1140%  {}
1141%  {\verb+tal_base_not_return+\approx taa \append \verb+tal_base_not_return+}
1142% \vspace{1ex}
1143% \infrule
1144%  {}
1145%  {\verb+tal_base_return+\approx taa \append \verb+tal_base_return+}
1146% \vspace{1ex}
1147% \infrule
1148%  {tlr_1\approx tlr_2 \andalso
1149%   s_1 \uparrow f \andalso s_2\uparrow f
1150%  }
1151%  {\verb+tal_base_call+~s_1~tlr_1\approx taa \append \verb+tal_base_call+~s_2~tlr_2}
1152% \vspace{1ex}
1153% \infrule
1154%  {tlr_1\approx tlr_2 \andalso
1155%   s_1 \uparrow f \andalso s_2\uparrow f \andalso
1156%   \verb+tal_collapsable+~tal_2
1157%  }
1158%  {\verb+tal_base_call+~s_1~tlr_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2)}
1159% \vspace{1ex}
1160% \infrule
1161%  {tlr_1\approx tlr_2 \andalso
1162%   s_1 \uparrow f \andalso s_2\uparrow f \andalso
1163%   \verb+tal_collapsable+~tal_1
1164%  }
1165%  {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_base_call+~s_2~tlr_2)}
1166% \vspace{1ex}
1167% \infrule
1168%  {tlr_1 \approx tlr_2 \andalso
1169%   s_1 \uparrow f \andalso s_2\uparrow f\andalso
1170%   tal_1 \approx tal_2 \andalso
1171%  }
1172%  {\verb+tal_step_call+~s_1~tlr_1~tal_1 \approx taa \append \verb+tal_step_call+~s_2~tlr_2~tal_2}
1173% \caption{The inference rule for the relation $\approx$.}
1174% \label{fig:txx_rel}
1175% \end{figure}
1176% %
1177% \begin{comment}
1178% \begin{verbatim}
1179% let rec tlr_rel S1 st1 st1' S2 st2 st2'
1180%   (tlr1 : trace_label_return S1 st1 st1')
1181%   (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
1182% match tlr1 with
1183%   [ tlr_base st1 st1' tll1 ⇒
1184%     match tlr2 with
1185%     [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
1186%     | _ ⇒ False
1187%     ]
1188%   | tlr_step st1 st1' st1'' tll1 tl1 ⇒
1189%     match tlr2 with
1190%     [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
1191%       tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
1192%     | _ ⇒ False
1193%     ]
1194%   ]
1195% and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
1196%  (tll1 : trace_label_label S1 fl1 st1 st1')
1197%  (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
1198%   match tll1 with
1199%   [ tll_base fl1 st1 st1' tal1 H ⇒
1200%     match tll2 with
1201%     [ tll_base fl2 st2 st2 tal2 G ⇒
1202%       as_label_safe … («?, H») = as_label_safe … («?, G») ∧
1203%       tal_rel … tal1 tal2
1204%     ]
1205%   ]
1206% and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
1207%  (tal1 : trace_any_label S1 fl1 st1 st1')
1208%  (tal2 : trace_any_label S2 fl2 st2 st2')
1209%    on tal1 : Prop ≝
1210%   match tal1 with
1211%   [ tal_base_not_return st1 st1' _ _ _ ⇒
1212%     fl2 = doesnt_end_with_ret ∧
1213%     ∃st2mid,taa,H,G,K.
1214%     tal2 ≃ taa_append_tal ? st2 ??? taa
1215%       (tal_base_not_return ? st2mid st2' H G K)
1216%   | tal_base_return st1 st1' _ _ ⇒
1217%     fl2 = ends_with_ret ∧
1218%     ∃st2mid,taa,H,G.
1219%     tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
1220%       (tal_base_return ? st2mid st2' H G)
1221%   | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒
1222%     fl2 = doesnt_end_with_ret ∧
1223%     ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
1224%     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
1225%     (* we must allow a tal_base_call to be similar to a call followed
1226%       by a collapsable trace (trace_any_any followed by a base_not_return;
1227%       we cannot use trace_any_any as it disallows labels in the end as soon
1228%       as it is non-empty) *)
1229%     (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
1230%       tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
1231%     ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
1232%     ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
1233%       tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
1234%       tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
1235%   | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
1236%     ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
1237%     ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
1238%     (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
1239%       tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
1240%       tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
1241%     ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
1242%     ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
1243%       tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
1244%       tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
1245%   | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
1246%     tal_rel … tl1 tal2 (* <- this makes it many to many *)
1247%   ].
1248% \end{verbatim}
1249% \end{comment}
1250% %
1251% In the preceding rules, a $taa$ is an inhabitant of the
1252% $\verb+trace_any_any+~s_1~s_2$ (shorthand $\verb+TAA+~s_1~s_2$),
1253% an inductive data type whose definition
1254% is not in the paper for lack of space. It is the type of valid
1255% prefixes (even empty ones) of \verb+TAL+'s that do not contain
1256% any function call. Therefore it
1257% is possible to concatenate (using ``$\append$'') a \verb+TAA+ to the
1258% left of a \verb+TAL+. A \verb+TAA+ captures
1259% a sequence of silent moves.
1260% The \verb+tal_collapsable+ unary predicate over \verb+TAL+'s
1261% holds when the argument does not contain any function call and it ends
1262% with a label (not a return). The intuition is that after a function call we
1263% can still perform a sequence of silent actions while remaining similar.
1264%
1265% As should be expected, even though the rules are asymmetric $\approx$ is in fact
1266% an equivalence relation.
1267\section{Forward simulation}
1268\label{simulation}
1269
1270We summarise here the results of the previous sections. Each intermediate
1271unstructured language can be given a semantics based on structured traces,
1272that single out those runs that respect a certain number of invariants.
1273A cost model can be computed on the object code and it can be used to predict
1274the execution costs of runs that produce structured traces. The cost model
1275can be lifted from the target to the source code of a pass if the pass maps
1276structured traces to similar structured traces. The latter property is called
1277a \emph{forward simulation}.
1278
1279As for labelled transition systems, in order to establish the forward
1280simulation we are interested in (preservation of observables), we are
1281forced to prove a stronger notion of forward simulation that introduces
1282an explicit relation between states. The classical notion of a 1-to-many
1283forward simulation is the existence of a relation $\S$ over states such that
1284if $s_1 \S s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
1285$s_2 \to^* s_2'$ and $s_1' \S s_2'$. In our context, we need to replace the
1286one and multi step transition relations $\to^n$ with the existence of
1287a structured trace between the two states, and we need to add the request that
1288the two structured traces are similar. Thus what we would like to state is
1289something like:\\
1290for all $s_1,s_2,s_1'$ such that there is a $\tau_1$ from
1291$s_1$ to $s_1'$ and $s_1 \S s_2$ there exists an $s_2'$ such that
1292$s_1' \S s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
1293$\tau_1$ is similar to $\tau_2$. We call this particular form of forward
1294simulation \emph{trace reconstruction}.
1295
1296The statement just introduced, however, is too simplistic and not provable
1297in the general case. To understand why, consider the case of a function call
1298and the pass that fixes the parameter passing conventions. A function
1299call in the source code takes in input an arbitrary number of pseudo-registers (the actual parameters to pass) and returns an arbitrary number of pseudo-registers (where the result is stored). A function call in the target language has no
1300input nor output parameters. The pass must add explicit code before and after
1301the function call to move the pseudo-registers content from/to the hardware
1302registers or the stack in order to implement the parameter passing strategy.
1303Similarly, each function body must be augmented with a preamble and a postamble
1304to complete/initiate the parameter passing strategy for the call/return phase.
1305Therefore what used to be a call followed by the next instruction to execute
1306after the function return, now becomes a sequence of instructions, followed by
1307a call, followed by another sequence. The two states at the beginning of the
1308first sequence and at the end of the second sequence are in relation with
1309the status before/after the call in the source code, like in an usual forward
1310simulation. How can we prove however the additional condition for function calls
1311that asks that when the function returns the instruction immediately after the
1312function call is called? To grant this invariant, there must be another relation
1313between the address of the function call in the source and in the target code.
1314This additional relation is to be used in particular to relate the two stacks.
1315
1316Another example is given by preservation of code emission statements. A single
1317code emission instruction can be simulated by a sequence of steps, followed
1318by a code emission, followed by another sequence. Clearly the initial and final
1319statuses of the sequence are to be in relation with the status before/after the
1320code emission in the source code. In order to preserve the structured traces
1321invariants, however, we must consider a second relation between states that
1322traces the preservation of the code emission statement.
1323
1324Therefore we now introduce an abstract notion of relation set between abstract
1325statuses and an abstract notion of 1-to-many forward simulation conditions.
1326These two definitions enjoy the following remarkable properties:
1327\begin{enumerate}
1328 \item they are generic enough to accommodate all passes of the CerCo compiler
1329 \item the conjunction of the 1-to-many forward simulation conditions are
1330       just slightly stricter than the statement of a 1-to-many forward
1331       simulation in the classical case. In particular, they only require
1332       the construction of very simple forms of structured traces made of
1333       silent states only.
1334 \item they allow to prove our main result of the paper: the 1-to-many
1335       forward simulation conditions are sufficient to prove the trace
1336       reconstruction theorem
1337\end{enumerate}
1338
1339Point 3. is the important one. First of all it means that we have reduced
1340the complex problem of trace reconstruction to a much simpler one that,
1341moreover, can be solved with slight adaptations of the forward simulation proof
1342that is performed for a compiler that only cares about functional properties.
1343Therefore we have successfully splitted as much as possible the proof of
1344preservation of functional properties from that of non-functional ones.
1345Secondly, combined with the results in the previous section, it implies
1346that the cost model can be computed on the object code and lifted to the
1347source code to reason on non-functional properties, assuming that
1348the 1-to-many forward simulation conditions are fulfilled for every
1349compiler pass.
1350
1351\paragraph{Relation sets.}
1352
1353We introduce now the four relations $\mathcal{S,C,L,R}$ between abstract
1354statuses that are used to correlate the corresponding statues before and
1355after a compiler pass. The first two are abstract and must be instantiated
1356by every pass. The remaining two are derived relations.
1357
1358The $\S$ relation between states is the classical relation used
1359in forward simulation proofs. It correlates the data of the status
1360(e.g. registers, memory, etc.).
1361
1362The $\C$ relation correlates call states. It allows to track the
1363position in the target code of every call in the source code.
1364
1365The $\L$ relation simply says that the two states are both label
1366emitting states that emit the same label, \emph{i.e.}\ $s_1\L s_2\iffdef \ell~s_1=\ell~s_2$.
1367It allows to track the position in
1368the target code of every cost emitting statement in the source code.
1369
1370Finally the $\R$ relation is the more complex one. Two states
1371$s_1$ and $s_2$ are $\R$ correlated if every time $s_1$ is the
1372successors of a call state that is $\C$-related to a call state
1373$s_2'$ in the target code, then $s_2$ is the successor of $s_2'$. Formally:
1374$$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.$$
1375We will require all pairs of states that follow a related call to be
1376$\R$-related. This is the fundamental requirement granting
1377that the target trace is well structured, \emph{i.e.}\ that calls are well
1378nested and returning where they are supposed to.
1379
1380% \begin{alltt}
1381% record status_rel (S1,S2 : abstract_status) : Type[1] := \{
1382%   \(\S\): S1 \(\to\) S2 \(\to\) Prop;
1383%   \(\C\): (\(\Sigma\)s.as_classifier S1 s cl_call) \(\to\)
1384%      (\(\Sigma\)s.as_classifier S2 s cl_call) \(\to\) Prop \}.
1385%
1386% definition \(\L\) S1 S2 st1 st2 := as_label S1 st1 = as_label S2 st2.
1387%
1388% definition \(\R\) S1 S2 (R: status_rel S1 S2) s1_ret s2_ret ≝
1389%  \(\forall\)s1_pre,s2_pre.
1390%   as_after_return s1_pre s1_ret \(\to\) s1_pre \(\R\) s2_pre \(\to\)
1391%    as_after_return s2_pre s2_ret.
1392% \end{alltt}
1393
1394\begin{figure}
1395\centering
1396\begin{tabular}{@{}c@{}c@{}c@{}}
1397% \begin{subfigure}{.475\linewidth}
1398% \centering
1399% \begin{tikzpicture}[every join/.style={ar}, join all, thick,
1400%                             every label/.style=overlay, node distance=10mm]
1401%     \matrix [diag] (m) {%
1402%          \node (s1) [is jump] {}; & \node [fill=white] (t1) {};\\
1403%          \node (s2) {}; & \node (t2) {}; \\
1404%     };
1405%     \node [above=0 of t1, overlay] {$\alpha$};
1406%     {[-stealth]
1407%     \draw (s1) -- (t1);
1408%     \draw [new] (s2) -- node [above] {$*$} (t2);
1409%     }
1410%     \draw (s1) to node [rel] {$\S$} (s2);
1411%     \draw [new] (t1) to node [rel] {$\S,\L$} (t2);
1412% \end{tikzpicture}
1413% \caption{The \verb+cl_jump+ case.}
1414% \label{subfig:cl_jump}
1415% \end{subfigure}
1416% &
1417\begin{subfigure}{.25\linewidth}
1418\centering
1419\begin{tikzpicture}[every join/.style={ar}, join all, thick,
1420                            every label/.style=overlay, node distance=10mm]
1421    \matrix [diag] (m) {%
1422         \node (s1) {}; & \node (t1) {};\\
1423         \node (s2) {}; & \node (t2) {}; \\
1424    };
1425    {[-stealth]
1426    \draw (s1) -- (t1);
1427    \draw [new] (s2) -- node [above] {$*$} (t2);
1428    }
1429    \draw (s1) to [bend right, anchor=mid] node [rel] {$\S$} (s2);
1430    \draw [new] (t1) to [bend left, anchor=mid] node [rel] {$\S,\L$} (t2);
1431\end{tikzpicture}
1432\caption{The \verb+cl_oher+ and \verb+cl_jump+ cases.}
1433\label{subfig:cl_other_jump}
1434\end{subfigure}
1435&
1436\begin{subfigure}{.375\linewidth}
1437\centering
1438\begin{tikzpicture}[every join/.style={ar}, join all, thick,
1439                            every label/.style=overlay, node distance=10mm]
1440    \matrix [diag, small gap] (m) {%
1441         &\node (t1) {}; \\
1442         \node (s1) [is call] {}; \\
1443         && \node (l) {}; & \node (t2) {};\\
1444         \node (s2) {}; & \node (c) [is call] {};\\   
1445    };
1446    {[-stealth]
1447    \draw (s1) -- node [above left] {$f$} (t1);
1448    \draw [new] (s2) -- node [above] {$*$} (c);
1449    \draw [new] (c) -- node [below right] {$f$} (l);
1450    \draw [new] (l) -- node [above] {$*$} (t2);
1451    }
1452    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
1453    \draw [new] (t1) to [bend left] node [rel] {$\S$} (t2);
1454    \draw [new] (t1) to [bend left] node [rel] {$\L$} (l);
1455    \draw [new] (t1) to [bend right] node [rel] {$\C$} (c);
1456    \end{tikzpicture}
1457\caption{The \verb+cl_call+ case.}
1458\label{subfig:cl_call}
1459\end{subfigure}
1460&
1461\begin{subfigure}{.375\linewidth}
1462\centering
1463\begin{tikzpicture}[every join/.style={ar}, join all, thick,
1464                            every label/.style=overlay, node distance=10mm]
1465    \matrix [diag, small gap] (m) {%
1466        \node (s1) [is ret] {}; \\
1467        &\node (t1) {}; \\
1468        \node (s2) {}; & \node (c) [is ret] {};\\
1469        && \node (r) {}; & \node (t2) {}; \\   
1470    };
1471    {[-stealth]
1472    \draw (s1) -- node [above right] {$RET$} (t1);
1473    \draw [new] (s2) -- node [above] {$*$} (c);
1474    \draw [new] (c) -- node [below left] {$RET$} (r);
1475    \draw [new] (r) -- node [above] {$*$} (t2);
1476    }
1477    \draw (s1) to [bend right] node [rel] {$\S$} (s2);
1478    \draw [new, overlay] (t1) to [bend left=60] node [rel] {$\S,\L$} (t2);
1479    \draw [new, overlay] (t1) to [bend left ] node [rel] {$\R$} (r);
1480\end{tikzpicture}
1481\caption{The \verb+cl_return+ case.}
1482\label{subfig:cl_return}
1483\end{subfigure}
1484\end{tabular}
1485\caption{Mnemonic diagrams depicting the hypotheses for the preservation of structured traces.
1486         Dashed lines
1487         and arrows indicates how the diagrams must be closed when solid relations
1488         are present.}
1489\label{fig:forwardsim}
1490\end{figure}
1491
1492\paragraph{1-to-many forward simulation conditions.}
1493\begin{condition}[Cases \verb+cl_other+ and \verb+cl_jump+]
1494 For all $s_1,s_1',s_2$ such that $s_1 \S s_1'$, and
1495 $s_1\exec s_1'$, and either $s_1 \class \verb+cl_other+$ or
1496 both $s_1\class\verb+cl_other+\}$ and $\ell~s_1'$,
1497 there exists an $s_2'$ and a $\verb+trace_any_any_free+~s_2~s_2'$ called $taaf$
1498 such that $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
1499$taaf$ is non empty, or one among $s_1$ and $s_1'$ is \verb+as_costed+.
1500\end{condition}
1501
1502In the above condition depicted in \autoref{subfig:cl_other_jump},
1503a $\verb+trace_any_any_free+~s_1~s_2$ (which from now on
1504will be shorthanded as \verb+TAAF+) is an
1505inductive type of structured traces that do not contain function calls or
1506cost emission statements. Differently from a \verb+TAA+, the
1507instruction to be executed in the lookahead state $s_2$ may be a cost emission
1508statement.
1509
1510The intuition of the condition is that one step can be replaced with zero or more steps if it
1511preserves the relation between the data and if the two final statuses are
1512labelled in the same way. Moreover, we must take special care of the empty case
1513to avoid collapsing two consecutive states that emit a label, missing one of the two emissions.
1514
1515\begin{condition}[Case \verb+cl_call+]
1516 For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$ and
1517 $s_1\exec s_1'$ and $s_1 \class \verb+cl_call+$, there exists $s_a, s_b, s_2'$, a
1518$\verb+TAA+~s_2~s_a$, and a
1519$\verb+TAAF+~s_b~s_2'$ such that:
1520$s_a\class\verb+cl_call+$, the \verb+as_call_ident+'s of
1521the two call states are the same, $s_1 \C s_a$,
1522$s_a\exec s_b$, $s_1' \L s_b$ and
1523$s_1' \S s_2'$.
1524\end{condition}
1525
1526The condition, depicted in \autoref{subfig:cl_call} says that, to simulate a function call, we can perform a
1527sequence of silent actions before and after the function call itself.
1528The old and new call states must be $\C$-related, the old and new
1529states at the beginning of the function execution must be $\L$-related
1530and, finally, the two initial and final states must be $\S$-related
1531as usual.
1532
1533\begin{condition}[Case \verb+cl_return+]
1534 For all $s_1,s_1',s_2$ s.t. $s_1 \S s_1'$,
1535 $s_1\exec s_1'$ and $s_1 \class \verb+cl_return+$, there exists $s_a, s_b, s_2'$, a
1536$\verb+TAA+~s_2~s_a$, a
1537$\verb+TAAF+~s_b~s_2'$ called $taaf$ such that:
1538$s_a\class\verb+cl_return+$,
1539$s_a\exec s_b$,
1540$s_1' \R s_b$ and
1541$s_1' \mathrel{{\S} \cap {\L}} s_2'$ and either
1542$taaf$ is non empty, or $\lnot \ell~s_a$.
1543\end{condition}
1544
1545Similarly to the call condition, to simulate a return we can perform a
1546sequence of silent actions before and after the return statement itself,
1547as depicted in \autoref{subfig:cl_return}.
1548The old and the new statements after the return must be $\R$-related,
1549to grant that they returned to corresponding calls.
1550The two initial and final states must be $\S$-related
1551as usual and, moreover, they must exhibit the same labels. Finally, when
1552the suffix is non empty we must take care of not inserting a new
1553unmatched cost emission statement just after the return statement.
1554
1555\begin{comment}
1556\begin{verbatim}
1557definition status_simulation ≝
1558  λS1 : abstract_status.
1559  λS2 : abstract_status.
1560  λsim_status_rel : status_rel S1 S2.
1561    ∀st1,st1',st2.as_execute S1 st1 st1' →
1562    sim_status_rel st1 st2 →
1563    match as_classify … st1 with
1564    [ None ⇒ True
1565    | Some cl ⇒
1566      match cl with
1567      [ cl_call ⇒ ∀prf.
1568        (*
1569             st1' ------------S----------\
1570              ↑ \                         \
1571             st1 \--L--\                   \
1572              | \       \                   \
1573              S  \-C-\  st2_after_call →taa→ st2'
1574              |       \     ↑
1575             st2 →taa→ st2_pre_call
1576        *)
1577        ∃st2_pre_call.
1578        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
1579        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
1580        ∃st2_after_call,st2'.
1581        ∃taa2 : trace_any_any … st2 st2_pre_call.
1582        ∃taa2' : trace_any_any … st2_after_call st2'.
1583        as_execute … st2_pre_call st2_after_call ∧
1584        sim_status_rel st1' st2' ∧
1585        label_rel … st1' st2_after_call
1586      | cl_return ⇒
1587        (*
1588             st1
1589            / ↓
1590           | st1'----------S,L------------\
1591           S   \                           \
1592            \   \-----R-------\            |     
1593             \                 |           |
1594             st2 →taa→ st2_ret |           |
1595                          ↓   /            |
1596                     st2_after_ret →taaf→ st2'
1597
1598           we also ask that st2_after_ret be not labelled if the taaf tail is
1599           not empty
1600        *)
1601        ∃st2_ret,st2_after_ret,st2'.
1602        ∃taa2 : trace_any_any … st2 st2_ret.
1603        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
1604        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
1605        as_classifier … st2_ret cl_return ∧
1606        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
1607        ret_rel … sim_status_rel st1' st2_after_ret ∧
1608        label_rel … st1' st2'
1609      | cl_other ⇒
1610          (*         
1611          st1 → st1'
1612            |      \
1613            S      S,L
1614            |        \
1615           st2 →taaf→ st2'
1616           
1617           the taaf can be empty (e.g. tunneling) but we ask it must not be the
1618           case when both st1 and st1' are labelled (we would be able to collapse
1619           labels otherwise)
1620         *)
1621        ∃st2'.
1622        ∃taa2 : trace_any_any_free … st2 st2'.
1623        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
1624        sim_status_rel st1' st2' ∧
1625        label_rel … st1' st2'
1626      | cl_jump ⇒
1627        (* just like cl_other, but with a hypothesis more *)
1628        as_costed … st1' →
1629        ∃st2'.
1630        ∃taa2 : trace_any_any_free … st2 st2'.
1631        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
1632        sim_status_rel st1' st2' ∧
1633        label_rel … st1' st2'
1634      ]
1635    ].
1636\end{verbatim}
1637\end{comment}
1638
1639\paragraph{Main result: the 1-to-many forward simulation conditions
1640are sufficient to trace reconstruction}
1641
1642Let us assume that a relation set is given such that the 1-to-many
1643forward simulation conditions are satisfied. Under this assumption we
1644can prove the following three trace reconstruction theorems by mutual
1645structural induction over the traces given in input between the
1646$s_1$ and $s_1'$ states.
1647
1648In particular, the \verb+status_simulation_produce_tlr+ theorem
1649applied to the \verb+main+ function of the program and equal
1650$s_{2_b}$ and $s_2$ states shows that, for every initial state in the
1651source code that induces a structured trace in the source code,
1652the compiled code produces a similar structured trace.
1653
1654\begin{theorem}[\verb+status_simulation_produce_tlr+]
1655For every $s_1,s_1',s_{2_b},s_2$ s.t.
1656there is a $\verb+TLR+~s_1~s_1'$ called $tlr_1$ and a
1657$\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
1658$s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
1659there is a $\verb+TLR+~s_{2_b}~s_{2_m}$ called $tlr_2$ and
1660there is a $\verb+TAAF+~s_{2_m}~s_2'$ called $taaf$
1661s.t. if $taaf$ is non empty then $\lnot (\ell~s_{2_m})$,
1662and $tlr_1\approx tlr_2$
1663and $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1664$s_1' \R s_{2_m}$.
1665\end{theorem}
1666
1667The theorem states that a \verb+trace_label_return+ in the source code
1668together with a precomputed preamble of silent states
1669(the \verb+TAA+) in the target code induces a
1670similar \verb+trace_label_return+ in the target code which can be
1671followed by a sequence of silent states. Note that the statement does not
1672require the produced \verb+trace_label_return+ to start with the
1673precomputed preamble, even if this is likely to be the case in concrete
1674implementations. The preamble in input is necessary for compositionality, e.g.
1675because the 1-to-many forward simulation conditions allow in the
1676case of function calls to execute a preamble of silent instructions just after
1677the function call.
1678
1679Clearly similar results are also available for the other two types of structured
1680traces (in fact, they are all proved simultaneously by mutual induction).
1681% \begin{theorem}[\verb+status_simulation_produce_tll+]
1682% For every $s_1,s_1',s_{2_b},s_2$ s.t.
1683% there is a $\verb+TLL+~b~s_1~s_1'$ called $tll_1$ and a
1684% $\verb+TAA+~s_{2_b}~s_2$ and $s_1 \L s_{2_b}$ and
1685% $s_1 \S s_2$, there exists $s_{2_m},s_2'$ s.t.
1686% \begin{itemize}
1687%  \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
1688%        and a trace $\verb+TLL+~b~s_{2_b}~s_{2_m}$ called $tll_2$
1689%        and a $\verb+TAAF+~s_{2_m}~s_2'$ called $taa_2$ s.t.
1690%        $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1691%        $s_1' \R s_{2_m}$ and
1692%        $tll_1\approx tll_2$ and
1693%        if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
1694%  \item else there exists $s_2'$ and a
1695%        $\verb+TLL+~b~s_{2_b}~s_2'$ called $tll_2$ such that
1696%        $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1697%        $tll_1\approx tll_2$.
1698% \end{itemize}
1699% \end{theorem}
1700%
1701% The statement is similar to the previous one: a source
1702% \verb+trace_label_label+ and a given target preamble of silent states
1703% in the target code induce a similar \verb+trace_label_label+ in the
1704% target code, possibly followed by a sequence of silent moves that become the
1705% preamble for the next \verb+trace_label_label+ translation.
1706%
1707% \begin{theorem}[\verb+status_simulation_produce_tal+]
1708% For every $s_1,s_1',s_2$ s.t.
1709% there is a $\verb+TAL+~b~s_1~s_1'$ called $tal_1$ and
1710% $s_1 \S s_2$
1711% \begin{itemize}
1712%  \item if $b$ (the trace ends with a return) then there exists $s_{2_m},s_2'$
1713%    and a trace $\verb+TAL+~b~s_2~s_{2_m}$ called $tal_2$ and a
1714%    $\verb+TAAF+~s_{2_m}~s_2'$ called $taa_2$ s.t.
1715%    $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1716%    $s_1' \R s_{2_m}$ and
1717%    $tal_1 \approx tal_2$ and
1718%    if $taa_2$ is non empty then $\lnot \ell~s_{2_m}$;
1719%  \item else there exists $s_2'$ and a
1720%    $\verb+TAL+~b~s_2~s_2'$ called $tal_2$ such that
1721%    either $s_1' \mathrel{{\S} \cap {\L}} s_2'$ and
1722%        $tal_1\approx tal_2$
1723%    or $s_1' \mathrel{{\S} \cap {\L}} s_2$ and
1724%    $\verb+tal_collapsable+~tal_1$ and $\lnot \ell~s_1$.
1725% \end{itemize}
1726% \end{theorem}
1727%
1728% The statement is also similar to the previous ones, but for the lack of
1729% the target code preamble.
1730
1731\begin{comment}
1732\begin{corollary}
1733For every $s_1,s_1',s_2$ s.t.
1734there is a $\verb+trace_label_return+~s_1~s_1'$ called $tlr_1$ and
1735$s_1 (\L \cap \S) s_2$
1736there exists $s_{2_m},s_2'$ s.t.
1737there is a $\verb+trace_label_return+~s_2~s_{2_m}$ called $tlr_2$ and
1738there is a $\verb+trace_any_any_free+~s_{2_m}~s_2'$ called $taaf$
1739s.t. if $taaf$ is non empty then $\lnot (\verb+as_costed+~s_{2_m})$,
1740and $\verb+tlr_rel+~tlr_1~tlr_2$
1741and $s_1' (\S \cap \L) s_2'$ and
1742$s_1' \R s_{2_m}$.
1743\end{corollary}
1744\end{comment}
1745
1746\begin{comment}
1747\begin{verbatim}
1748status_simulation_produce_tlr S1 S2 R
1749(* we start from this situation
1750     st1 →→→→tlr→→→→ st1'
1751      | \
1752      L  \---S--\
1753      |          \
1754   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
1755                        by the preceding call)
1756   
1757   and we produce
1758     st1 →→→→tlr→→→→ st1'
1759             \\      /  \
1760             //     R    \-L,S-\
1761             \\     |           \
1762   st2_lab →tlr→ st2_mid →taaf→ st2'
1763*)
1764  st1 st1' st2_lab st2
1765  (tlr1 : trace_label_return S1 st1 st1')
1766  (taa2_pre : trace_any_any S2 st2_lab st2)
1767  (sim_execute : status_simulation S1 S2 R)
1768  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
1769  ∃st2_mid.∃st2'.
1770  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
1771  ∃taa2 : trace_any_any_free … st2_mid st2'.
1772  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
1773  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
1774  tlr_rel … tlr1 tlr2
1775\end{verbatim}
1776\end{comment}
1777
1778\section{Conclusions and future works}
1779\label{conclusions}
1780The labelling approach is a technique to implement compilers that induce on
1781the source code a non uniform cost model determined from the object code
1782produced. The cost model assigns a cost to each basic block of the program.
1783The main theorem of the approach says that there is an exact
1784correspondence between the sequence of basic blocks started in the source
1785and object code, and that no instruction in the source or object code is
1786executed outside a basic block. Thus the cost of object code execution
1787can be computed precisely on the source.
1788
1789In this paper we scale the labelling approach to cover a programming language
1790with function calls. This introduces new difficulties only when the language
1791is unstructured, i.e. it allows function calls to return anywhere in the code,
1792destroying the hope of a static prediction of the cost of basic blocks.
1793We restore static predictability by introducing a new semantics for unstructured
1794programs that single outs well structured executions. The latter are represented
1795by structured traces, a generalisation of streams of observables that capture
1796several structural invariants of the execution, like well nesting of functions
1797or the fact that every basic block must start with a code emission statement.
1798We show that structured traces are sufficiently structured to statically compute
1799a precise cost model on the object code.
1800
1801We introduce a similarity relation on structured traces that must hold between
1802source and target traces. When the relation holds for every program, we prove
1803that the cost model can be lifted from the object to the source code.
1804
1805In order to prove that similarity holds, we present a generic proof of forward
1806simulation that is aimed at pulling apart as much as possible the part of the
1807simulation related to non-functional properties (preservation of structure)
1808from that related to functional properties. In particular, we reduce the
1809problem of preservation of structure to that of showing a 1-to-many
1810forward simulation that only adds a few additional proof obligations to those
1811of a traditional, function properties only, proof.
1812
1813All results presented in the paper are part of a larger certification of a
1814C compiler which is based on the labelling approach. The certification, done
1815in Matita, is the main deliverable of the FET-Open Certified Complexity (CerCo).
1816
1817The short term future work consists in the completion of the certification of
1818the CerCo compiler exploiting the main theorem of this paper.
1819
1820\paragraph{Related works.}
1821CerCo is the first project that explicitly tries to induce a
1822precise cost model on the source code in order to establish non-functional
1823properties of programs on an high level language. Traditional certifications
1824of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation
1825of the functional properties.
1826
1827Usually forward simulations take the following form: for each transition
1828from $s_1$ to $s_2$ in the source code, there exists an equivalent sequence of
1829transitions in the target code of length $n$. The number $n$ of transition steps
1830in the target code can just be the witness of the existential statement.
1831An equivalent alternative when the proof of simulation is constructive consists
1832in providing an explicit function, called \emph{clock function} in the
1833literature~\cite{clockfunctions}, that computes $n$ from $s_1$. Every clock
1834function constitutes then a cost model for the source code, in the spirit of
1835what we are doing in CerCo. However, we believe our solution to be superior
1836in the following respects: 1) the machinery of the labelling approach is
1837insensible to the resource being measured. Indeed, any cost model computed on
1838the object code can be lifted to the source code (e.g. stack space used,
1839energy consumed, etc.). On the contrary, clock functions only talk about
1840number of transition steps. In order to extend the approach with clock functions
1841to other resources, additional functions must be introduced. Moreover, the
1842additional functions would be handled differently in the proof.
18432) the cost models induced by the labelling approach have a simple presentation.
1844In particular, they associate a number to each basic block. More complex
1845models can be induced when the approach is scaled to cover, for instance,
1846loop optimisations~\cite{loopoptimizations}, but the costs are still meant to
1847be easy to understand and manipulate in an interactive theorem prover or
1848in Frama-C.
1849On the contrary, a clock function is a complex function of the state $s_1$
1850which, as a function, is an opaque object that is difficult to reify as
1851source code in order to reason on it.
1852
1853\bibliographystyle{splncs03}
1854\bibliography{ccexec}
1855
1856% \appendix
1857% \section{Notes for the reviewers}
1858%
1859% The results described in the paper are part of a larger formalization
1860% (the certification of the CerCo compiler). At the moment of the submission
1861% we need to single out from the CerCo formalization the results presented here.
1862% Before the 16-th of February we will submit an attachment that contains the
1863% minimal subset of the CerCo formalization that allows to prove those results.
1864% At that time it will also be possible to measure exactly the size of the
1865% formalization described here. At the moment a rough approximation suggests
1866% about 2700 lines of Matita code.
1867%
1868% We will also attach the development version of the interactive theorem
1869% prover Matita that compiles the submitted formalization. Another possibility
1870% is to backport the development to the last released version of the system
1871% to avoid having to re-compile Matita from scratch.
1872%
1873% The programming and certification style used in the formalization heavily
1874% exploit dependent types. Dependent types are used: 1) to impose invariants
1875% by construction on the data types and operations (e.g. a traces from a state
1876% $s_1$ to a state $s_2$ can be concatenad to a trace from a state
1877% $s_2'$ to a state $s_3$ only if $s_2$ is convertible with $s_2'$); 2)
1878% to state and prove the theorems by using the Russell methodology of
1879% 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.
1880% }, 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
1881% mandatorily on dependent types: it should be easy to adapt the technique
1882% and results presented in the paper to HOL.
1883%
1884% Finally, Matita and Coq are based on minor variations of the Calculus of
1885% (Co)Inductive Constructions. These variations do not affect the CerCo
1886% formalization. Therefore a porting of the proofs and ideas to Coq would be
1887% rather straightforward.
1888
1889\end{document}
Note: See TracBrowser for help on using the repository browser.