Changeset 2606 for Papers/itp2013/ccexec.tex
 Timestamp:
 Feb 6, 2013, 12:13:00 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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