source: Papers/itp-2013/ccexec.tex @ 2622

Last change on this file since 2622 was 2622, checked in by sacerdot, 7 years ago


File size: 56.7 KB
10% NB: might be worth removing this if changing class in favour of
11% a built-in definition.
16  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
17   morekeywords={[2]if,then,else,forall,Prop,match,with,end,let},
18  }
21  morekeywords={int8_t}
25        keywordstyle=\color{red}\bfseries,
26        keywordstyle=[2]\color{blue},
27        commentstyle=\color{green},
28        stringstyle=\color{blue},
29        showspaces=false,showstringspaces=false,
30        xleftmargin=1em}
34\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
35Emerging Technologies (FET) programme within the Seventh Framework
36Programme for Research of the European Commission, under FET-Open grant
37number: 243881}}
38\author{Paolo Tranquilli \and Claudio Sacerdoti Coen}
39\institute{Department of Computer Science and Engineering, University of Bologna,\\\email{}, \email{}}
42The labelling approach is a technique to lift cost models for non-functional
43properties of programs from the object code to the source code. It is based
44on the preservation of the structure of the high level program in every
45intermediate language used by the compiler. Such structure is captured by
46observables that are added to the semantics and that needs to be preserved
47by the forward simulation proof of correctness of the compiler. Additional
48special observables are required for function calls. In this paper we
49present a generic forward simulation proof that preserves all these observables.
50The proof statement is based on a new mechanized semantics that traces the
51structure of execution when the language is unstructured. The generic semantics
52and simulation proof have been mechanized in the interactive theorem prover
58The \emph{labelling approach} has been introduced in~\cite{easylabelling} as
59a technique to \emph{lift} cost models for non-functional properties of programs
60from the object code to the source code. Examples of non-functional properties
61are execution time, amount of stack/heap space consumed and energy required for
62communication. The basic idea of the approach is that it is impossible to
63provide a \emph{uniform} cost model for an high level language that is preserved
64\emph{precisely} by a compiler. For instance, two instances of an assignment
65$x = y$ in the source code can be compiled very differently according to the
66place (registers vs stack) where $x$ and $y$ are stored at the moment of
67execution. Therefore a precise cost model must assign a different cost
68to every occurrence, and the exact cost can only be known after compilation.
70According to the labeling approach, the compiler is free to compile and optimize
71the source code without any major restriction, but it must keep trace
72of what happens to basic blocks during the compilation. The cost model is
73then computed on the object code. It assigns a cost to every basic block.
74Finally, the compiler propagates back the cost model to the source level,
75assigning a cost to each basic block of the source code.
77Implementing the labelling approach in a certified compiler
78allows to reason formally on the high level source code of a program to prove
79non-functional properties that are granted to be preserved by the compiler
80itself. The trusted code base is then reduced to 1) the interactive theorem
81prover (or its kernel) used in the certification of the compiler and
822) the software used to certify the property on the source language, that
83can be itself certified further reducing the trusted code base.
84In~\cite{easylabelling} the authors provide an example of a simple
85certified compiler that implements the labelling approach for the
86imperative \texttt{While} language~\cite{while}, that does not have
87pointers and function calls.
89The labelling approach has been shown to scale to more interesting scenarios.
90In particular in~\cite{functionallabelling} it has been applied to a functional
91language and in~\cite{loopoptimizations} it has been shown that the approach
92can be slightly complicated to handle loop optimizations and, more generally,
93program optimizations that do not preserve the structure of basic blocks.
94On-going work also shows that the labelling approach is also compatible with
95the complex analyses required to obtain a cost model for object code
96on processors that implement advanced features like pipelining, superscalar
97architectures and caches.
99In the European Project CerCo (Certified Complexity~\footnote{\url{}})~\cite{cerco} we are certifying a labelling approach based compiler for a large subset of C to
1008051 object code. The compiler is
101moderately optimizing and implements a compilation chain that is largely
102inspired to that of CompCert~\cite{compcert1,compcert2}. Compared to work done in~\cite{easylabelling}, the main novely and source of difficulties is due to the presence
103of function calls. Surprisingly, the addition of function calls require a
104rivisitation of the proof technique given in~\cite{easylabelling}. In
105particular, at the core of the labelling approach there is a forward
106simulation proof that, in the case of \texttt{While}, is only minimally
107more complex than the proof required for the preservation of the
108functional properties only. In the case of a programming language with
109function calls, instead, it turns out that the forward simulation proof for
110the back-end languages must grant a whole new set of invariants.
112In this paper we present a formalization in the Matita interactive theorem
113prover of a generic version of the simulation proof required for unstructured
114languages. All back-end languages of the CerCo compiler are unstructured
115languages, so the proof covers half of the correctness of the compiler.
116The statement of the generic proof is based on a new semantics
117for imperative unstructured languages that is based on \emph{structured
118traces} and that restores the preservation of structure in the observables of
119the semantics. The generic proof allows to almost completely split the
120part of the simulation that deals with functional properties only from the
121part that deals with the preservation of structure.
123The plan of this paper is the following. In Section~\ref{labelling} we
124sketch the labelling method and the problems derived from the application
125to languages with function calls. In Section~\ref{semantics} we introduce
126a generic description of an unstructured imperative language and the
127corresponding structured traces (the novel semantics). In
128Section~\ref{simulation} we describe the forward simulation proof.
129Conclusions and future works are in Section~\ref{conclusions}
131\section{The labelling approach}
133We briefly sketch here a simplified version of the labelling approach as
134introduced in~\cite{easylabelling}. The simplification strengthens the
135sufficient conditions given in~\cite{easylabelling} to allow a simpler
136explanation. The simplified conditions given here are also used in the
137CerCo compiler to simplify the proof.
139Let $\mathcal{P}$ be a programming language whose semantics is given in
140terms of observables: a run of a program yields a finite or infinite
141stream of observables. We also assume for the time being that function
142calls are not available in $\mathcal{P}$. We want to associate a cost
143model to a program $P$ written in $\mathcal{P}$. The first step is to
144extend the syntax of $\mathcal{P}$ with a new construct $\texttt{emit L}$
145where $L$ is a label distinct from all observables of $\mathcal{P}$.
146The semantics of $\texttt{emit L}$ is the emission of the observable
147\texttt{L} that is meant to signal the beginning of a basic block.
149There exists an automatic procedure that injects into the program $P$ an
150$\texttt{emit L}$ at the beginning of each basic block, using a fresh
151\texttt{L} for each block. In particular, the bodies of loops, both branches
152of \texttt{if-then-else}s and the targets of \texttt{goto}s must all start
153with an emission statement.
155Let now $C$ be a compiler from $\mathcal{P}$ to the object code $\mathcal{M}$,
156that is organized in passes. Let $\mathcal{Q}_i$ be the $i$-th intermediate
157language used by the compiler. We can easily extend every
158intermediate language (and its semantics) with an $\texttt{emit L}$ statement
159as we did for $\mathcal{P}$. The same is possible for $\mathcal{M}$ too, with
160the additional difficulty that the syntax of object code is given as a
161sequence of bytes. The injection of an emission statement in the object code
162can be done using a map that maps two consecutive code addresses with the
163statement. The intended semantics is that, if $(pc_1,pc_2) \mapsto \texttt{emit L}$ then the observable \texttt{L} is emitted after the execution of the
164instruction stored at $pc_1$ and before the execution of the instruction
165stored at $pc_2$. The two program counters are necessary because the
166instruction stored at $pc_1$ can have multiple possible successors (e.g.
167in case of a conditional branch or an indirect call). Dually, the instruction
168stored at $pc_2$ can have multiple possible predecessors (e.g. if it is the
169target of a jump).
171The compiler, to be functionally correct, must preserve the observational
172equivalence, i.e. executing the program after each compiler pass should
173yield the same stream of observables. After the injection of emission
174statements, observables now capture both functional and non-functional
176This correctness property is called in the litterature a forward simulation
177and is sufficient for correctness when the target language is
179We also require a stronger, non-functional preservation property: after each
180pass all basic blocks must start with an emission statement, and all labels
181\texttt{L} must be unique.
183Now let $M$ be the object code obtained for the program $P$. Let us suppose
184that we can statically inspect the code $M$ and associate to each basic block
185a cost (e.g. the number of clock cycles required to execute all instructions
186in the basic block, or an upper bound to that time). Every basic block is
187labelled with an unique label \texttt{L}, thus we can actually associate the
188cost to \texttt{L}. Let call it $k(\texttt{L})$.
190The function $k$ is defined as the cost model for the object code control
191blocks. It can be equally used as well as the cost model for the source
192control blocks. Indeed, if the semantics of $P$ is the stream
193$L_1 L_2 \ldots$, then, because of forward simulation, the semantics of $M$ is
194also $L_1 L_2 \ldots$ and its actual execution cost is $\Sigma_i k(L_i)$ because
195every instruction belongs to a control block and every control block is
196labelled. Thus it is correct to say that the execution cost of $P$ is also
197$\Sigma_i k(L_i)$. In other words, we have obtained a cost model $k$ for
198the blocks of the high level program $P$ that is preserved by compilation.
200How can the user profit from the high level cost model? Suppose, for instance,
201that he wants to prove that the WCET of his program is bounded by $c$. It
202is sufficient for him to prove that $\Sigma_i k(L_i) \leq c$, which is now
203a purely functional property of the code. He can therefore use any technique
204available to certify functional properties of the source code.
205What is suggested in~\cite{easylabelling} is to actually instrument the
206source code $P$ by replacing every label emission statement
207$\texttt{emit L}$ with the instruction $\texttt{cost += k(L)}$ that increments
208a global fresh variable \texttt{cost}. The bound is now proved by establishing
209the program invariant $\texttt{cost} \leq c$, which can be done for example
210using the Frama-C~\cite{framaC} suite if the source code is some variant of
213\subsection{Labelling function calls}
214We now want to extend the labelling approach to support function calls.
215On the high level, \emph{structured} programming language $\mathcal{P}$ there
216is not much to change.
217When a function is invoked, the current basic block is temporarily exited
218and the basic block the function starts with take control. When the function
219returns, the execution of the original basic block is resumed. Thus the only
220significant change is that basic blocks can now be nested. Let \texttt{E}
221be the label of the external block and \texttt{I} the label of a nested one.
222Since the external starts before the internal, the semantics observed will be
223\texttt{E I} and the cost associated to it on the source language will be
224$k(\texttt{E}) + k(\texttt{I})$, i.e. the cost of executing all instructions
225in the block \texttt{E} first plus the cost of executing all the instructions in
226the block \texttt{I}. However, we know that some instructions in \texttt{E} are
227executed after the last instruction in \texttt{I}. This is actually irrelevant
228because we are here assuming that costs are additive, so that we can freely
229permute 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
230the function call terminates and yields back control to the basic block
231\texttt{E}. If the call diverges, the instrumentation
232$\texttt{cost += k(E)}$ executed at the beginning of \texttt{E} is still valid,
233but just as an upper bound to the real execution cost: only precision is lost.
235Let now consider what happens when we move down the compilation chain to an
236unstructured intermediate or final language. Here unstructured means that
237the only control operators are conditional and unconditional jumps, function
238calls and returns. Unlike a structured language, though, there is no guarantee
239that a function will return control just after the function call point.
240The semantics of the return statement, indeed, consists in fetching the
241return address from some internal structure (tipically the control stack) and
242jumping directly to it. The code can freely manipulate the control stack to
243make the procedure returns to whatever position. Indeed, it is also possible
244to break the well nesting of function calls/returns.
246Is it the case that the code produced by a correct compiler must respect the
247additional property that every function returns just after its function call
248point? The answer is negative and the property is not implied by forward
249simulation proofs. For instance, imagine to modify a correct compiler pass
250by sistematically adding one to the return address on the stack and by
251putting a \texttt{NOP} (or any other instruction that takes one byte) after
252every function call. The obtained code will be functionally indistinguishable,
253and the added instructions will all be dead code.
255This lack of structure in the semantics badly interferes with the labelling
256approach. The reason is the following: when a basic block labelled with
257\texttt{E} contains a function call, it no longer makes any sense to associate
258to a label \texttt{E} the sum of the costs of all the instructions in the block.
259Indeed, there is no guarantee that the function will return into the block and
260that the instructions that will be executed after the return will be the ones
261we are paying for in the cost model.
263How can we make the labelling approach work in this scenario? We only see two
264possible ways. The first one consists in injecting an emission statement after
265every function call: basic blocks no longer contain function calls, but are now
266terminated by them. This completely solves the problem and allows the compiler
267to break the structure of function calls/returns at will. However, the
268technique has several drawbacks. First of all, it greatly augments the number
269of cost labels that are injected in the source code and that become
270instrumentation statements. Thus, when reasoning on the source code to prove
271non-functional properties, the user (or the automation tool) will have to handle
272larger expressions. Second, the more labels are emitted, the more difficult it
273becomes to implement powerful optimizations respecting the code structure.
274Indeed, function calls are usually implemented in such a way that most registers
275are preserved by the call, so that the static analysis of the block is not
276interrupted by the call and an optimization can involve both the code before
277and after the function call. Third, instrumenting the source code may require
278unpleasant modification of it. Take, for example, the code
279\texttt{f(g(x));}. We need to inject an emission statement/instrumentation
280instruction just after the execution of \texttt{g}. The only way to do that
281is to rewrite the code as \texttt{y = g(x); emit L; f(y);} for some fresh
282variable \texttt{y}. It is pretty clear how in certain situations the obtained
283code would be more obfuscated and then more difficult to manually reason on.
285For the previous reasons, in this paper and in the CerCo project we adopt a
286different approach. We do not inject emission statements after every
287function call. However, we want to propagate a strong additional invariant in
288the forward simulation proof. The invariant is the propagation of the structure
289 of the original high level code, even if the target language is unstructured.
290The structure we want to propagate, that will become more clear in the next
291section, comprises 1) the property that every function should return just after
292the function call point, which in turns imply well nesting of function calls;
2932) the property that every basic block starts with a code emission statement.
295In the original labelling approach of~\cite{easylabelling}, the second property
296was granted syntactically as a property of the generated code.
297In our revised approach, instead, we will impose the property on the runs:
298it will be possible to generate code that does not respect the syntactic
299property, as soon as all possible runs respect it. For instance, dead code will no longer
300be required to have all basic blocks correctly labelled. The switch is suggested
301from the fact that the first of the two properties --- that related to
302function calls/returns --- can only be defined as property of runs,
303not of the static code. The switch is
304beneficial to the proof because the original proof was made of two parts:
305the forward simulation proof and the proof that the static property was granted.
306In our revised approach the latter disappears and only the forward simulation
307is kept.
309In order to capture the structure semantics so that it is preserved
310by a forward simulation argument, we need to make the structure observable
311in the semantics. This is the topic of the next section.
313\section{Structured traces}
315The program semantics adopted in the traditional labelling approach is based
316on labelled deductive systems. Given a set of observables $\mathcal{O}$ and
317a set of states $\mathcal{S}$, the semantics of one deterministic execution
318step is
319defined as a function $S \to S \times O^*$ where $O^*$ is a (finite) stream of
320observables. The semantics is then lifted compositionally to multiple (finite
321or infinite) execution steps.
322Finally, the semantics of a a whole program execution is obtained by forgetting
323about the final state (if any), yielding a function $S \to O^*$ that given an
324initial status returns the finite or infinite stream of observables in output.
326We present here a new definition of semantics where the structure of execution,
327as defined in the previous section, is now observable. The idea is to replace
328the stream of observables with a structured data type that makes explicit
329function call and returns and that grants some additional invariants by
330construction. The data structure, called \emph{structured traces}, is
331defined inductively for terminating programs and coinductively for diverging
332ones. In the paper we focus only on the inductive structure, i.e. we assume
333that all programs that are given a semantics are total. The Matita formalization
334also shows the coinductive definitions. The semantics of a program is then
335defined as a function that maps an initial state into a structured trace.
337In order to have a definition that works on multiple intermediate languages,
338we abstract the type of structure traces over an abstract data type of
339abstract statuses:
341record abstract_status := \{ S: Type[0];
342 as_execute: S \(\to\) S \(\to\) Prop;     as_classify: S \(\to\) classification;
343 as_costed: S \(\to\) Prop;      as_label: \(\forall\) s. as_costed S s \(\to\) label;
344 as_call_ident: \(\forall\) s. as_classify S s = cl_call \(\to\) label;
345 as_after_return:
346  (\(\Sigma\)s:as_status. as_classify s = Some ? cl_call) \(\to\) as_status \(\to\) Prop \}
348The predicate $\texttt{as\_execute}~s_1~s_2$ holds if $s_1$ evolves into
349$s_2$ in one step;\\ $\texttt{as\_classify}~s~c$ holds if the next instruction
350to be executed in $s$ is classified according to $c \in
351\{\texttt{cl\_return,cl\_jump,cl\_call,cl\_other}\}$ (we omit tailcalls for simplicity);
352the predicate $\texttt{as\_costed}~s$ holds if the next instruction to be
353executed in $s$ is a cost emission statement (also classified
354as \texttt{cl\_other}); finally $(\texttt{as\_after\_return}~s_1~s_2)$ holds
355if the next instruction to be executed in $s_2$ follows the function call
356to be executed in (the witness of the $\Sigma$-type) $s_1$.
359The inductive type for structured traces is actually made by three multiple
360inductive types with the following semantics:
362 \item $(\texttt{trace\_label\_return}~s_1~s_2)$ is a trace that begins in
363   the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
364   such that the instruction to be executed in $s_1$ is a label emission
365   statement and the one to be executed in the state before $s_2$ is a return
366   statement. Thus $s_2$ is the state after the return. The trace
367   may contain other label emission statements. It captures the structure of
368   the execution of function bodies: they must start with a cost emission
369   statement and must end with a return; they are obtained by concatenating
370   one or more basic blocks, all starting with a label emission
371   (e.g. in case of loops).
372 \item $(\texttt{trace\_any\_label}~b~s_1~s_2)$ is a trace that begins in
373   the state $s_1$ (included) and ends just before the state $s_2$ (excluded)
374   such that the instruction to be executed in $s_2$/in the state before
375   $s_2$ is either a label emission statement or
376   or a return, according to the boolean $b$. It must not contain
377   any label emission statement. It captures the notion of a suffix of a
378   basic block.
379 \item $(\texttt{trace\_label\_label}~b~s_1~s_2)$ is the special case of
380   $(\texttt{trace\_any\_label}~b~s_1~s_2)$ such that the instruction to be
381   executed in $s_1$ is a label emission statement. It captures the notion of
382   a basic block.
386 {\texttt{trace\_label\_label}~true~s_1~s_2}
387 {\texttt{trace\_label\_return}~s_1~s_2}
390 {\texttt{trace\_label\_label}~false~s_1~s_2 \andalso
391  \texttt{trace\_label\_return}~s_2~s_3
392 }
393 {\texttt{trace\_label\_return}~s_1~s_3}
396 {\texttt{trace\_any\_label}~b~s_1~s_2 \andalso
397  \texttt{as\_costed}~s_1
398 }
399 {\texttt{trace\_label\_label}~b~s_1~s_2}
402 {\texttt{as\_execute}~s_1~s_2 \andalso
403  \texttt{as\_classify}~s_1 \in \{\texttt{cl\_jump,cl\_other}\} \andalso
404  \texttt{as\_costed}~s_2
405 }
406 {\texttt{trace\_any\_label}~false~s_1~s_2}
409 {\texttt{as\_execute}~s_1~s_2 \andalso
410  \texttt{as\_classify}~s_1 = \texttt{cl\_return} \\
411 }
412 {\texttt{trace\_any\_label}~true~s_1~s_2}
415 {\texttt{as\_execute}~s_1~s_2 \andalso
416  \texttt{as\_classify}~s_1 = \texttt{cl\_call} \\
417  \texttt{as\_after\_return}~s_1~s_3 \andalso
418  \texttt{trace\_label\_return}~s_2~s_3 \andalso
419  \texttt{as\_costed}~s_3
420 }
421 {\texttt{trace\_any\_label}~false~s_1~s_3}
424 {\texttt{as\_execute}~s_1~s_2 \andalso
425  \texttt{as\_classify}~s_1 = \texttt{cl\_call} \\
426  \texttt{as\_after\_return}~s_1~s_3 \andalso
427  \texttt{trace\_label\_return}~s_2~s_3 \\
428  \lnot \texttt{as\_costed}~s_3 \andalso
429  \texttt{trace\_any\_label}~b~s_3~s_4
430 }
431 {\texttt{trace\_any\_label}~b~s_1~s_4}
434 {\texttt{as\_execute}~s_1~s_2 \andalso
435  \lnot \texttt{as\_costed}~s_2 \\
436  \texttt{trace\_any\_label}~b~s_2~s_3
437  \texttt{as\_classify}~s_1 = \texttt{cl\_other}
438 }
439 {\texttt{trace\_any\_label}~b~s_1~s_3}
444inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
445  | tlr_base:
446      ∀status_before: S.
447      ∀status_after: S.
448        trace_label_label S ends_with_ret status_before status_after →
449        trace_label_return S status_before status_after
450  | tlr_step:
451      ∀status_initial: S.
452      ∀status_labelled: S.
453      ∀status_final: S.
454        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
455        trace_label_return S status_labelled status_final →
456          trace_label_return S status_initial status_final
457with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
458  | tll_base:
459      ∀ends_flag: trace_ends_with_ret.
460      ∀start_status: S.
461      ∀end_status: S.
462        trace_any_label S ends_flag start_status end_status →
463        as_costed S start_status →
464          trace_label_label S ends_flag start_status end_status
465with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
466  (* Single steps within a function which reach a label.
467     Note that this is the only case applicable for a jump. *)
468  | tal_base_not_return:
469      ∀start_status: S.
470      ∀final_status: S.
471        as_execute S start_status final_status →
472        (as_classifier S start_status cl_jump ∨
473         as_classifier S start_status cl_other) →
474        as_costed S final_status →
475          trace_any_label S doesnt_end_with_ret start_status final_status
476  | tal_base_return:
477      ∀start_status: S.
478      ∀final_status: S.
479        as_execute S start_status final_status →
480        as_classifier S start_status cl_return →
481          trace_any_label S ends_with_ret start_status final_status
482  (* A call followed by a label on return. *)
483  | tal_base_call:
484      ∀status_pre_fun_call: S.
485      ∀status_start_fun_call: S.
486      ∀status_final: S.
487        as_execute S status_pre_fun_call status_start_fun_call →
488        ∀H:as_classifier S status_pre_fun_call cl_call.
489          as_after_return S «status_pre_fun_call, H» status_final →
490          trace_label_return S status_start_fun_call status_final →
491          as_costed S status_final →
492            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
493  (* A call followed by a non-empty trace. *)
494  | tal_step_call:
495      ∀end_flag: trace_ends_with_ret.
496      ∀status_pre_fun_call: S.
497      ∀status_start_fun_call: S.
498      ∀status_after_fun_call: S.
499      ∀status_final: S.
500        as_execute S status_pre_fun_call status_start_fun_call →
501        ∀H:as_classifier S status_pre_fun_call cl_call.
502          as_after_return S «status_pre_fun_call, H» status_after_fun_call →
503          trace_label_return S status_start_fun_call status_after_fun_call →
504          ¬ as_costed S status_after_fun_call →
505          trace_any_label S end_flag status_after_fun_call status_final →
506            trace_any_label S end_flag status_pre_fun_call status_final
507  | tal_step_default:
508      ∀end_flag: trace_ends_with_ret.
509      ∀status_pre: S.
510      ∀status_init: S.
511      ∀status_end: S.
512        as_execute S status_pre status_init →
513        trace_any_label S end_flag status_init status_end →
514        as_classifier S status_pre cl_other →
515        ¬ (as_costed S status_init) →
516          trace_any_label S end_flag status_pre status_end.
519A \texttt{trace\_label\_return} is isomorphic to a list of
520\texttt{trace\_label\_label}s that end with a cost emission followed by a
521\texttt{trace\_label\_label} that ends with a return.
523The interesting cases are those of $(\texttt{trace\_any\_label}~b~s_1~s_2)$.
524A \texttt{trace\_any\_label} is a sequence of steps built by a syntax directed
525definition on the classification of $s_1$. The constructors of the datatype
526impose several invariants that are meant to impose a structure to the
527otherwise unstructured execution. In particular, the following invariants are
530 \item the trace is never empty; it ends with a return iff $b$ is
531       true (\texttt{ends\_with\_ret})
532 \item a jump must always be the last instruction of the trace, and it must
533       be followed by a cost emission statement; i.e. the target of a jump
534       is always the beginning of a new basic block; as such it must start
535       with a cost emission statement
536 \item a cost emission statement can never occur inside the trace, only in
537       the status immediately after
538 \item the trace for a function call step is made from a subtrace of type
539       $(\texttt{trace\_label\_return}~s_1~s_2)$, possibly followed by the
540       rest of the trace for this basic block. The subtrace represents the
541       function execution. Being an inductive datum, it grants totality of
542       the function call. The status $s_2$ is the one that follows the return
543       statement. The next instruction of $s_2$ must follow the function call
544       instruction. As a consequence, function calls are also well nested.
547The three mutual structural recursive functions \texttt{flatten\_trace\_label\_return, flatten\_trace\_label\_label} and \texttt{flatten\_trance\_any\_label}
548allow to extract from a structured trace the list of states whose next
549instruction is a cost emission statement. We only show here the type of one
550of them:
553  (S: abstract_status)
554    (start_status: S) (final_status: S)
555      (the_trace: trace_label_return S start_status final_status)
556        on the_trace: list (as_cost_label S)
559\paragraph{Cost prediction on structured traces}
561The first main theorem of CerCo about structured traces
562(theorem \texttt{compute\_max\_trace\_label\_return\_cost\_ok\_with\_trace})
563holds for the
565of the structured traces to the concrete status of object code programs.
566Simplifying a bit, it states that
567$\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.
568  clock~s_2 = clock~s_1 + \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau} k(L(s))$ where $L$ maps a labelled state to its emitted label, and the
569cost model $k$ is statically computed from the object code
570by associating to each label \texttt{L} the sum of the cost of the instructions
571in the basic block that starts at \texttt{L} and ends before the next labelled
572instruction. The theorem is proved by structural induction over the structured
573trace, and is based on the invariant that
574iff the function that computes the cost model has analyzed the instruction
575to be executed at $s_2$ after the one to be executed at $s_1$, and if
576the structured trace starts with $s_1$, then eventually it will contain also
577$s_2$. When $s_1$ is not a function call, the result holds trivially because
578of the $(\texttt{as\_execute}~s_1~s_2)$ condition obtained by inversion on
579the trace. The only non
580trivial case is the one of function calls: the cost model computation function
581does recursion on the first instruction that follows that function call; the
582\texttt{as\_after\_return} condition of the \texttt{tal\_base\_call} and
583\texttt{tal\_step\_call} grants exactly that the execution will eventually reach
584this state.
586\paragraph{Structured traces similarity and cost prediction invariance}
588A compiler pass maps source to object code and initial states to initial
589states. The source code and initial state uniquely determine the structured
590trace of a program, if it exists. The structured trace fails to exists iff
591the structural conditions are violated by the program execution (e.g. a function
592body does not start with a cost emission statement). Let us assume that the
593target structured trace exists.
595What is the relation between the source and target structured traces?
596In general, the two traces can be arbitrarily different. However, we are
597interested only in those compiler passes that maps a trace $\tau_1$ to a trace
598$\tau_2$ such that
599\begin{displaymath}(\texttt{flatten\_trace\_label\_return}~\tau_1 = \texttt{flatten\_trace\_label\_return}~\tau_2)\label{condition1}\end{displaymath}
600The reason is that when this happens we obviously have the
601following corollary to the previous theorem:
602$$\forall s_1,s_2. \forall \tau: \texttt{trace\_label\_return}~s_1~s_2.
603  clock~s_2 - clock~s_1 = \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau_1} k(L(s)) = \Sigma_{s \in \texttt{flatten\_trace\_label\_return}~\tau_2} k(L(s))$$
604The 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
605transfer the cost model from the target to the source code and reason on the
606source code only.
608We are therefore interested in conditions stronger than~\ref{condition1}.
609Therefore we introduce here a similarity relation between traces that captures
610the fact that two traces have the same structure and that
611implies~\ref{condition1} (theorem \texttt{tlr\_rel\_to\_traces\_same\_flatten}). Two traces are similar when one can be obtained from
612the other by erasing or inserting steps classified as \texttt{other} into the
613\texttt{trace\_any\_label} blocks of the trace. In particular,
614the relation maps function calls to function calls to the same function,
615label emission statements to emissions of the same label, concatenation of
616subtraces to concatenation of subtraces of the same lenghth and starting with
617the same emissione statement, etc.
619The similarity relation definition if simple, but it involves a large
620number of cases. In the formalization, we define
621$(\texttt{tlr\_rel}~tlr_1~tlr_2)$ by structural recursion on $tlr_1$ and pattern
622matching over $tlr_2$. Here we turn
623the definition into inference rules for the sake of readability. We also
624omit from trace constructors all arguments, but those that are traces or that
625are used in the premises of the rules.
628 {\texttt{tll\_rel}~tll_1~tll_2
629 }
630 {\texttt{tlr\_rel}~(\texttt{tlr\_base}~tll_1)~(\texttt{tlr\_base}~tll_2)}
633 {\texttt{tll\_rel}~tll_1~tll_2 \andalso
634  \texttt{tlr\_rel}~tlr_1~tlr_2
635 }
636 {\texttt{tlr\_rel}~(\texttt{tlr\_step}~tll_1~tlr_1)~(\texttt{tlr\_step}~tll_2~tlr_2)}
639 {\texttt{as\_label}~H_1 = \texttt{as\_label}~H_2 \andalso
640  \texttt{tal\_rel}~tal_1~tal_2
641 }
642 {\texttt{tll\_rel}~(\texttt{tll\_base}~tal_1~H_1)~(\texttt{tll\_base}~tal_2~H_2)}
645 {}
646 {\texttt{tal\_rel}~\texttt{tal\_base\_not\_return}~(taa @ \texttt{tal\_base\_not\_return}}
649 {}
650 {\texttt{tal\_rel}~\texttt{tal\_base\_return}~(taa @ \texttt{tal\_base\_return}}
653 {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
654  \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2
655 }
656 {\texttt{tal\_rel}~(\texttt{tal\_base\_call}~H_1~tlr_1)~(taa @ \texttt{tal\_base\_call}~H_2~tlr_2)}
659 {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
660  \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2 \andalso
661  \texttt{tal\_collapsable}~tal_2
662 }
663 {\texttt{tal\_rel}~(\texttt{tal\_base\_call}~tlr_1)~(taa @ \texttt{tal\_step\_call}~tlr_2~tal_2)}
666 {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
667  \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2 \andalso
668  \texttt{tal\_collapsable}~tal_1
669 }
670 {\texttt{tal\_rel}~(\texttt{tal\_step\_call}~tlr_1~tal_1)~(taa @ \texttt{tal\_base\_call}~tlr_2)}
673 {\texttt{tlr\_rel}~tlr_1~tlr_2 \andalso
674  \texttt{tal\_rel}~tal_1~tal_2 \andalso
675  \texttt{as\_call\_ident}~H_1 = \texttt{as\_call\_ident}~H_2
676 }
677 {\texttt{tal\_rel}~(\texttt{tal\_step\_call}~tlr_1~tal_1)~(taa @ \texttt{tal\_step\_call}~tlr_2~tal_2)}
680 {\texttt{tal\_rel}~tal_1~tal_2
681 }
682 {\texttt{tal\_rel}~(\texttt{tal\_step\_default}~tal_1)~tal_2}
685let rec tlr_rel S1 st1 st1' S2 st2 st2'
686  (tlr1 : trace_label_return S1 st1 st1')
687  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
688match tlr1 with
689  [ tlr_base st1 st1' tll1 ⇒
690    match tlr2 with
691    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
692    | _ ⇒ False
693    ]
694  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
695    match tlr2 with
696    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
697      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
698    | _ ⇒ False
699    ]
700  ]
701and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
702 (tll1 : trace_label_label S1 fl1 st1 st1')
703 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
704  match tll1 with
705  [ tll_base fl1 st1 st1' tal1 H ⇒
706    match tll2 with
707    [ tll_base fl2 st2 st2 tal2 G ⇒
708      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
709      tal_rel … tal1 tal2
710    ]
711  ]
712and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
713 (tal1 : trace_any_label S1 fl1 st1 st1')
714 (tal2 : trace_any_label S2 fl2 st2 st2')
715   on tal1 : Prop ≝
716  match tal1 with
717  [ tal_base_not_return st1 st1' _ _ _ ⇒
718    fl2 = doesnt_end_with_ret ∧
719    ∃st2mid,taa,H,G,K.
720    tal2 ≃ taa_append_tal ? st2 ??? taa
721      (tal_base_not_return ? st2mid st2' H G K)
722  | tal_base_return st1 st1' _ _ ⇒
723    fl2 = ends_with_ret ∧
724    ∃st2mid,taa,H,G.
725    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
726      (tal_base_return ? st2mid st2' H G)
727  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒
728    fl2 = doesnt_end_with_ret ∧
729    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
730    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
731    (* we must allow a tal_base_call to be similar to a call followed
732      by a collapsable trace (trace_any_any followed by a base_not_return;
733      we cannot use trace_any_any as it disallows labels in the end as soon
734      as it is non-empty) *)
735    (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
736      tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
737    ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
738    ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
739      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
740      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
741  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
742    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
743    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
744    (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
745      tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
746      tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
747    ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
748    ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
749      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
750      tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
751  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
752    tal_rel … tl1 tal2 (* <- this makes it many to many *)
753  ].
757In the preceding rules, a $taa$ is an inhabitant of the
758$(\texttt{trace\_any\_any}~s_1~s_2)$ inductive data type whose definition
759we do not give in the paper for lack of space. It is the type of valid
760prefixes (even empty ones) of \texttt{trace\_any\_label}s that do not contain
761any function call. Therefore it
762is possible to concatenate (using ``$@$'') a \texttt{trace\_any\_any} to the
763left of a \texttt{trace\_any\_label}. The intuition is that two traces are
764similar if one of them can perform more silent (non observables) moves,
765whose sequences are here represented by \texttt{trace\_any\_any}.
767The \texttt{tal\_collapsable} unary predicate over \texttt{trace\_any\_label}s
768holds when the argument does not contain any function call and it ends
769with a label (not a return). The intuition is that after a function call we
770can still perform a sequence of silent actions while remaining similar.
772\section{Forward simulation}
775We summarize here the results of the previous sections. Each intermediate
776unstructured language can be given a semantics based on structured traces,
777that single out those runs that respect a certain number of invariants.
778A cost model can be computed on the object code and it can be used to predict
779the execution costs of runs that produce structured traces. The cost model
780can be lifted from the target to the source code of a pass if the pass maps
781structured traces to similar structured traces. The latter property is called
782a \emph{forward simulation}.
784As for labelled transition systems, in order to establish the forward
785simulation we are interested in (preservation of observables), we are
786forced to prove a stronger notion of forward simulation that introduces
787an explicit relation between states. The classical notion of a 1-to-0-or-many
788forward simulation is the existence of a relation $R$ over states such that
789if $s_1 R s_2$ and $s_1 \to^1 s_1'$ then there exists an $s_2'$ such that
790$s_1' \to^* s_2'$ and $s_1' R s_2'$. In our context, we need to replace the
791one and multi step transition relations $\to^n$ with the existence of
792a structured trace between the two states, and we need to add the request that
793the two structured traces are similar. Thus what we would like to state is
794something like:\\
795for all $s_1,s_2,s_1'$ such that there is a $\tau_1$ from
796$s_1$ to $s_1'$ and $s_1 R s_2$ there exists an $s_2'$ such that
797$s_1' R s_2'$ and a $\tau_2$ from $s_2$ to $s_2'$ such that
798$\tau_1 \approx \tau_2$.\\
800The statement just introduced, however, is too simplicistic and not provable
801in the general case. To understand why, consider the case of a function call
802and the pass that fixes the parameter passing conventions. A function
803call 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 call has no
804input nor output parameters. The pass must add explicit code before and after
805the function call to move the pseudo-registers content from/to the hardware
806registers or the stack in order to implement the parameter passing strategy.
807Similarly, each function body must be augmented with a preamble and a postamble
808to complete/initiate the parameter passing strategy for the call/return phase.
809Therefore what used to be a call followed by the next instruction to execute
810after the function return, now becomes a sequence of instructions, followed by
811a call, followed by another sequence. The two states at the beginning of the
812first sequence and at the end of the second sequence are in relation with
813the status before/after the call in the source code, like in an usual forward
814simulation. How can we prove however the additional condition for function calls
815that asks that when the function returns the instruction immediately after the
816function call is called? To grant this invariant, there must be another relation
817between the address of the function call in the source and in the target code.
818This additional relation is to be used in particular to relate the two stacks.
820Another example is given by preservation of code emission statements. A single
821code emission instruction can be simulated by a sequence of steps, followed
822by a code emission, followed by another sequence. Clearly the initial and final
823statuses of the sequence are to be in relation with the status before/after the
824code emission in the source code. In order to preserve the structured traces
825invariants, however, we must consider a second relation between states that
826traces the preservation of the code emission statement.
828Therefore we now introduce an abstract notion of relation set between abstract
829statuses and an abstract notion of 1-to-0-or-many forward simulation. These
830two definitions enjoy the following remarkable properties:
832 \item they are generic enough to accomodate all passes of the CerCo compiler
833 \item they allow to lift the 1-to-0-or-many forward simulation to the
834   structured traces preserving forward simulation we are interested in
837The latter lifting is proved by the following theorem which has the
8381-to-0-or-many forward simulation statement as an hypothesis. Combined with
839the results in the previous section, it has as a corollary that the cost
840model can be computed on the object code and lifted to the source code to
841reason on non-functional properties iff a simpler 1-to-0-or-many forward
842simulation is proved. The statement of the latter is way more complex than a
843traditional 1-to-0-or-many forward simulation statement, but proofs have now
844about the same complexity. Indeed, it should be possible to largely reuse an
845existent traditional forward simulation proof. The lifting theorem below,
846proved once and for all in this paper, is the one that does all the job to
847put the labelling approach in motion.
849\begin{condition}[Cases \texttt{cl\_other} and \texttt{cl\_jump}]
850 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$, and
851 $\texttt{as\_execute}~s_1~s_1'$, and $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ or $\texttt{as\_classify}~s_1 = \texttt{cl\_other}$ and
852$(\texttt{as\_costed}~s_1')$, there exists an $s_2'$ and a $taaf$ of type $(\texttt{trace\_any\_any\_free}~s_2~s_2')$ such that $s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
853$taaf$ is non empty, or one among $s_1$ and $s_1'$ is \texttt{as\_costed}.
856In the above condition, a $(\texttt{trace\_any\_any\_free}~s_1~s_2)$ is an
857inductive type of structured traces that do not contain function calls or
858cost emission statements. Differently from a \texttt{trace\_any\_any}, the
859instruction to be executed in the lookahead state $s_2$ may be a cost emission
862The intuition of the condition is that one step can be replaced with zero or more steps if it
863preserves the relation between the data and if the two final statuses are
864labelled in the same way. Moreover, we must take special care of the empty case
865to avoid collapsing two consecutive states that emit the same label to just
866one state, missing one of the two emissions.
868\begin{condition}[Case \texttt{cl\_call}]
869 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
870 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_call}$, there exists $s_2', s_b, s_a$, a $taa_1$ of type
871$(\texttt{trace\_any\_any}~s_2~s_b)$, a $taa_2$ of type
872$(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
873$s_a$ is classified as a \texttt{cl\_call}, the \texttt{as\_identifiers} of
874the two call states are the same, $s_1 \mathcal{C} s_b$, the predicate
875$(\texttt{as\_execute}~s_b~s_a)$ holds, $s_1' \mathcal{L} s_b$ and
876$s_1' \mathcal{S} s_2'$.
879The condition says that, to simulate a function call, we can perform a
880sequence of silent actions before and after the function call itself.
881The old and new call states must be $\mathcal{C}$-related, the old and new
882states at the beginning of the function execution must be $\mathcal{L}$-related
883and, finally, the two initial and final states must be $\mathcal{S}$-related
884as usual.
886\begin{condition}[Case \texttt{cl\_return}]
887 For all $s_1,s_1',s_2$ such that $s_1 \mathcal{S} s_1'$ and
888 $\texttt{as\_execute}~s_1~s_1'$ and $\texttt{as\_classify}~s_1 = \texttt{cl\_return}$, there exists $s_2', s_b, s_a$, a $taa$ of type
889$(\texttt{trace\_any\_any}~s_2~s_b)$, a $taaf$ of type
890$(\texttt{trace\_any\_any\_free}~s_a~s_2')$ such that:
891$s_a$ is classified as a \texttt{cl\_return},
892$s_1 \mathcal{C} s_b$, the predicate
893$(\texttt{as\_execute}~s_b~s_a)$ holds,
894$s_1' \mathcal{R} s_a$ and
895$s_1' (\mathcal{S} \cap \mathcal{L}) s_2'$ and either
896$taaf$ is non empty, or $s_a$ is not \texttt{as\_costed}.
899Similarly to the call condition, to simulate a return we can perform a
900sequence of silent actions before and after the return statement itself.
901The old and the new statements after the return must be $\mathcal{R}$-related,
902to grant that they returned to corresponding calls.
903The two initial and final states must be $\mathcal{S}$-related
904as usual and, moreover, they must exhibit the same labels. Finally, when
905the suffix is non empty we must take care of not inserting a new
906unmatched cost emission statement just after the return statement.
910definition status_simulation ≝
911  λS1 : abstract_status.
912  λS2 : abstract_status.
913  λsim_status_rel : status_rel S1 S2.
914    ∀st1,st1',st2.as_execute S1 st1 st1' →
915    sim_status_rel st1 st2 →
916    match as_classify … st1 with
917    [ None ⇒ True
918    | Some cl ⇒
919      match cl with
920      [ cl_call ⇒ ∀prf.
921        (*
922             st1' ------------S----------\
923              ↑ \                         \
924             st1 \--L--\                   \
925              | \       \                   \
926              S  \-C-\  st2_after_call →taa→ st2'
927              |       \     ↑
928             st2 →taa→ st2_pre_call
929        *)
930        ∃st2_pre_call.
931        as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧
932        call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧
933        ∃st2_after_call,st2'.
934        ∃taa2 : trace_any_any … st2 st2_pre_call.
935        ∃taa2' : trace_any_any … st2_after_call st2'.
936        as_execute … st2_pre_call st2_after_call ∧
937        sim_status_rel st1' st2' ∧
938        label_rel … st1' st2_after_call
939      | cl_return ⇒
940        (*
941             st1
942            / ↓
943           | st1'----------S,L------------\
944           S   \                           \
945            \   \-----R-------\            |     
946             \                 |           |
947             st2 →taa→ st2_ret |           |
948                          ↓   /            |
949                     st2_after_ret →taaf→ st2'
951           we also ask that st2_after_ret be not labelled if the taaf tail is
952           not empty
953        *)
954        ∃st2_ret,st2_after_ret,st2'.
955        ∃taa2 : trace_any_any … st2 st2_ret.
956        ∃taa2' : trace_any_any_free … st2_after_ret st2'.
957        (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧
958        as_classifier … st2_ret cl_return ∧
959        as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧
960        ret_rel … sim_status_rel st1' st2_after_ret ∧
961        label_rel … st1' st2'
962      | cl_other ⇒
963          (*         
964          st1 → st1'
965            |      \
966            S      S,L
967            |        \
968           st2 →taaf→ st2'
970           the taaf can be empty (e.g. tunneling) but we ask it must not be the
971           case when both st1 and st1' are labelled (we would be able to collapse
972           labels otherwise)
973         *)
974        ∃st2'.
975        ∃taa2 : trace_any_any_free … st2 st2'.
976        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
977        sim_status_rel st1' st2' ∧
978        label_rel … st1' st2'
979      | cl_jump ⇒
980        (* just like cl_other, but with a hypothesis more *)
981        as_costed … st1' →
982        ∃st2'.
983        ∃taa2 : trace_any_any_free … st2 st2'.
984        (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧
985        sim_status_rel st1' st2' ∧
986        label_rel … st1' st2'
987      ]
988    ].
993status_simulation_produce_tlr S1 S2 R
994(* we start from this situation
995     st1 →→→→tlr→→→→ st1'
996      | \
997      L  \---S--\
998      |          \
999   st2_lab →taa→ st2   (the taa preamble is in general either empty or given
1000                        by the preceding call)
1002   and we produce
1003     st1 →→→→tlr→→→→ st1'
1004             \\      /  \
1005             //     R    \-L,S-\
1006             \\     |           \
1007   st2_lab →tlr→ st2_mid →taaf→ st2'
1009  st1 st1' st2_lab st2
1010  (tlr1 : trace_label_return S1 st1 st1')
1011  (taa2_pre : trace_any_any S2 st2_lab st2)
1012  (sim_execute : status_simulation S1 S2 R)
1013  on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
1014  ∃st2_mid.∃st2'.
1015  ∃tlr2 : trace_label_return S2 st2_lab st2_mid.
1016  ∃taa2 : trace_any_any_free … st2_mid st2'.
1017  (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧
1018  R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧
1019  tlr_rel … tlr1 tlr2
1022\section{Conclusions and future works}
1024The labelling approach is a technique to implement compilers that induce on
1025the source code a non uniform cost model determined from the object code
1026produced. The cost model assigns a cost to each basic block of the program.
1027The main theorem of the labelling approach says that there is an exact
1028correspondence between the sequence of basic blocks started in the source
1029and object code, and that no instruction in the source or object code is
1030executed outside a basic block. Thus the overall cost of object code execution
1031can be computed precisely on the source code.
1033In this paper we scale the labelling approach to cover a programming language
1034with function calls. This introduces new difficulties only when the language
1035is unstructured, i.e. it allows function calls to return anywhere in the code,
1036destroying the hope of a static prediction of the cost of basic blocks.
1037We restore static predictability by introducing a new semantics for unstructured
1038programs that single outs well structured executions. The latter are represented
1039by structured traces, a generalization of streams of observables that capture
1040several structural invariants of the execution, like well nesting of functions
1041or the fact that every basic block must start with a code emission statement.
1042We show that structured traces are sufficiently structured to statically compute
1043a precise cost model on the object code.
1045We introduce a similarity relation on structured traces that must hold between
1046source and target traces. When the relation holds for every program, we prove
1047that the cost model can be lifted from the object to the source code.
1049In order to prove that similarity holds, we present a generic proof of forward
1050simulation that is aimed at pulling apart as much as possible the part of the
1051simulation related to non-functional properties (preservation of structure)
1052from that related to functional properties. In particular, we reduce the
1053problem of preservation of structure to that of showing a 1-to-0-or-many
1054forward simulation that only adds a few additional proof obligations to those
1055of a traditional, function properties only, proof.
1057All the results presented in the paper are part of a larger certification of a
1058C compiler which is based on the labelling approach. The certification, done
1059in Matita, is the main deliverable of the European Project CerCo.
1061The short term future work consists in the completion of the certification of
1062the CerCo compiler. In particular, the results presented in this paper will
1063be used to certify all the passes of the back-end of the compiler.
1065\paragraph{Related works}
1066CerCo is the first certification project which explicitly tries to induce a
1067precise cost model on the source code in order to establish non-functional
1068properties of programs on an high level language. Traditional certifications
1069of compilers, like~\cite{compcert2,piton}, only explicitly prove preservation
1070of the functional properties via forward simulations.
1072Usually forward simulations take the following form: for each transition
1073from $s_1$ to $s_2$ in the source code, there exists an equivalent sequence of
1074transitions in the target code of length $n$. The number $n$ of transition steps
1075in the target code can just be the witness of the existential statement.
1076An equivalent alternative when the proof of simulation is constructive consists
1077in providing an explicit function, called \emph{clock function} in the
1078litterature~\cite{clockfunctions}, that computes $n$ from $s_1$. Every clock
1079function constitutes then a cost model for the source code, in the spirit of
1080what we are doing in CerCo. However, we believe our solution to be superior
1081in the following points: 1) the machinery of the labelling approach is
1082insensible to the resource being measured. Indeed, any cost model computed on
1083the object code can be lifted to the source code (e.g. stack space used,
1084energy consumed, etc.). On the contrary, clock functions only talk about
1085number of transition steps. In order to extend the approach with clock functions
1086to other resources, additional functions must be introduced. Moreover, the
1087additional functions would be handled differently in the proof.
10882) the cost models induced by the labelling approach have a simple presentation.
1089In particular, they associate a number to each basic block. More complex
1090models can be induced when the approach is scaled to cover, for instance,
1091loop optimizations~\cite{loopoptimizations}, but the costs are still meant to
1092be easy to understandable and manipulate in an interactive theorem prover.
1093On the contrary, a clock function is a complex function of the state $s_1$
1094which, as a function, is an opaque object that is difficult to reify as
1095source code in order to reason on it.
Note: See TracBrowser for help on using the repository browser.