source: Deliverables/D3.4/Report/report.tex @ 3140

\documentclass[11pt,epsf,a4wide]{article}
\usepackage[mathletters]{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{listings}
\usepackage{../../style/cerco}
\newcommand{\ocaml}{OCaml}
\newcommand{\clight}{Clight}
\newcommand{\matita}{Matita}
\newcommand{\sdcc}{\texttt{sdcc}}

\newcommand{\textSigma}{\ensuremath{\Sigma}}

% LaTeX Companion, p 74
\newcommand{\todo}[1]{\marginpar{\raggedright - #1}}

\lstdefinelanguage{coq}
  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
   morekeywords={[2]if,then,else},
  }

\lstdefinelanguage{matita}
  {keywords={definition,lemma,theorem,remark,inductive,record,qed,let,rec,match,with,Type,and,on},
   morekeywords={[2]whd,normalize,elim,cases,destruct},
   mathescape=true,
   morecomment=[n]{(*}{*)},
  }

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

\lstset{extendedchars=false}
\lstset{inputencoding=utf8x}
\DeclareUnicodeCharacter{8797}{:=}
\DeclareUnicodeCharacter{10746}{++}
\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}


\title{
INFORMATION AND COMMUNICATION TECHNOLOGIES\\
(ICT)\\
PROGRAMME\\
\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}

\date{ }
\author{}

\begin{document}
\thispagestyle{empty}

\vspace*{-1cm}
\begin{center}
\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
\end{center}

\begin{minipage}{\textwidth}
\maketitle
\end{minipage}


\vspace*{0.5cm}
\begin{center}
\begin{LARGE}
\bf
Report n. D3.4\\
Front-end Correctness Proofs\\
\end{LARGE} 
\end{center}

\vspace*{2cm}
\begin{center}
\begin{large}
Version 1.0
\end{large}
\end{center}

\vspace*{0.5cm}
\begin{center}
\begin{large}
Authors:\\
Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark
\end{large}
\end{center}

\vspace*{\fill}
\noindent
Project Acronym: \cerco{}\\
Project full title: Certified Complexity\\
Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\

\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}

\newpage

\vspace*{7cm}
\paragraph{Abstract}
We report on the correctness proofs for the front-end of the \cerco{} cost
lifting compiler, considering three distinct parts of the task: showing that
the \emph{annotated source code} output by the compiler has equivalent
behaviour to the original input (up to the annotations); showing that a
\emph{measurable} subtrace of the annotated source code corresponds to an
equivalent measurable subtrace in the code produced by the front-end, including
costs; and finally showing that the enriched \emph{structured} execution traces
required for cost correctness in the back-end can be constructed from the 
properties of the code produced by the front-end.

A key part of our work is that the intensional correctness results that show
that we get consistent cost measurements throughout the intermediate languages
of the compiler can be layered on top of normal forward simulation results,
if we split them into local call-structure preserving results.

This deliverable shows correctness results about the formalised compiler
described in D3.2, using the source language semantics from D3.1 and
intermediate language semantics from D3.3.  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?

\newpage 

\tableofcontents

% CHECK: clear up any -ize vs -ise
% CHECK: clear up any "front end" vs "front-end"
% CHECK: clear up any mentions of languages that aren't textsf'd.
% CHECK: fix unicode in listings

\section{Introduction}

TODO: briefly, cerco compiler's purpose, prototype, formalisation, whole
compiler.  Full functional correctness too ambitious; fortunately get nice
layering of intensional correctness on top of mildly refined normal simulations.
Hence, concentrate on new intensional correctness results; add stack space for
more precise statement.  Also do some
translation validation on sound, precise labelling properties.  Fluffly version
of correctness statement.

The \cerco{} compiler compiles C code targeting microcontrollers implementing
the Intel 8051 architecture, which produces both the object code and source
code containing annotations describing the timing behavior 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 that version of the compiler, and how that fits
into the verification of the whole compiler.

