Changeset 3214


Ignore:
Timestamp:
Apr 29, 2013, 7:17:03 PM (4 years ago)
Author:
campbell
Message:

Some 3.4 revisions.

File:
1 edited

Legend:

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

    r3212 r3214  
    114114properties of the code produced by the front-end.
    115115
    116 A key part of our work is that the intensional correctness results that show
     116A key part of our work is that the intensional correctness results which show
    117117that we get consistent cost measurements throughout the intermediate languages
    118118of the compiler can be layered on top of normal forward simulation results,
     
    122122compiler described in D3.2, using the source language semantics from
    123123D3.1 and intermediate language semantics from D3.3.  It builds on
    124 earlier work on a toy compiler built to test the labelling approach in
    125 D2.1. Together with the companion deliverable about the correctness of
    126 the back-end, D4.4, we obtain results about the whole formalised
    127 compiler.
     124earlier work on the correctness of a toy compiler built to test the
     125labelling approach in D2.1. Together with the companion deliverable
     126about the correctness of the back-end, D4.4, we obtain results about
     127the whole formalised compiler.
    128128
    129129% TODO: mention the deliverable about the extracted compiler et al?
     
    140140\section{Introduction}
    141141
    142 The \cerco{} compiler compiles C code, targeting microcontrollers
    143 implementing the Intel 8051 architecture.  It produces both the object
    144 code and source code containing annotations describing the timing
    145 behaviour of the object code.  There are two versions: first, an
    146 initial prototype implemented in \ocaml{}~\cite{d2.2}, and a version
    147 formalised in the \matita{} proof assistant~\cite{d3.2,d4.2} and then
    148 extracted to \ocaml{} code to produce an executable compiler.  In this
    149 document we present results formalised in \matita{} about the
    150 front-end of the latter version of the compiler, and how that fits
    151 into the verification of the whole compiler.
     142The \cerco{} compiler produces a version of the source code containing
     143annotations describing the timing behaviour of the object code, as well
     144as the object code itself. It compiles C code, targeting
     145microcontrollers implementing the Intel 8051 architecture.  There are
     146two versions: first, an initial prototype was implemented in
     147\ocaml{}~\cite{d2.2}, then a version was formalised in the \matita{} proof
     148assistant~\cite{d3.2,d4.2} and extracted to \ocaml{} code to
     149produce an executable compiler.  In this document we present results
     150formalised in \matita{} about the front-end of the latter version of
     151the compiler, and how that fits into the verification of the whole
     152compiler.
    152153
    153154A key part of this work was to layer the intensional correctness
    154 results that show that the costs given are correct on top of the
     155results that show that the costs produced are correct on top of the
    155156proofs about the compiled code's extensional behaviour (that is, the
    156157functional correctness of the compiler).  Unfortunately, the ambitious
    157158goal of completely verifying the entire compiler was not feasible
    158159within the time available, but thanks to this separation of
    159 extensional and intensional proofs we are able to axiomatize
    160 simulation results similar to those in other compiler verification
     160extensional and intensional proofs we are able to axiomatize some
     161simulation results which are similar to those in other compiler verification
    161162projects and concentrate on the novel intensional proofs.  We were
    162163also able to add stack space costs to obtain a stronger result.  The
     
    174175statement more precise.  Following that, in Section~\ref{sec:fegoals} we
    175176describe the statements we need to prove about the intermediate \textsf{RTLabs}
    176 programs sufficient for the back-end proofs.
     177programs for the back-end proofs.
    177178Section~\ref{sec:inputtolabelling} covers the passes which produce the
    178179annotated source program and Section~\ref{sec:measurablelifting} the rest
     
    191192\begin{figure}
    192193\begin{center}
    193 \includegraphics{compiler-plain.pdf}
     194\includegraphics[width=0.5\linewidth]{compiler-plain.pdf}
    194195\end{center}
    195196\caption{Languages in the \cerco{} compiler}
     
    237238statements before labelling --- we need to remove them because the
    238239simple form of labelling used in the formalised compiler is not quite
    239 capable of capturing their execution time costs, largely due to the
    240 fall-through behaviour.
     240capable of capturing their execution time costs, largely due to C's
     241`fall-through' behaviour where execution from one branch continues in
     242the next unless there is an explicit \lstinline[language=C]'break'.
    241243
    242244The cast removal phase which follows cost labelling simplifies
    243 expressions to prevent unnecessary arithmetic promotion which is
     245expressions to prevent unnecessary arithmetic promotion, which is
    244246specified by the C standard but costly for an 8-bit target.  The
    245247transformation to \textsf{Cminor} and subsequently \textsf{RTLabs}
     
    252254The whole compilation function returns the following information on success:
    253255\begin{lstlisting}[language=matita]
    254 record compiler_output : Type[0] :=
    255  { c_labelled_object_code: labelled_object_code
    256  ; c_stack_cost: stack_cost_model
    257  ; c_max_stack: nat
    258  ; c_init_costlabel: costlabel
    259  ; c_labelled_clight: clight_program
    260  ; c_clight_cost_map: clight_cost_map
    261  }.
     256  record compiler_output : Type[0] :=
     257   { c_labelled_object_code: labelled_object_code
     258   ; c_stack_cost: stack_cost_model
     259   ; c_max_stack: nat
     260   ; c_init_costlabel: costlabel
     261   ; c_labelled_clight: clight_program
     262   ; c_clight_cost_map: clight_cost_map
     263   }.
    262264\end{lstlisting}
    263265It consists of annotated 8051 object code, a mapping from function
    264 identifiers to the function's stack space usage\footnote{The compiled
    265   code's only stack usage is to allocate a fixed-size frame on each
    266   function entry and discard it on exit.  No other dynamic allocation
    267   is provided by the compiler.}, the space available for the
     266identifiers to the function's stack space usage, the space available for the
    268267stack after global variable allocation, a cost label covering the
    269268execution time for the initialisation of global variables and the call
     
    272271costs.
    273272
    274 An \ocaml{} pretty printer is used to provide a concrete version of the output
    275 code.  In the case of the annotated source code, it also inserts the actual
    276 costs alongside the cost labels, and optionally adds a global cost variable
    277 and instrumentation to support further reasoning.
     273An \ocaml{} pretty printer is used to provide a concrete version of
     274the output code and annotated source code.  In the case of the
     275annotated source code, it also inserts the actual costs alongside the
     276cost labels, and optionally adds a global cost variable and
     277instrumentation to support further reasoning.
    278278
    279279\subsection{Revisions to the prototype compiler}
     
    285285allocation provided by the compiler, so we were able to strengthen the
    286286statement of the goal to guarantee successful execution whenever the
    287 stack space obeys a bound calculated by subtracting the global
    288 variable requirements from the total memory available.
    289 
    290 The cost checks at the end of Figure~\ref{fig:summary} have been
     287stack space obeys the \lstinline'c_max_stack' bound calculated by
     288subtracting the global variable requirements from the total memory
     289available.
     290
     291The cost labelling checks at the end of Figure~\ref{fig:summary} have been
    291292introduced to reduce the proof burden, and are described in
    292293Section~\ref{sec:costchecks}.
     
    295296invariants makes every front-end pass except \textsf{Clight} to
    296297\textsf{Cminor} and the cost checks total functions.  Hence various
    297 well-formedness and type checks are dealt with once in that phase.
     298well-formedness and type safety checks are performed once between
     299\textsf{Clight} and \textsf{Cminor}, and the invariants rule out any
     300difficulties in the later stages.
    298301With the benefit of hindsight we would have included an initial
    299302checking phase to produce a `well-formed' variant of \textsf{Clight},
Note: See TracChangeset for help on using the changeset viewer.