Changeset 1731

Feb 23, 2012, 5:25:43 PM (7 years ago)

A bit of front-end proof outline.

1 edited


  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1728 r1731  
    3939This document provides a very high-level, pen-and-paper sketch of what we view as the best path to completing the correctness proof for the compiler.
    4040In particular, for every translation between two intermediate languages, in both the front- and back-ends, we identify the key translation steps, and identify some invariants that we view as being important for the correctness proof.
     42\section{Front-end: Clight to RTLabs}
     44The front-end of the CerCo compiler consists of several stages:
     49\quad \= $\downarrow$ \quad \= \kill
     51\> $\downarrow$ \> cast removal\\
     52\> $\downarrow$ \> add runtime functions\footnote{Following the last project
     53meeting we intend to move this transformation to the back-end}\\
     54\> $\downarrow$ \> cost labelling\\
     55\> $\downarrow$ \> stack variable allocation and control structure
     56 simplification\\
     58\> $\downarrow$ \> generate global variable initialisation code\\
     59\> $\downarrow$ \> transform to RTL graph\\
     61\> $\downarrow$ \> start of target specific back-end\\
     62\>\quad \vdots
     67%Our overall statements of correctness with respect to costs will
     68%require a correctly labelled program
     70There are three layers in most of the proofs proposed:
     72\item invariants closely tied to the syntax and transformations using
     73  dependent types,
     74\item a forward simulation proof, and
     75\item syntactic proofs about the cost labelling.
     77The first will support both function correctness and allow us to show
     78the totality of some of the compiler stages (that is, these stages of
     79the compiler cannot fail).  The second provides the main functional
     80correctness result, and the last will be crucial for applying
     81correctness results about the costings from the back-end.
     83We will also prove that a suitably labelled RTLabs trace can be turned
     84into a \emph{structured trace} which splits the execution trace into
     85cost-label-to-cost-label chunks with nested function calls.  This
     86structure was identified during work on the correctness of the
     87back-end cost analysis as retaining important information about the
     88structure of the execution that is difficult to reconstruct later in
     89the compiler.
     91\subsection{Clight Cast removal}
     93This removes some casts inserted by the parser to make arithmetic
     94promotion explicit when they are superfluous (such as
     95\lstinline[language=C]'c = (short)((int)a + (int)b);').
     97The transformation only affects Clight expressions, recursively
     98detecting casts that can be safely eliminated.  The semantics provides
     99a big-step definition for expression, so we should be able to show a
     100lock-step forward simulation using a lemma showing that cast
     101elimination does not change the evaluation of expressions.  This lemma
     102will follow from a structural induction on the source expression.  We
     103have already proved a few of the underlying arithmetic results
     104necessary to validate the approach.
     106\subsection{Clight cost labelling}
     108This adds cost labels before and after selected statements and
     109expressions, and the execution traces ought to be equivalent modulo
     110cost labels.  Hence it requires a simple forward simulation with a
     111limited amount of stuttering whereever a new cost label is introduced.
     112A bound can be given for the amount of stuttering allowed can be given
     113based on the statement or continuation to be evaluated next.
     115We also intend to show three syntactic properties about the cost
     118\item every function starts with a cost label,
     119\item every branching instruction is followed by a label (note that
     120  exiting a loop is treated as a branch), and
     121\item the head of every loop (and any \lstinline'goto' destination) is
     122  a cost label.
     124These can be shown by structural induction on the source term.
     126\subsection{Clight to Cminor translation}
     128\subsection{Cminor global initialisation code}
     130\subsection{Cminor to RTLabs translation}
     132\subsection{RTLabs structured trace generation}
    42134\section{The RTLabs to RTL translation}
Note: See TracChangeset for help on using the changeset viewer.