% TODO: maybe mention stack space here?  other additions?  refer to "layering"?
A key part of this work was to separate the proofs about the compiled code's
extensional behaviour (that is, the functional correctness of the compiler)
from the intensional correctness that the costs given are correct.
Unfortunately, the ambitious goal of completely verifying the 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 projects and concentrate on the novel
intensional proofs.  The proofs were also made more tractable by introducing
compile-time checks for the `sound and precise' cost labelling properties
rather than proving that they are preserved throughout.

The overall statement of correctness says that the annotated program has the
same behaviour as the input, and that for any suitably well-structured part of
the execution (which we call \emph{measurable}), the object code will execute
the same behaviour taking precisely the time given by the cost annotations in
the annotated source program.

In the next section we recall the structure of the compiler and make the overall
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.  TODO: rest of document structure

\section{The compiler and main goals}

TODO: outline compiler, maybe figure from talk, maybe something like the figure
below.

TODO: might want a version of this figure
\begin{figure}
\begin{center}
\begin{minipage}{.8\linewidth}
\begin{tabbing}
\quad \= $\downarrow$ \quad \= \kill
\textsf{C} (unformalized)\\
\> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
\textsf{Clight}\\
\> $\downarrow$ \> cast removal\\
\> $\downarrow$ \> add runtime functions\\
\> $\downarrow$ \> labelling\\
\> $\downarrow$ \> stack variable allocation and control structure
 simplification\\
\textsf{Cminor}\\
\> $\downarrow$ \> generate global variable initialization code\\
\> $\downarrow$ \> transform to RTL graph\\
\textsf{RTLabs}\\
\> $\downarrow$ \> start of target specific back-end\\
\>\quad \vdots
\end{tabbing}
\end{minipage}
\end{center}
\caption{Front-end languages and transformations}
\label{fig:summary}
\end{figure}

The compiler function returns the following record 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
 }.
\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.}, a cost label covering the
initialisation of global variables and calling the
\lstinline[language=C]'main' function, the annotated source code, and
finally a mapping from cost labels to actual execution time 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.  \todo{Cross-ref case study
deliverables}

\subsection{Revisions to the prototype compiler}

TODO: could be a good idea to have this again

\subsection{Main goals}

TODO: need an example for this

Informally, our main intensional result links the time difference in a source
code execution to the time difference in the object code, expressing the time
for the source by summing the values for the cost labels in the trace, and the
time for the target by a clock built in to the 8051 executable semantics.

The availability of precise timing information for 8501
implementations and the design of the compiler allow it to give exact
time costs in terms of processor cycles.  However, these exact results
are only available if the subtrace we measure starts and ends at
suitable points.  In particular, pure computation with no observable
effects may be reordered and moved past cost labels, so we cannot
measure time between arbitrary statements in the program.

There is also a constraint on the subtraces that we
measure due to the requirements of the correctness proof for the
object code timing analysis.  To be sure that the timings are assigned
to the correct cost label, we need to know that each return from a
function call must go to the correct return address.  It is difficult
to observe this property locally in the object code because it relies
on much earlier stages in the compiler.  To convey this information to
the timing analysis extra structure is imposed on the subtraces, which
we will give more details on in Section~\ref{sec:fegoals}.

% Regarding the footnote, would there even be much point?
These restrictions are reflected in the subtraces that we give timing
guarantees on; they must start at a cost label and end at the return
of the enclosing function of the cost label\footnote{We expect that
  this would generalise to subtraces between cost labels in the same
  function, but could not justify the extra complexity that would be
  required to show this.}.  A typical example of such a subtrace is
the execution of an entire function from the cost label at the start
of the function until it returns.  We call such any such subtrace
\emph{measurable} if it (and the prefix of the trace before it) can
also be executed within the available stack space.

Now we can give the main intensional statement for the compiler.
Given a \emph{measurable} subtrace for a labelled \textsf{Clight}
program, there is a subtrace of the 8051 object code program where the
time differences match.  Moreover, \emph{observable} parts of the
trace also match --- these are the appearance of cost labels and
function calls and returns.

More formally, the definition of this statement in \matita{} is
\begin{lstlisting}[language=matita]
definition simulates := 
  $\lambda$p: compiler_output.
  let initial_status := initialise_status $\dots$ (cm (c_labelled_object_code $\dots$ p)) in
  $\forall$m1,m2.
   measurable Clight_pcs (c_labelled_clight $\dots$ p) m1 m2
    (lookup_stack_cost (c_stack_cost $\dots$ p)) (c_max_stack $\dots$ p) $\rightarrow$
  $\forall$c1,c2.
   clock_after Clight_pcs (c_labelled_clight $\dots$ p) m1 (c_clight_cost_map $\dots$ p) = OK $\dots$ c1 $\rightarrow$
   clock_after Clight_pcs (c_labelled_clight $\dots$ p) (m1+m2) (c_clight_cost_map $\dots$ p) = OK $\dots$ c2 $\rightarrow$
  $\exists$n1,n2.
   observables Clight_pcs (c_labelled_clight $\dots$ p) m1 m2 =
   observables (OC_preclassified_system (c_labelled_object_code $\dots$ p))
    (c_labelled_object_code $\dots$ p) n1 n2
  $\wedge$
   c2 - c1 = clock $\dots$ (execute n2 ? initial_status) - clock $\dots$ (execute n1 ? initial_status).
\end{lstlisting}
where the \lstinline'measurable', \lstinline'clock_after' and
\lstinline'observables' definitions can be applied to multiple
languages; in this case the \lstinline'Clight_pcs' record applies them
to \textsf{Clight} programs.

There is a second part to the statement, which says that the initial
processing of the input program to produce the cost labelled version
does not affect the semantics of the program:
% Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function
\begin{lstlisting}[language=matita]
  $\forall$input_program,output.
  compile input_program = return output $\rightarrow$
  not_wrong … (exec_inf … clight_fullexec input_program) $\rightarrow$
  sim_with_labels
   (exec_inf … clight_fullexec input_program)
   (exec_inf … clight_fullexec (c_labelled_clight … output))
\end{lstlisting}
That is, any successful compilation produces a labelled program that
has identical behaviour to the original, so long as there is no
`undefined behaviour'.

