Changeset 2606

Ignore:
Timestamp:
Feb 6, 2013, 12:13:00 PM (8 years ago)
Message:

conclusions

File:
1 edited

Unmodified
Added
Removed
• Papers/itp-2013/ccexec.tex

 r2605 \section{Conclusions and future works} \label{conclusions} The labelling approach is a technique to implement compilers that induce on the source code a non uniform cost model determined from the object code produced. The cost model assigns a cost to each basic block of the program. The main theorem of the labelling approach says that there is an exact correspondence between the sequence of basic blocks started in the source and object code, and that no instruction in the source or object code is executed outside a basic block. Thus the overall cost of object code execution can be computed precisely on the source code. In this paper we scale the labelling approach to cover a programming language with function calls. This introduces new difficulties only when the language is unstructured, i.e. it allows function calls to return anywhere in the code, destroying the hope of a static prediction of the cost of basic blocks. We restore static predictability by introducing a new semantics for unstructured programs that single outs well structured executions. The latter are represented by structured traces, a generalization of streams of observables that capture several structural invariants of the execution, like well nesting of functions or the fact that every basic block must start with a code emission statement. We show that structured traces are sufficiently structured to statically compute a precise cost model on the object code. We introduce a similarity relation on structured traces that must hold between source and target traces. When the relation holds for every program, we prove that the cost model can be lifted from the object to the source code. In order to prove that similarity holds, we present a generic proof of forward simulation that is aimed at pulling apart as much as possible the part of the simulation related to non-functional properties (preservation of structure) from that related to functional properties. In particular, we reduce the problem of preservation of structure to that of showing a 1-to-0-or-many forward simulation that only adds a few additional proof obligations to those of a traditional, function properties only, proof. All the results presented in the paper are part of a larger certification of a C compiler which is based on the labelling approach. The certification, done in Matita, is the main deliverable of the European Project CerCo. The short term future work consists in the completion of the certification of the CerCo compiler. In particular, the results presented in this paper will be used to certify all the passes of the back-end of the compiler. \paragraph{Related works} CerCo is the first certification project which explicitly tries to induce a precise cost model on the source code in order to establish non-functional properties of programs on an high level language. Traditional certifications of compilers, like~\cite{compcert,python}, only explicitly prove preservation of the functional properties via forward simulations. Usually forward simulations take the following form: for each transition from $s_1$ to $s_2$ in the source code, there exists an equivalent sequence of transitions in the target code of length $n$. The number $n$ of transition steps in the target code can just be the witness of the existential statement. An equivalent alternative when the proof of simulation is constructive consists in providing an explicit function, called \emph{clock function} in the litterature~\cite{clockfunctions}, that computes $n$ from $s_1$. Every clock function constitutes then a cost model for the source code, in the spirit of what we are doing in CerCo. However, we believe our solution to be superior in the following points: 1) the machinery of the labelling approach is insensible to the resource being measured. Indeed, any cost model computed on the object code can be lifted to the source code (e.g. stack space used, energy consumed, etc.). On the contrary, clock functions only talk about number of transition steps. In order to extend the approach with clock functions to other resources, additional functions must be introduced. Moreover, the additional functions would be handled differently in the proof. 2) the cost models induced by the labelling approach have a simple presentation. In particular, they associate a number to each basic block. More complex models can be induced when the approach is scaled to cover, for instance, loop optimizations~\cite{loopoptimizations}, but the costs are still meant to be easy to understandable and manipulate in an interactive theorem prover. On the contrary, a clock function is a complex function of the state $s_1$ which, as a function, is an opaque object that is difficult to reify as source code in order to reason on it. \bibliographystyle{splncs03}
Note: See TracChangeset for help on using the changeset viewer.