 Timestamp:
 Jun 17, 2013, 10:40:42 PM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/itp2013/ccexec2.tex
r3368 r3369 243 243 244 244 The plan of this paper is the following. In Section~\ref{sec:labelling} we 245 summari ze the labelling method. In Section~\ref{extension} we scale245 summarise the labelling method. In Section~\ref{extension} we scale 246 246 the method to unstructured languages with function calls. In 247 247 Section~\ref{sec:simulation} we give the necessary condition for the 248 248 correctness of the compiler (forward simulation proof). 249 Section~\ref{sec:formalization} sketches the formali zation of the249 Section~\ref{sec:formalization} sketches the formalisation of the 250 250 datastructures and proofs in Matita. 251 251 Conclusions and future works are in Section~\ref{sec:conclusions} … … 265 265 code emits the same sequence of labels ($L_1; L_2; L_2; L_3$ in the example). 266 266 This is achieved by keeping track of basic blocks during compilation, avoiding 267 all optimi zations that alter the control flow. The latter can be recovered with267 all optimisations that alter the control flow. The latter can be recovered with 268 268 a more refined version of the labelling approach~\cite{loopoptimizations}, but in the 269 269 present paper we stick to this simple variant for simplicity. Once the object 270 code is produced, the compiler runs a static code analy zer to associate to270 code is produced, the compiler runs a static code analyser to associate to 271 271 each label $L_1, \ldots, L_3$ the cost (in clock cycles) of the instructions 272 272 that belong to the corresponding basic block. For example, the cost $k_1$ … … 357 357 still grants that the sequence of labels observed on the two programs are 358 358 the same. A new difficulty appears when the compiler needs to statically 359 analy ze the object code to assign a cost to every label. What should the scope359 analyse the object code to assign a cost to every label. What should the scope 360 360 of the $L_1$ label be? After executing the $I_4$ block, the \verb+CALL+ 361 361 statement passes control to a function that cannot be determined statically. … … 411 411 \end{figure} 412 412 413 The latter definition of scope is ade guate on the source level because413 The latter definition of scope is adequate on the source level because 414 414 C is a structured language that guarantees that every function call, if it 415 415 returns, passes control to the first instruction that follows the call. However, … … 439 439 because of structure. Moreover, in order to avoid proving 440 440 too many preservation properties of our compiler, we drop the original 441 requirements on the object code (all instruct ons must be in scope of some labels,441 requirements on the object code (all instructions must be in scope of some labels, 442 442 no loops inside a scope, etc.) in favour of the corresponding requirement 443 443 for structured runs (a structured run must start with a label emission, no … … 459 459 properties. 460 460 461 All the definitions and theorems presented in the paper have been formali zed461 All the definitions and theorems presented in the paper have been formalised 462 462 in the interactive theorem prover Matita and are being used to certify 463 463 the complexity preserving compiler developed in the CerCo project~\cite{cerco}. 464 The formali zation heavily relies on algebraic and dependent types. In the464 The formalisation heavily relies on algebraic and dependent types. In the 465 465 first part of the paper 466 we did not try to stay close to the formali zation. On the contrary,466 we did not try to stay close to the formalisation. On the contrary, 467 467 the definitions given in the paper are the result of a significant 468 468 simplification effort for 469 469 the sake of presentation and to make easier the reimplementation of the 470 470 concepts in a proof assistant which is not based on the Calculus of Inductive 471 Constructions. In any case the formali zation, briefly presented at the end of471 Constructions. In any case the formalisation, briefly presented at the end of 472 472 the paper, is heavily commented to allow the 473 reader to understand the technical details of the formali zation.473 reader to understand the technical details of the formalisation. 474 474 475 475 … … 878 878 a local simulation condition: given two states in relation, if the source 879 879 one performs one step then the target one performs zero or more steps and 880 the two resulting states are synchroni zed again according to the relation.880 the two resulting states are synchronised again according to the relation. 881 881 No requirements are imposed on the intermediate target states. 882 882 Finally, the lemma is iterated over the execution fragment to establish the … … 1812 1812 % st2 →taaf→ st2' 1813 1813 % 1814 % the taaf can be empty (e.g. tunnel ing) but we ask it must not be the1814 % the taaf can be empty (e.g. tunnelling) but we ask it must not be the 1815 1815 % case when both st1 and st1' are labelled (we would be able to collapse 1816 1816 % labels otherwise) … … 2765 2765 % \section{Notes for the reviewers} 2766 2766 % 2767 % The results described in the paper are part of a larger formali zation2767 % The results described in the paper are part of a larger formalisation 2768 2768 % (the certification of the CerCo compiler). At the moment of the submission 2769 % we need to single out from the CerCo formali zation the results presented here.2769 % we need to single out from the CerCo formalisation the results presented here. 2770 2770 % Before the 16th of February we will submit an attachment that contains the 2771 % minimal subset of the CerCo formali zation that allows to prove those results.2771 % minimal subset of the CerCo formalisation that allows to prove those results. 2772 2772 % At that time it will also be possible to measure exactly the size of the 2773 % formali zation described here. At the moment a rough approximation suggests2773 % formalisation described here. At the moment a rough approximation suggests 2774 2774 % about 2700 lines of Matita code. 2775 2775 % 2776 2776 % We will also attach the development version of the interactive theorem 2777 % prover Matita that compiles the submitted formali zation. Another possibility2777 % prover Matita that compiles the submitted formalisation. Another possibility 2778 2778 % is to backport the development to the last released version of the system 2779 2779 % to avoid having to recompile Matita from scratch. 2780 2780 % 2781 % The programming and certification style used in the formali zation heavily2781 % The programming and certification style used in the formalisation heavily 2782 2782 % exploit dependent types. Dependent types are used: 1) to impose invariants 2783 2783 % by construction on the data types and operations (e.g. a traces from a state … … 2792 2792 % Finally, Matita and Coq are based on minor variations of the Calculus of 2793 2793 % (Co)Inductive Constructions. These variations do not affect the CerCo 2794 % formali zation. Therefore a porting of the proofs and ideas to Coq would be2794 % formalisation. Therefore a porting of the proofs and ideas to Coq would be 2795 2795 % rather straightforward. 2796 2796
Note: See TracChangeset
for help on using the changeset viewer.