Changeset 3214

Timestamp:

Apr 29, 2013, 7:17:03 PM (6 years ago)

Author:

campbell

Message:

Some 3.4 revisions.

File:

• Deliverables/D3.4/Report/report.tex (modified) (10 diffs)

Deliverables/D3.4/Report/report.tex

@@ -114 +114 @@
 properties of the code produced by the front-end.
 
-A key part of our work is that the intensional correctness results that show
+A key part of our work is that the intensional correctness results which show
 that we get consistent cost measurements throughout the intermediate languages
 of the compiler can be layered on top of normal forward simulation results,
@@ -122 +122 @@
 compiler described in D3.2, using the source language semantics from
 D3.1 and intermediate language semantics from D3.3.  It builds on
-earlier work on a toy compiler built to test the labelling approach in
-D2.1. Together with the companion deliverable about the correctness of
-the back-end, D4.4, we obtain results about the whole formalised
-compiler.
+earlier work on the correctness of a toy compiler built to test the
+labelling approach in D2.1. Together with the companion deliverable
+about the correctness of the back-end, D4.4, we obtain results about
+the whole formalised compiler.
 
 % TODO: mention the deliverable about the extracted compiler et al?
@@ -140 +140 @@
 \section{Introduction}
 
-The \cerco{} compiler compiles C code, targeting microcontrollers
-implementing the Intel 8051 architecture.  It produces both the object
-code and source code containing annotations describing the timing
-behaviour of the object code.  There are two versions: first, an
-initial prototype implemented in \ocaml{}~\cite{d2.2}, and a version
-formalised in the \matita{} proof assistant~\cite{d3.2,d4.2} and then
-extracted to \ocaml{} code to produce an executable compiler.  In this
-document we present results formalised in \matita{} about the
-front-end of the latter version of the compiler, and how that fits
-into the verification of the whole compiler.
+The \cerco{} compiler produces a version of the source code containing
+annotations describing the timing behaviour of the object code, as well
+as the object code itself. It compiles C code, targeting
+microcontrollers implementing the Intel 8051 architecture.  There are
+two versions: first, an initial prototype was implemented in
+\ocaml{}~\cite{d2.2}, then a version was formalised in the \matita{} proof
+assistant~\cite{d3.2,d4.2} and extracted to \ocaml{} code to
+produce an executable compiler.  In this document we present results
+formalised in \matita{} about the front-end of the latter version of
+the compiler, and how that fits into the verification of the whole
+compiler.
 
 A key part of this work was to layer the intensional correctness
-results that show that the costs given are correct on top of the
+results that show that the costs produced are correct on top of the
 proofs about the compiled code's extensional behaviour (that is, the
 functional correctness of the compiler).  Unfortunately, the ambitious
 goal of completely verifying the entire compiler was not feasible
 within the time available, but thanks to this separation of
-extensional and intensional proofs we are able to axiomatize
-simulation results similar to those in other compiler verification
+extensional and intensional proofs we are able to axiomatize some
+simulation results which are similar to those in other compiler verification
 projects and concentrate on the novel intensional proofs.  We were
 also able to add stack space costs to obtain a stronger result.  The
@@ -174 +175 @@
 statement more precise.  Following that, in Section~\ref{sec:fegoals} we
 describe the statements we need to prove about the intermediate \textsf{RTLabs}
-programs sufficient for the back-end proofs.
+programs for the back-end proofs.
 Section~\ref{sec:inputtolabelling} covers the passes which produce the
 annotated source program and Section~\ref{sec:measurablelifting} the rest
@@ -191 +192 @@
 \begin{figure}
 \begin{center}
-\includegraphics{compiler-plain.pdf}
+\includegraphics[width=0.5\linewidth]{compiler-plain.pdf}
 \end{center}
 \caption{Languages in the \cerco{} compiler}
@@ -237 +238 @@
 statements before labelling --- we need to remove them because the
 simple form of labelling used in the formalised compiler is not quite
-capable of capturing their execution time costs, largely due to the
-fall-through behaviour.
+capable of capturing their execution time costs, largely due to C's 
+`fall-through' behaviour where execution from one branch continues in
+the next unless there is an explicit \lstinline[language=C]'break'.
 
 The cast removal phase which follows cost labelling simplifies
-expressions to prevent unnecessary arithmetic promotion which is
+expressions to prevent unnecessary arithmetic promotion, which is
 specified by the C standard but costly for an 8-bit target.  The
 transformation to \textsf{Cminor} and subsequently \textsf{RTLabs}
@@ -252 +254 @@
 The whole compilation function returns the following information on success:
 \begin{lstlisting}[language=matita]
-record compiler_output : Type[0] :=
- { c_labelled_object_code: labelled_object_code
- ; c_stack_cost: stack_cost_model
- ; c_max_stack: nat
- ; c_init_costlabel: costlabel
- ; c_labelled_clight: clight_program
- ; c_clight_cost_map: clight_cost_map
- }.
+  record compiler_output : Type[0] :=
+   { c_labelled_object_code: labelled_object_code
+   ; c_stack_cost: stack_cost_model
+   ; c_max_stack: nat
+   ; c_init_costlabel: costlabel
+   ; c_labelled_clight: clight_program
+   ; c_clight_cost_map: clight_cost_map
+   }.
 \end{lstlisting}
 It consists of annotated 8051 object code, a mapping from function
-identifiers to the function's stack space usage\footnote{The compiled
-  code's only stack usage is to allocate a fixed-size frame on each
-  function entry and discard it on exit.  No other dynamic allocation
-  is provided by the compiler.}, the space available for the
+identifiers to the function's stack space usage, the space available for the
 stack after global variable allocation, a cost label covering the
 execution time for the initialisation of global variables and the call
@@ -272 +271 @@
 costs.
 
-An \ocaml{} pretty printer is used to provide a concrete version of the output
-code.  In the case of the annotated source code, it also inserts the actual
-costs alongside the cost labels, and optionally adds a global cost variable
-and instrumentation to support further reasoning.
+An \ocaml{} pretty printer is used to provide a concrete version of
+the output code and annotated source code.  In the case of the
+annotated source code, it also inserts the actual costs alongside the
+cost labels, and optionally adds a global cost variable and
+instrumentation to support further reasoning.
 
 \subsection{Revisions to the prototype compiler}
@@ -285 +285 @@
 allocation provided by the compiler, so we were able to strengthen the
 statement of the goal to guarantee successful execution whenever the
-stack space obeys a bound calculated by subtracting the global
-variable requirements from the total memory available.
-
-The cost checks at the end of Figure~\ref{fig:summary} have been
+stack space obeys the \lstinline'c_max_stack' bound calculated by
+subtracting the global variable requirements from the total memory
+available.
+
+The cost labelling checks at the end of Figure~\ref{fig:summary} have been
 introduced to reduce the proof burden, and are described in
 Section~\ref{sec:costchecks}.
@@ -295 +296 @@
 invariants makes every front-end pass except \textsf{Clight} to
 \textsf{Cminor} and the cost checks total functions.  Hence various
-well-formedness and type checks are dealt with once in that phase.
+well-formedness and type safety checks are performed once between
+\textsf{Clight} and \textsf{Cminor}, and the invariants rule out any
+difficulties in the later stages.
 With the benefit of hindsight we would have included an initial
 checking phase to produce a `well-formed' variant of \textsf{Clight},