Note that this provides full functional correctness, including
preservation of (non-)termination.  The intensional result above does
not do this directly --- it does not guarantee the same result or same
termination.  There are two mitigating factors, however: first, to
prove the intensional property you need local simulation results that
can be pieced together to form full behavioural equivalence, only time
constraints have prevented us from doing so.  Second, if we wish to
confirm a result, termination, or non-termination we could add an
observable witness, such as a function that is only called if the
correct result is given.  The intensional result guarantees that the
observable witness is preserved, so the program must behave correctly.

\section{Intermediate goals for the front-end}
\label{sec:fegoals}

The essential parts of the intensional proof were outlined during work
on a toy
compiler~\cite{d2.1,springerlink:10.1007/978-3-642-32469-7_3}.  These
are
\begin{enumerate}
\item functional correctness, in particular preserving the trace of
  cost labels,
\item the \emph{soundness} and \emph{precision} of the cost labelling
  on the object code, and
\item the timing analysis on the object code produces a correct
  mapping from cost labels to time.
\end{enumerate}

However, that toy development did not include function calls.  For the
full \cerco{} compiler we also need to maintain the invariant that
functions return to the correct program location in the caller, as we
mentioned in the previous section.  During work on the back-end timing
analysis (describe in more detail in the companion deliverable, D4.4)
the notion of a \emph{structured trace} was developed to enforce this
return property, and also most of the cost labelling properties too.

\begin{figure}
\begin{center}
\includegraphics[width=0.5\linewidth]{compiler.pdf}
\end{center}
\caption{The compiler and proof outline}
\label{fig:compiler}
\end{figure}

Jointly, we generalised the structured traces to apply to any of the
intermediate languages with some idea of program counter.  This means
that they are introduced part way through the compiler, see
Figure~\ref{fig:compiler}.  Proving that a structured trace can be
constructed at \textsf{RTLabs} has several virtues:
\begin{itemize}
\item This is the first language where every operation has its own
  unique, easily addressable, statement.
\item Function calls and returns are still handled in the language and
  so the structural properties are ensured by the semantics.
\item Many of the back-end languages from \textsf{RTL} share a common
  core set of definitions, and using structured traces throughout
  increases this uniformity.
\end{itemize}

\begin{figure}
\begin{center}
\includegraphics[width=0.6\linewidth]{strtraces.pdf}
\end{center}
\caption{Nesting of functions in structured traces}
\label{fig:strtrace}
\end{figure}
A structured trace is a mutually inductive data type which principally
contains the steps from a normal program trace, but arranged into a
nested structure which groups entire function calls together and
aggregates individual steps between cost labels (or between the final
cost label and the return from the function), see
Figure~\ref{fig:strtrace}.  This capture the idea that the cost labels
only represent costs \emph{within} a function --- calls to other
functions are accounted for in the trace for their execution, and we
can locally regard function calls as a single step.

These structured traces form the core part of the intermediate results
that we must prove so that the back-end can complete the main
intensional result stated above.  In full, we provide the back-end
with
\begin{enumerate}
\item A normal trace of the \textbf{prefix} of the program's execution
  before reaching the measurable subtrace.  (This needs to be
  preserved so that we know that the stack space consumed is correct.)
\item The \textbf{structured trace} corresponding to the measurable
  subtrace.
\item An additional property about the structured trace that no
  `program counter' is \textbf{repeated} between cost labels.  Together with
  the structure in the trace, this takes over from showing that
  cost labelling is sound and precise.
\item A proof that the \textbf{observables} have been preserved.
\item A proof that the \textbf{stack limit} is still observed by the prefix and
  the structure trace.  (This is largely a consequence of the
  preservation of observables.)
\end{enumerate}

Following the outline in Figure~\ref{fig:compiler}, we will first deal
with the transformations in \textsf{Clight} that produce the source
program with cost labels, then show that measurable traces can be
lifted to \textsf{RTLabs}, and finally that we can construct the
properties listed above ready for the back-end proofs.

\section{Input code to cost labelled program}

The simple form of labelling used in the formalised compiler is not
quite capable of capturing costs arising from complex C
\lstinline[language=C]'switch' statements, largely due to the
fall-through behaviour.  Our first pass replaces these statements with
simpler C code, allowing our second pass to perform the cost
labelling.  We show that the behaviour of programs is unchanged by
these passes.

TODO: both give one-step-sim-by-many forward sim results; switch
removal tricky, uses aux var to keep result of expr, not central to
intensional correctness so curtailed proof effort once reasonable
level of confidence in code gained; labelling much simpler; don't care
what the labels are at this stage, just need to know when to go
through extra steps.  Rolled up into a single result with a cofixpoint
to obtain coinductive statement of equivalence (show).

\section{Finding corresponding measurable subtraces}

\section{Existence of a structured trace}
\label{sec:structuretrace}

\section{Conclusion}

TODO

\bibliographystyle{plain}
\bibliography{report}

\end{document}