Changeset 3223


Ignore:
Timestamp:
Apr 30, 2013, 12:05:24 PM (4 years ago)
Author:
campbell
Message:

More revisions to 3.4.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.4/Report/report.tex

    r3218 r3223  
    305305code.
    306306
    307 \todo{move of initialisation code?}
     307Following D2.2, we previous generated code for global variable
     308initialisation in \textsf{Cminor}, for which we reserved a cost label
     309to represent the execution time for initialisation.  However, the
     310back-end must also add an initial call to the main function, whose
     311cost must also be accounted for, so we decided to move the
     312initialisation code to the back-end and merge the costs.
    308313
    309314\subsection{Main goals}
     
    409414observable witness is preserved, so the program must behave correctly.
    410415
    411 \section{Intermediate goals for the front-end}
     416\section{Goals for the front-end}
    412417\label{sec:fegoals}
    413418
     
    561566  instead of \textbf{break}).
    562567\end{itemize}
    563 
    564568In order to tackle the first point, we implemented a version of memory
    565 extensions similar to Compcert's. What has been done is the simulation proof
    566 for all ``easy'' cases, that do not interact with the switch removal per se,
    567 plus a bit of the switch case. This comprises propagating the memory extension
    568 through  each statement (except switch), as well as various invariants that
    569 are needed for the switch case (in particular, freshness hypotheses). The
    570 details of the evaluation process for the source switch statement and its
    571 target counterpart can be found in the file \textbf{switchRemoval.ma},
    572 along more details on the transformation itself.
     569extensions similar to CompCert's.
     570
     571For the simulation we decided to prove a sufficient amount to give us
     572confidence in the definitions and approach, but curtail the proof
     573because this pass does not contribute to the intensional correctness
     574result.  We tackled several simple cases, that do not interact with
     575the switch removal per se, to show that the definitions were usable,
     576and part of the switch case to check that the approach is
     577reasonable. This comprises propagating the memory extension through
     578each statement (except switch), as well as various invariants that are
     579needed for the switch case (in particular, freshness hypotheses). The
     580details of the evaluation process for the source switch statement and
     581its target counterpart can be found in the file
     582\textbf{switchRemoval.ma}, along more details on the transformation
     583itself.
    573584
    574585Proving the correctness of the second point would require reasoning on the
     
    820831both the implementation and the proof more complex, even though more
    821832comprehensive checks are made in the next stage.
    822 \todo{Make this a particular case of the more general statement on baking more invariants in the Clight language}
     833%\todo{Make this a particular case of the more general statement on baking more invariants in the Clight language}
    823834
    824835\subsubsection{Clight to Cminor}
     
    827838Its input is a full \textsf{Clight} program, and its output is a
    828839\textsf{Cminor} program. Note that we do not use an equivalent of
    829 Compcert's \textsf{C\#minor} language: we translate directly to a
     840CompCert's \textsf{C\#minor} language: we translate directly to a
    830841variant of \textsf{Cminor}. This presents the advantage of not
    831842requiring the special loop constructs, nor the explicit block
     
    855866Our memory injections are modelled after the work of Blazy \& Leroy.
    856867However, the corresponding paper is based on the first version of the
    857 Compcert memory model, whereas we use a much more concrete model, allowing byte-level
    858 manipulations (as in the later version of Compcert's memory model). We proved
     868CompCert memory model, whereas we use a much more concrete model, allowing byte-level
     869manipulations (as in the later version of CompCert's memory model). We proved
    859870roughly 80 \% of the required lemmas. Some difficulties encountered were notably
    860871due to some overly relaxed conditions on pointer validity (fixed during development).
     
    867878\paragraph{Simulation proof.}
    868879
    869 The correctness proof for this transformation was not completed. We proved the
    870 simulation result for expressions and for some subset of the critical statement cases.
    871 Notably lacking are the function entry and exit, where the memory injection is
    872 properly set up. As would be expected, a significant amount of work has to be performed
    873 to show the conservation of all invariants at each simulation step.
    874 
    875 \todo{list cases, explain while loop, explain labeling problem}
     880We proved the simulation result for expressions and a representative
     881selection of statements.  In particular we tackled
     882\lstinline[language=C]'while' statements to ensure that we correctly
     883translate loops because our approach differs from CompCert by
     884converting directly to \textsf{Cminor} \lstinline[language=C]'goto's
     885rather than maintaining a notion of loops.  We also have a partial
     886proof for function entry, covering the setup of the memory injection,
     887but not function exit.  Exits, and the remaining statements, have been
     888axiomatised.
     889
     890Careful management of the proof state was required due to the proof
     891terms that are embedded in \textsf{Cminor} code to show that some
     892invariants are respected.  These proof terms can be large and awkward,
     893and while generalising them away is usually sufficient, it can be
     894difficult when they appear under a binder.
     895
     896%The correctness proof for this transformation was not completed. We proved the
     897%simulation result for expressions and for some subset of the critical statement cases.
     898%Notably lacking are the function entry and exit, where the memory injection is
     899%properly set up. As would be expected, a significant amount of work has to be performed
     900%to show the conservation of all invariants at each simulation step.
     901
     902%\todo{list cases, explain while loop, explain labeling problem}
    876903
    877904\subsubsection{Cminor to RTLabs}
Note: See TracChangeset for help on using the changeset viewer.