Changeset 3181

Apr 26, 2013, 11:08:14 AM (4 years ago)

Compiler overview section of 3.4

1 added
1 edited


  • Deliverables/D3.4/Report/report.tex

    r3173 r3181  
    181181\section{The compiler and main goals}
    183 TODO: outline compiler, maybe figure from talk, maybe something like the figure
    184 below.
    186 TODO: might want a version of this figure
     183The unformalised \ocaml{} \cerco{} compiler was originally described
     184in Deliverables 2.1 and 2.2.  Its design was replicated in the formal
     185\matita{} code, which was presented in Deliverables 3.2 and 4.2, for
     186the front-end and back-end respectively.
     192\caption{Languages in the \cerco{} compiler}
     196The compiler uses a number of intermediate languages, as outlined the
     197middle two lines of Figure~\ref{fig:compilerlangs}.  The upper line
     198represents the front-end of the compiler, and the lower the back-end,
     199finishing with 8051 binary code.  Not all of the front-end passes
     200introduces a new language, and Figure~\ref{fig:summary} presents a
     201list of every pass involved.
    215 The compiler function returns the following record on success:
     232The annotated source code is taken after the cost labelling phase.
     233Note that there is a pass to replace C \lstinline[language=C]'switch'
     234statements before labelling --- we need to remove them because the
     235simple form of labelling used in the formalised compiler is not quite
     236capable of capturing their execution time costs, largely due to the
     237fall-through behaviour.
     239The cast removal phase which follows cost labelling simplifies
     240expressions to prevent unnecessary arithmetic promotion which is
     241specified by the C standard but costly for an 8-bit target.  The
     242transformation to \textsf{Cminor} and subsequently \textsf{RTLabs}
     243bear considerable resemblance to some passes of the CompCert
     244compiler\todo{cite}, although we use a simpler \textsf{Cminor} where
     245all loops use \lstinline[language=C]'goto' statements, and the
     246\textsf{RTLabs} language retains a target-independent flavour.  The
     247back-end takes \textsf{RTLabs} code as input.
     249The whole compilation function returns the following information on success:
    217251record compiler_output : Type[0] :=
    243277\subsection{Revisions to the prototype compiler}
    245 TODO: could be a good idea to have this again; stack space,
    246 initialisation, cost checks, had we dropped cminor loops in previous
    247 writing?, check mailing list in case I've forgotten something
    249 TODO: continued use of dep types to reduce partiality
     279Our focus on intensional properties prompted us to consider whether we
     280could incorporate stack space into the costs presented to the user.
     281We only allocate one fixed-size frame per function, so modelling this
     282was relatively simple.  It is the only form of dynamic memory
     283allocation provided by the compiler, so we were able to strengthen the
     284statement of the goal to guarantee successful execution whenever the
     285stack space obeys a bound calculated by subtracting the global
     286variable requirements from the total memory available.
     288The cost checks at the end of Figure~\ref{fig:summary} have been
     289introduced to reduce the proof burden, and are described in
     292The use of dependent types to capture simple intermediate language
     293invariants makes every front-end pass except \textsf{Clight} to
     294\textsf{Cminor} and the cost checks total functions.  Hence various
     295well-formedness and type checks are dealt with once in that phase.
     296With the benefit of hindsight we would have included an initial
     297checking phase to produce a `well-formed' variant of \textsf{Clight},
     298conjecturing that this would simplify various parts of the proofs for
     299the \textsf{Clight} stages which deal with potentially ill-formed
     302\todo{move of initialisation code?}
    251304\subsection{Main goals}
    444497\section{Input code to cost labelled program}
    446 The simple form of labelling used in the formalised compiler is not
    447 quite capable of capturing costs arising from complex C
    448 \lstinline[language=C]'switch' statements, largely due to the
    449 fall-through behaviour.  Our first pass replaces these statements with
     499As explained on page~\pageref{page:switchintro}, the costs of complex
     500C \lstinline[language=C]'switch' statements cannot be represented with
     501the simple labelling.  Our first pass replaces these statements with
    450502simpler C code, allowing our second pass to perform the cost
    451503labelling.  We show that the behaviour of programs is unchanged by
    746798\section{Checking cost labelling properties}
    748801Ideally, we would provide proofs that the cost labelling pass always
Note: See TracChangeset for help on using the changeset viewer.