Changeset 3369


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

submitted

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/itp-2013/ccexec2.tex

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