Changeset 2606 for Papers/itp-2013/ccexec.tex

Timestamp:

Feb 6, 2013, 12:13:00 PM (7 years ago)

Author:

sacerdot

Message:

conclusions

File:

• Papers/itp-2013/ccexec.tex (modified) (1 diff)

Papers/itp-2013/ccexec.tex

@@ -845 +845 @@
 \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}