Changeset 3231


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

Final revisions to 3.4.

Location:
Deliverables/D3.4/Report
Files:
2 edited

Legend:

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

    r3212 r3231  
    9393  pages = {263-288}
    9494}
     95
     96@article{2008-Leroy-Blazy-memory-model,
     97  author = {Xavier Leroy and Sandrine Blazy},
     98  title = {Formal verification of a {C}-like memory model
     99                 and its uses for verifying program transformations},
     100  journal = {Journal of Automated Reasoning},
     101  volume = 41,
     102  number = 1,
     103  pages = {1--31},
     104  url = {http://gallium.inria.fr/~xleroy/publi/memory-model-journal.pdf},
     105  urlpublisher = {http://dx.doi.org/10.1007/s10817-008-9099-0},
     106  hal = {http://hal.inria.fr/inria-00289542/},
     107  year = 2008,
     108  pubkind = {journal-int-multi}
     109}
  • Deliverables/D3.4/Report/report.tex

    r3228 r3231  
    132132of the compiler can be layered on top of normal forward simulation results,
    133133if we split those results into local call-structure preserving simulations.
    134 This split allowed us to concentrate on the intensional proofs by
    135 axiomatising some of the simulation results that are very similar to
    136 existing compiler correctness results.
     134This split allowed us to concentrate on the \textbf{intensional} proofs by
     135axiomatising some of the extensional simulation results that are very similar to
     136existing compiler correctness results, such as CompCert.
    137137
    138138This report is about the correctness results that are deliverable
     
    168168into the verification of the whole compiler.
    169169
    170 A key part of this work was to layer the intensional correctness
     170A key part of this work was to layer the \emph{intensional} correctness
    171171results that show that the costs produced are correct on top of the
    172 proofs about the compiled code's extensional behaviour (that is, the
     172proofs about the compiled code's \emph{extensional} behaviour (that is, the
    173173functional correctness of the compiler).  Unfortunately, the ambitious
    174174goal of completely verifying the entire compiler was not feasible
    175175within the time available, but thanks to this separation of
    176 extensional and intensional proofs we are able to axiomatize some
     176extensional and intensional proofs we are able to axiomatise some extensional
    177177simulation results which are similar to those in other compiler verification
    178178projects and concentrate on the novel intensional proofs.  We were
     
    192192describe the statements we need to prove about the intermediate \textsf{RTLabs}
    193193programs for the back-end proofs.
    194 Section~\ref{sec:inputtolabelling} covers the passes which produce the
     194Section~\ref{sec:inputtolabelling} covers the compiler passes which produce the
    195195annotated source program and Section~\ref{sec:measurablelifting} the rest
    196 of the transformations in the front-end.  Then the compile time checks
     196of the transformations in the front-end.  Then the compile-time checks
    197197for good cost labelling are detailed in Section~\ref{sec:costchecks}
    198198and the proofs that the structured traces required by the back-end
    199199exist are discussed in Section~\ref{sec:structuredtrace}.
    200200
    201 \section{The compiler and main goals}
    202 
    203 The unformalised \ocaml{} \cerco{} compiler was originally described
     201\section{The compiler and its correctness statement}
     202
     203The uncertified prototype \ocaml{} \cerco{} compiler was originally described
    204204in Deliverables 2.1 and 2.2.  Its design was replicated in the formal
    205205\matita{} code, which was presented in Deliverables 3.2 and 4.2, for
     
    217217middle two lines of Figure~\ref{fig:compilerlangs}.  The upper line
    218218represents the front-end of the compiler, and the lower the back-end,
    219 finishing with 8051 binary code.  Not all of the front-end passes
    220 introduces a new language, and Figure~\ref{fig:summary} presents a
     219finishing with Intel 8051 binary code.  Not all of the front-end compiler passes
     220introduce a new language, and Figure~\ref{fig:summary} presents a
    221221list of every pass involved.
    222222
     
    226226\begin{tabbing}
    227227\quad \= $\downarrow$ \quad \= \kill
    228 \textsf{C} (unformalized)\\
    229 \> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
     228\textsf{C} (unformalised)\\
     229\> $\downarrow$ \> CIL parser (unformalised \ocaml)\\
    230230\textsf{Clight}\\
    231231%\> $\downarrow$ \> add runtime functions\\
     
    250250
    251251\label{page:switchintro}
    252 The annotated source code is taken after the cost labelling phase.
     252The annotated source code is produced by the cost labelling phase.
    253253Note that there is a pass to replace C \lstinline[language=C]'switch'
    254254statements before labelling --- we need to remove them because the
     
    291291annotated source code, it also inserts the actual costs alongside the
    292292cost labels, and optionally adds a global cost variable and
    293 instrumentation to support further reasoning.
     293instrumentation to support further reasoning in external tools such as
     294Frama-C.
    294295
    295296\subsection{Revisions to the prototype compiler}
     
    310311
    311312The use of dependent types to capture simple intermediate language
    312 invariants makes every front-end pass except \textsf{Clight} to
    313 \textsf{Cminor} and the cost checks total functions.  Hence various
    314 well-formedness and type safety checks are performed once between
     313invariants makes every front-end pass a total function, except
     314\textsf{Clight} to \textsf{Cminor} and the cost checks.  Hence various
     315well-formedness and type safety checks are performed only once between
    315316\textsf{Clight} and \textsf{Cminor}, and the invariants rule out any
    316 difficulties in the later stages.
    317 With the benefit of hindsight we would have included an initial
    318 checking phase to produce a `well-formed' variant of \textsf{Clight},
    319 conjecturing that this would simplify various parts of the proofs for
    320 the \textsf{Clight} stages which deal with potentially ill-formed
    321 code.
    322 
    323 Following D2.2, we previous generated code for global variable
     317difficulties in the later stages.  With the benefit of hindsight we
     318would have included an initial checking phase to produce a
     319`well-formed' variant of \textsf{Clight}, conjecturing that this would
     320simplify various parts of the proofs for the \textsf{Clight} stages
     321which deal with potentially ill-formed code.
     322
     323Following D2.2, we previously generated code for global variable
    324324initialisation in \textsf{Cminor}, for which we reserved a cost label
    325325to represent the execution time for initialisation.  However, the
     
    328328initialisation code to the back-end and merge the costs.
    329329
    330 \subsection{Main goals}
     330\subsection{Main correctness statement}
    331331
    332332Informally, our main intensional result links the time difference in a source
     
    433433theorem in the file \lstinline'correctness.ma'.
    434434
    435 \section{Goals for the front-end}
     435\section{Correctness statement for the front-end}
    436436\label{sec:fegoals}
    437437
     
    588588\end{itemize}
    589589In order to tackle the first point, we implemented a version of memory
    590 extensions similar to CompCert's.
     590extensions similar to those of CompCert.
    591591
    592592For the simulation we decided to prove a sufficient amount to give us
     
    609609The invariant we would need is the fact that a global label lookup on a freshly
    610610created goto is equivalent to a local lookup. This would in turn require the
    611 propagation of some freshness hypotheses on labels. For reasons expressed above,
     611propagation of some freshness hypotheses on labels. As discussed,
    612612we decided to omit this part of the correctness proof.
    613613
     
    622622during the execution of a \lstinline[language=C]'while' loop.
    623623
    624 We do not attempt to capture any cost properties of the labelling in
    625 the simulation proof\footnote{We describe how the cost properties are
    626 established in Section~\ref{sec:costchecks}.}, allowing the proof to be oblivious to the choice
     624We do not attempt to capture any cost properties of the labelling\footnote{We describe how the cost properties are
     625established in Section~\ref{sec:costchecks}.} in
     626the simulation proof, which allows the proof to be oblivious to the choice
    627627of cost labels.  Hence we do not have to reason about the threading of
    628628name generation through the labelling function, greatly reducing the
     
    726726introduce extra steps, for example to store parameters in memory in
    727727\textsf{Cminor}.  Thus we have a version of the call simulation
    728 that deals with both in one result.
    729 
    730 In addition to the subtrace we are interested in measuring we must
    731 also prove that the earlier part of the trace is also preserved in
    732 order to use the simulation from the initial state.  It also
     728that deals with both the call and the cost label in one result.
     729
     730In addition to the subtrace we are interested in measuring, we must
     731prove that the earlier part of the trace is also preserved in
     732order to use the simulation from the initial state.  This proof also
    733733guarantees that we do not run out of stack space before the subtrace
    734734we are interested in.  The lemmas for this prefix and the measurable
     
    739739\begin{lstlisting}[language=matita]
    740740  let rec will_return_aux C (depth:nat)
    741                                (trace:list (cs_state $...$ C × trace)) on trace : bool :=
     741                               (trace:list (cs_state $...$ C $\times$ trace)) on trace : bool :=
    742742  match trace with
    743743  [ nil $\Rightarrow$ false
     
    766766Combining the lemmas about the prefix and the measurable subtrace
    767767requires a little care because the states joining the two might not be
    768 in the simulation relation.  In particular, if the measurable subtrace
     768related in the simulation.  In particular, if the measurable subtrace
    769769starts from the cost label at the beginning of the function there may
    770770be some extra instructions in the target code to execute to complete
    771771function entry before the states are back in the relation.  Hence we
    772 carefully phrased the lemmas to allow for these extra steps.
     772carefully phrased the lemmas to allow for such extra steps.
    773773
    774774Together, these then gives us an overall result for any simulation fitting the
     
    830830The \textsf{simplify\_inv} invariant encodes either the conservation
    831831of the semantics during the transformation corresponding to the failure
    832 of the transformation (\textsf{Inv\_eq} constructor), or the successful
     832of the coercion (\textsf{Inv\_eq} constructor), or the successful
    833833downcast of the considered expression to the target type
    834834(\textsf{Inv\_coerce\_ok}).
     
    900900Our memory injections are modelled after the work of Blazy \& Leroy.
    901901However, the corresponding paper is based on the first version of the
    902 CompCert memory model, whereas we use a much more concrete model, allowing byte-level
     902CompCert memory model~\cite{2008-Leroy-Blazy-memory-model}, whereas we use a much more concrete model, allowing byte-level
    903903manipulations (as in the later version of CompCert's memory model). We proved
    904 roughly 80 \% of the required lemmas. Some difficulties encountered were notably
    905 due to some overly relaxed conditions on pointer validity (fixed during development).
     904roughly 80 \% of the required lemmas. Notably, some of the difficulties encountered were
     905due to overly relaxed conditions on pointer validity (fixed during development).
    906906Some more side conditions had to be added to take care of possible overflows when converting
    907 from \textbf{Z} block bounds to $16$ bit pointer offsets (in practice, these overflows
     907from \textbf{Z} block bounds to $16$ bit pointer offsets (in practice, such overflows
    908908only occur in edge cases that are easily ruled out -- but this fact is not visible
    909909in memory injections). Concretely, some of the lemmas on the preservation of simulation of
     
    917917translate loops because our approach differs from CompCert by
    918918converting directly to \textsf{Cminor} \lstinline[language=C]'goto's
    919 rather than maintaining a notion of loops.  We also have a partial
     919rather than maintaining a notion of loop in \textsf{Cminor}.  We also have a partial
    920920proof for function entry, covering the setup of the memory injection,
    921921but not function exit.  Exits, and the remaining statements, have been
    922922axiomatised.
    923923
    924 Careful management of the proof state was required due to the proof
    925 terms that are embedded in \textsf{Cminor} code to show that some
    926 invariants are respected.  These proof terms can be large and awkward,
    927 and while generalising them away is usually sufficient, it can be
    928 difficult when they appear under a binder.
     924Careful management of the proof state was required because proof terms
     925are embedded in \textsf{Cminor} code to show that invariants are
     926respected.  These proof terms appear in the proof state when inverting
     927the translation functions, and they can be large and awkward.  While
     928generalising them away is usually sufficient, it can be difficult when
     929they appear under a binder.
    929930
    930931%The correctness proof for this transformation was not completed. We proved the
     
    940941The translation from \textsf{Cminor} to \textsf{RTLabs} is a fairly
    941942routine control flow graph (CFG) construction.  As such, we chose to
    942 axiomatise its simulation results.  However, we did prove several
     943axiomatise the associated extensional simulation results.  However, we did prove several
    943944properties of the generated programs:
    944945\begin{itemize}
     
    950951
    951952These properties rely on similar properties about type safety and the
    952 presence of \lstinline[language=C]'goto'-labels for Cminor programs
     953presence of \lstinline[language=C]'goto'-labels for \textsf{Cminor} programs
    953954which are checked at the preceding stage.  As a result, this
    954955transformation is total and any compilation failures must occur when
     
    959960graph inclusion.  We automated these proofs using a small amount of
    960961reflection, making the obligations much easier to handle.  One
    961 drawback to enforcing invariants thoroughly is that temporarily
     962drawback to enforcing invariants throughout is that temporarily
    962963breaking them can be awkward.  For example, \lstinline'return'
    963964statements were originally used as placeholders for
     
    994995
    995996\subsection{Implementation and correctness}
     997\label{sec:costchecksimpl}
    996998
    997999For a cost labelling to be sound and precise we need a cost label at
     
    10051007The implementation progresses through the set of nodes in the graph,
    10061008following successors until a cost label is found or a label-free cycle
    1007 is discovered (in which case the property does not hold and we stop).
    1008 This is made easier by the prior knowledge that any branch is followed
    1009 by cost labels, so we do not need to search each branch.  When a label
    1010 is found, we remove the chain from the set and continue from another
    1011 node in the set until it is empty, at which point we know that there
    1012 is a bound for every node in the graph.
    1013 
    1014 Directly reasoning about the function that implements this would be
     1009is discovered (in which case the property does not hold and we return
     1010an error).  This is made easier by the prior knowledge that every
     1011successor of a branch instruction is a cost label, so we do not need
     1012to search each branch.  When a label is found, we remove the chain of
     1013program counters from the set and continue from another node in the
     1014set until it is empty, at which point we know that there is a bound
     1015for every node in the graph.
     1016
     1017Directly reasoning about the function that implements this procedure would be
    10151018rather awkward, so an inductive specification of a single step of its
    10161019behaviour was written and proved to match the implementation.  This
     
    10311034\label{sec:structuredtrace}
    10321035
    1033 The \emph{structured traces} introduced in Section~\ref{sec:fegoals} enrich the execution trace of a program by
    1034 nesting function calls in a mixed-step style and embedding the cost labelling
    1035 properties of the program.  It was originally designed to support the
    1036 proof of correctness for the timing analysis of the object code in the
    1037 back-end, then generalised to provide a common structure to use from
    1038 the end of the front-end to the object code.  See
    1039 Figure~\ref{fig:strtrace} on page~\pageref{fig:strtrace} for an
    1040 illustration of a structured trace.
     1036The \emph{structured trace} idea introduced in
     1037Section~\ref{sec:fegoals} enriches the execution trace of a program by
     1038nesting function calls in a mixed-step style and embedding the cost
     1039labelling properties of the program.  See Figure~\ref{fig:strtrace} on
     1040page~\pageref{fig:strtrace} for an illustration of a structured trace.
     1041It was originally designed to support the proof of correctness for the
     1042timing analysis of the object code in the back-end, then generalised
     1043to provide a common structure to use from the end of the front-end to
     1044the object code.
    10411045
    10421046To make the definition generic we abstract over the semantics of the
     
    10561060  }.
    10571061\end{lstlisting}
    1058 which gives a type of states, an execution relation\footnote{All of
     1062which requires a type of states, an execution relation\footnote{All of
    10591063  our semantics are executable, but using a relation was simpler in
    1060   the abstraction.}, some notion of
    1061 program counters with decidable equality, the classification of states,
     1064  the abstraction.}, some notion of abstract
     1065program counter with decidable equality, the classification of states,
    10621066and functions to extract the observable intensional information (cost
    10631067labels and the identity of functions that are called).  The
     
    10931097The construction of the structured trace replaces syntactic cost
    10941098labelling properties, which place requirements on where labels appear
    1095 in the program, with semantics properties that constrain the execution
     1099in the program, with semantic properties that constrain the execution
    10961100traces of the program.  The construction begins by defining versions
    10971101of the sound and precise labelling properties on states and global
     
    11001104\textsf{RTLabs} semantics.
    11011105
    1102 Then we show that each cost labelling property the structured traces
    1103 definition requires is locally satisfied.  These are broken up by the
    1104 classification of states.  Similarly, we prove a step-by-step stack
    1105 preservation result, which states that the \textsf{RTLabs} semantics
    1106 never changes the lower parts of the stack.
     1106Then we show that each cost labelling property required by the
     1107definition of structured traces is locally satisfied.  These proofs are
     1108broken up by the classification of states.  Similarly, we prove a
     1109step-by-step stack preservation result, which states that the
     1110\textsf{RTLabs} semantics never changes the lower parts of the stack.
    11071111
    11081112The core part of the construction of a structured trace is to use the
     
    11211125with the property that there is a bound on the number of successor
    11221126instructions you can follow in the CFG before you encounter a cost
    1123 label.
     1127label (from Section~\ref{sec:costchecksimpl}).
    11241128
    11251129\subsubsection{Complete execution structured traces}
Note: See TracChangeset for help on using the changeset viewer.