# Changeset 3369 for Papers/itp-2013

Ignore:
Timestamp:
Jun 17, 2013, 10:40:42 PM (7 years ago)
Message:

submitted

File:
1 edited

### Legend:

Unmodified
 r3368 The plan of this paper is the following. In Section~\ref{sec:labelling} we summarize the labelling method. In Section~\ref{extension} we scale summarise the labelling method. In Section~\ref{extension} we scale the method to unstructured languages with function calls. In Section~\ref{sec:simulation} we give the necessary condition for the correctness of the compiler (forward simulation proof). Section~\ref{sec:formalization} sketches the formalization of the Section~\ref{sec:formalization} sketches the formalisation of the datastructures and proofs in Matita. Conclusions and future works are in Section~\ref{sec:conclusions} code emits the same sequence of labels ($L_1; L_2; L_2; L_3$ in the example). This is achieved by keeping track of basic blocks during compilation, avoiding all optimizations that alter the control flow. The latter can be recovered with all optimisations that alter the control flow. The latter can be recovered with a more refined version of the labelling approach~\cite{loopoptimizations}, but in the present paper we stick to this simple variant for simplicity. Once the object code is produced, the compiler runs a static code analyzer to associate to code is produced, the compiler runs a static code analyser to associate to each label $L_1, \ldots, L_3$ the cost (in clock cycles) of the instructions that belong to the corresponding basic block. For example, the cost $k_1$ still grants that the sequence of labels observed on the two programs are the same. A new difficulty appears when the compiler needs to statically analyze the object code to assign a cost to every label. What should the scope analyse the object code to assign a cost to every label. What should the scope of the $L_1$ label be? After executing the $I_4$ block, the \verb+CALL+ statement passes control to a function that cannot be determined statically. \end{figure} The latter definition of scope is adeguate on the source level because The latter definition of scope is adequate on the source level because C is a structured language that guarantees that every function call, if it returns, passes control to the first instruction that follows the call. However, because of structure. Moreover, in order to avoid proving too many preservation properties of our compiler, we drop the original requirements on the object code (all instructons must be in scope of some labels, requirements on the object code (all instructions must be in scope of some labels, no loops inside a scope, etc.) in favour of the corresponding requirement for structured runs (a structured run must start with a label emission, no properties. All the definitions and theorems presented in the paper have been formalized All the definitions and theorems presented in the paper have been formalised in the interactive theorem prover Matita and are being used to certify the complexity preserving compiler developed in the CerCo project~\cite{cerco}. The formalization heavily relies on algebraic and dependent types. In the The formalisation heavily relies on algebraic and dependent types. In the first part of the paper we did not try to stay close to the formalization. On the contrary, we did not try to stay close to the formalisation. On the contrary, the definitions given in the paper are the result of a significant simplification effort for the sake of presentation and to make easier the re-implementation of the concepts in a proof assistant which is not based on the Calculus of Inductive Constructions. In any case the formalization, briefly presented at the end of Constructions. In any case the formalisation, briefly presented at the end of the paper, is heavily commented to allow the reader to understand the technical details of the formalization. reader to understand the technical details of the formalisation. a local simulation condition: given two states in relation, if the source one performs one step then the target one performs zero or more steps and the two resulting states are synchronized again according to the relation. the two resulting states are synchronised again according to the relation. No requirements are imposed on the intermediate target states. Finally, the lemma is iterated over the execution fragment to establish the %            st2 →taaf→ st2' % %            the taaf can be empty (e.g. tunneling) but we ask it must not be the %            the taaf can be empty (e.g. tunnelling) but we ask it must not be the %            case when both st1 and st1' are labelled (we would be able to collapse %            labels otherwise) % \section{Notes for the reviewers} % % The results described in the paper are part of a larger formalization % The results described in the paper are part of a larger formalisation % (the certification of the CerCo compiler). At the moment of the submission % we need to single out from the CerCo formalization the results presented here. % we need to single out from the CerCo formalisation the results presented here. % Before the 16-th of February we will submit an attachment that contains the % minimal subset of the CerCo formalization that allows to prove those results. % minimal subset of the CerCo formalisation that allows to prove those results. % At that time it will also be possible to measure exactly the size of the % formalization described here. At the moment a rough approximation suggests % formalisation described here. At the moment a rough approximation suggests % about 2700 lines of Matita code. % % We will also attach the development version of the interactive theorem % prover Matita that compiles the submitted formalization. Another possibility % prover Matita that compiles the submitted formalisation. Another possibility % is to backport the development to the last released version of the system % to avoid having to re-compile Matita from scratch. % % The programming and certification style used in the formalization heavily % The programming and certification style used in the formalisation heavily % exploit dependent types. Dependent types are used: 1) to impose invariants % by construction on the data types and operations (e.g. a traces from a state % Finally, Matita and Coq are based on minor variations of the Calculus of % (Co)Inductive Constructions. These variations do not affect the CerCo % formalization. Therefore a porting of the proofs and ideas to Coq would be % formalisation. Therefore a porting of the proofs and ideas to Coq would be % rather straightforward.