source: Deliverables/Dissemination/final-review/wp3/front-end.tex @ 3290

\documentclass[nopanel]{beamer}
\usepackage{graphicx,color}
\usepackage{amsfonts}
\usepackage{listings}

\lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
        keywordstyle=\color{red}\bfseries,
        keywordstyle=[2]\color{blue},
        commentstyle=\color{green},
        stringstyle=\color{blue},
        showspaces=false,showstringspaces=false}


\setbeamertemplate{footline}[page number]
\setbeamertemplate{sidebar right}{}

\setbeamercolor{alerted text}{fg=red!70!orange}

\newcommand{\red}[1]{\textcolor{red}{#1}}
\newcommand{\blue}[1]{\textcolor{blue}{#1}}
\newcommand{\green}[1]{\textcolor{green}{#1}}
\newcommand{\grey}[1]{\textcolor{grey}{#1}}

\addtolength{\parskip}{0.3em}

\begin{document}

\title{WP3: Verified Compiler --- Front End\\[1\jot]
D3.4: Front-End Correctness Proofs}
\author{Brian~Campbell, Ilias~Garnier, James~McKinna, \underline{Ian~Stark}}
\institute{LFCS, University of Edinburgh\\[1ex]
\includegraphics[width=.3\linewidth]{cerco_logo.png}\\
\footnotesize Project FP7-ICT-2009-C-243881
}
\date{CerCo review meeting\\16th May 2013}
\maketitle


\begin{frame}{CerCo Outcomes}

  The final results of the CerCo project include the following:

  \medskip %
  \begin{itemize}
  \item A compiler from C to executable 8051 binaries, formalised in Matita as
    \blue{\lstinline|compiler.ma|} \dots
  \item \dots which adds labels and cost information to C source code
  \item \dots with exact values for time and space used by the binary.

    \medskip %
  \item A machine-checked proof of this in Matita
    \blue{\lstinline|correctness.ma|}:

    \smallskip %
    \begin{itemize}
    \item Addressing \red{intensional} properties --- clock cycles, stack bytes

      \smallskip %
    \item As well as \red{extensional} properties --- functional correctness.
    \end{itemize}
  \item An executable cost-annotating compiler \blue{\lstinline|cerco|}
    extracted from the formalisation.
  \end{itemize}

  \medskip %
  This talk treats the front-end compiler and proof, describing the technical
  challenges and contributions from the work in Period~3.
  
\end{frame}

\begin{frame}{Compiler}

  The CerCo compiler, given C source code, will generate:
  \begin{itemize}
  \item Labelled Clight source code;
  \item Labelled 8051 object code;
  \item Cost maps: for each label a count of time (clock cycles) and space
    (stack bytes) usage.
  \end{itemize}

  \medskip %
  The compiler operates in multiple passes, with each intermediate language
  having an executable semantics in Matita: %
  \vspace*{-\medskipamount}
  \begin{center}
    \includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
  \end{center}
  \vspace*{-\medskipamount}

\end{frame}

\begin{frame}{Correctness}
  
  Suppose we have C source with labelled Clight, labelled 8051 binary, and
  cost maps all generated from the CerCo compiler.

  \medskip %
  Then the Matita theorem for correctness is that:
  \begin{itemize}
  \item Executing the original and labelled Clight source gives the same
    behaviour;
  \item Executing the 8051 binary gives the same observables: labels and
    call/return;
  \item Applying the cost maps to the trace of C labels correctly
    describes the time and space usage of the 8051 execution.
  \end{itemize}

  In fact we give an exact result on all \red{measurable subtraces}: from any
  label to the end of its enclosing function.

  \medskip %
  The machine-checked proof is the concatenation of correctness results for
  the front end, the back end, and the assembler.

\end{frame}

\begin{frame}{Front-End Progress}
  
  \vspace*{-\bigskipamount}
  \begin{center}
    \includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
  \end{center}
  \vspace*{-\medskipamount}

  At the start of Period~3 the front end included in Matita:
  \begin{itemize}
  \item Executable semantics for source and intermediate languages;
  \item Labelling and compilation of source through these;
  \item Innovation of \red{structured traces}, originally to support timing
    calculation in the assembler.
  \end{itemize}

  At the completion of Period~3, the front end now includes proofs of
  correctness for all these stages, extension to stack usage, and considerable
  refinement of the existing formal development.
  
\end{frame}

\begin{frame}{Front-End Contribution}

  Notable features and original elements of the front-end include:
  \begin{itemize}
  \item Proof layering:
    \begin{itemize}
    \item A \blue{functional correctness proof};
    \item A \blue{cost proof}, separate but depending on functional
      correctness.
    \end{itemize}
  \item \blue{Internal checks} as a proof shortcut, like translation
    validation.
  \item \blue{Structured traces} for holding detailed data on resource
    behaviour, not just for assembler cost calculation.
  \item Introduction of \blue{measurable subtraces} as a unit of cost
    proof.
  \end{itemize}
  These features are significant in particular because:
  \begin{itemize}
  \item Compilation is not 1-1 transliteration: code is rearranged and
    modified, but label sequencing is preserved;
  \item The source language has implicit control flow constraints not present
    in the target (call/return, branches, loops).
  \end{itemize}

\end{frame}

\begin{frame}{Axiomatization}

  The translation in \blue{\lstinline|compile.ma|} is complete --- essential
  for extracting a compiler.

  \medskip %
  The simulation results in \blue{\lstinline|correctness.ma|} are fully
  specified, and with substantially complete proofs.  Some parts, however,
  have been axiomatized and their correctness assumed.

  \medskip %
  In the front-end there are two sources of this axiomatisation:
  \begin{itemize}
  \item \red{Functional correctness.}  Other projects, notably
    \blue{CompCert}, provide assurances that such proofs can be completed; so
    certain parts of this proof have been assumed.
  \item Simulation steps with \red{many cases}, some very similar; here we
    have identified representative and more challenging cases for detailed
    proof.
  \end{itemize}
 
\end{frame}

\begin{frame}{Structure of the Proof}

  \begin{center}
    \includegraphics[width=0.7\linewidth]{compiler.pdf}
  \end{center}

  The transition from front-end to back-end marks the change:
  \begin{itemize}
  \item From a language with explicit call/return structure and high-level
    structured control flow;
  \item To a language with unconstrained jumps for control flow.
  \end{itemize}

  Correspondingly, the proof hands over
  \begin{itemize}
  \item From measurable subtraces with labelling that must be checked
    \blue{sound} and \blue{precise};
  \item To \blue{structured traces} which embed these invariants.
  \end{itemize}

\end{frame}

\begin{frame}{Structured Traces}

  Embed call structure and label invariants into execution traces.

  \begin{center}
    \includegraphics{strtraces.pdf}
  \end{center}
  \vspace*{-\bigskipamount}
  \begin{itemize}
  \item Enforces \blue{invariants} on positions of cost labels.
  \item \blue{Groups} execution steps according to preceding cost label.
  \item Forbids \blue{repeating} addresses in grouped steps.
  \end{itemize}

  Constructed by folding up \red{measurable subtraces}, using their termination
  and the fact that labelling is \blue{sound} and \blue{precise}.

\end{frame}

\begin{frame}{Step-by-Step: Getting to Labelled Source}

  \blue{C $\to$ Clight}

  \smallskip %
  To translate from C to Clight we reuse the CompCert parser.

  \bigskip %
  \blue{Switch Removal}

  \smallskip %
  Control flow for \red{\lstinline'switch'} is too subtle for simple
  labelling; we replace with an \red{\lstinline'if .. then .. else'} tree.
  Proof requires tracking memory extension for an extra test variable.

  \bigskip %
  \blue{Cost Labels}

  \smallskip %
  Labels added at function start, branch targets, \dots

  \smallskip %
  Simulation of execution is exact, just skipping over labels.

\end{frame}

\begin{frame}{Front-End Correctness}

  Suppose we have a \blue{measurable} subtrace of Clight execution, including
  the \blue{prefix} of that trace from initial state.

  \medskip %
  Then for handover to the back-end we have in RTLabs:
  \begin{itemize}
  \item A corresponding \red{prefix};
  \item A \red{structured trace} corresponding to the measurable subtrace;
  \item The required invariants, including \red{no repeating addresses};
  \item A proof that the same \red{stack limit} is observed.
  \end{itemize}

  \medskip %
  In addition, to link this with the source program:
  \begin{itemize}
  \item The observables for the RTLabs \blue{prefix} and \blue{structured
      trace} are the same as for their counterparts in Clight.
  \end{itemize}

\end{frame}

\begin{frame}{Lifting Measurable Traces}

  For each pass find a target \red{measurable subtrace} equivalent to any
  source \red{measurable subtrace}.

  \begin{center}
    \includegraphics{meassim.pdf}
  \end{center}

  Split normal simulation proof:
  \begin{enumerate}
  \item each \blue{call} becomes a \blue{call} step plus zero or more
    \blue{normal} steps; following cost labels should stay next to the call
    step
  \item each \blue{return} becomes a \blue{return} plus zero or
    more \blue{normal} steps
  \item \blue{cost} label steps are preserved
  \item other \blue{normal} steps become zero or more \blue{normal} steps
  \end{enumerate}

  This preserves the defining property for \red{measurable subtraces}.

\end{frame}

\begin{frame}{Front-End Simulation Results}
  \blue{Cast simplification}
  \begin{itemize}
  \item Simplify expressions for 8-bit target.
  \item Only expressions change --- statements are in lock-step.
  \end{itemize}

  \blue{Clight to Cminor}
  \begin{itemize}
  \item Stack allocation and control flow transformation.
  \item Similar to \blue{CompCert}, but using \red{\lstinline'goto'} instead
    of \red{\lstinline'loop'}
  \item Large proof terms for invariants embedded in Cminor programs using
    dependent types.
  \end{itemize}

  \blue{Cminor to RTLabs}
  \begin{itemize}
  \item Construction of control-flow graph.
  \item Embedded invariants mean that translation function is \red{total}.
  \end{itemize}
\end{frame}

\begin{frame}{Checking Cost Labelling}

  Building structured traces in \blue{RTLabs} depends on having cost labelling
  on the linear trace that is \red{sound} and \red{precise}.

  \medskip %
  Instead of carrying this as an invariant all the way through each previous
  pass, we take a \blue{shortcut} and check on the spot.

  \medskip %
  This is similar to \blue{translation validation}.

  \medskip %
   The specific requirements for labelling \blue{RTLabs} code are:
   \begin{description}[\red{soundness}]
   \item[\red{soundness}] At every point, a finite bound on the number of
     instructions until the next label; 
   \item[\red{soundness}] A label at the start of every function;
   \item[\red{precision}] A label after every branch.
   \end{description}
  
   \medskip % 
   The bound is the hard part; the rest is a simple syntactic check.
\end{frame}

\begin{frame}[fragile]{Checking Bound to Next Label}

    \begin{center}
  \begin{overprint}[0.5\linewidth]
      \onslide<1>\includegraphics[width=0.8\linewidth]{loop.pdf}
      \onslide<2>\includegraphics[width=0.8\linewidth]{loop1.pdf}
      \onslide<3>\includegraphics[width=0.8\linewidth]{loop2.pdf}
      \onslide<4>\includegraphics[width=0.8\linewidth]{loop3.pdf}
      \onslide<5>\includegraphics[width=0.8\linewidth]{loop4.pdf}
      \onslide<6->\includegraphics[width=0.8\linewidth]{loopx.pdf}
  \end{overprint}
    \end{center}
  \begin{itemize}
  \item Pick an arbitrary node in the CFG;
  \item<2-> Follow successor instructions;
  \item<4-> If we find a \alert{cost label} all the traced nodes have a
    bound\dots
  \item<5-> \dots so remove them and pick a new node, continue;
  \item<6-> But if we find an \alert{unlabelled loop} then the labelling is
    unsound, report an error.
  \end{itemize}

  \onslide<7->
  When complete, we have a proof that every loop contains a label.

\end{frame}

\begin{frame}{Checking Cost Labelling}

  This check of soundness and precision in RTLabs:
  \begin{itemize}
  \item Will always succeed when invariants hold (and fail when not);
  \item Extracts to additional checking code in the compiler;
  \item[\checkmark] Significantly reduces the proof effort.
  \end{itemize}

  \medskip %
  The last point is our key observation: a conventional proof would require
  showing that: 
  \begin{quote}
    \red{If} every loop in \blue{Cminor} code is headed by a cost label;
    \\[1\jot]
    \red{Then} at every point in every \blue{RTLabs} execution there is a
    finite bound on the number of instructions until the next cost label.
  \end{quote}
  We expect just proving existence of this bound to be considerably harder
  than implementing the whole checking mechanism.

\end{frame}

\begin{frame}{Putting the Proofs Together}

  \begin{center}
    \includegraphics[width=0.7\linewidth]{compiler.pdf}
  \end{center}

  The front-end proof demonstrates that for any Clight execution:
  \begin{itemize}
  \item We have a corresponding \blue{structured trace} with \blue{invariants}
    \dots
  \item \dots and with the same \blue{observables} of labels and call/return.
  \end{itemize}

  The back-end proof takes this structured trace and shows that
  \begin{itemize}
  \item There is a corresponding assembler trace \dots
  \item \dots with \blue{sound} and \blue{precise} labelling and the same
    \blue{observables}.
  \end{itemize}

  Combining these gives a proof that time and space costs computed on the
  source are exactly those observed on executing the binary.

\end{frame}

\begin{frame}{Summary}

  CerCo WP3 has produced the front-end of a C-to-8051 compiler that annotates
  C source with runtime cycle counts and stack space.

  \medskip %
  This is formalised in the Matita proof assistant, with a proof of
  correctness, and can be extracted as an executable compiler.

  \smallskip %
  \begin{itemize}
  \item Modular \blue{layering} of intensional proofs over extensional
    results;
  \item Extensional results richer than normal and carefully chosen, but do
    not require large changes to proof techniques.
  \item \blue{Compile-time checks} on intermediate code reduce proof effort.
  \item \blue{Structured traces} as a repository for invariant information.
  \item \blue{Measurable subtraces} as a unit of cost proof.
  \end{itemize}

  \smallskip %
  Going beyond this, in future projects (REMS, \dots) we plan to:
  \begin{itemize}
  \item Generalize  labelling schemes for more sophisticated targets;
  \item Apply \blue{decompilation} to jump the gap from source to binary.
  \end{itemize}

\end{frame}
\end{document}

% LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM
% LocalWords:  reexecutes subtrace RTLabs subtraces Garnier McKinna cerco
%  LocalWords:  Axiomatization axiomatized Cminor goto