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


1 edited


  • Papers/itp-2013/ccexec.tex

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