source: Deliverables/Dissemination/front-end/front-end.tex @ 3264

\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{Front-end Correctness Proofs}
\author{Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark}
\institute{LFCS, University of Edinburgh\\[1ex]
\includegraphics[width=.3\linewidth]{cerco_logo.png}\\
\footnotesize Project FP7-ICT-2009-C-243881
}
\date{CerCo workshop\\23rd March 2013}
\maketitle

\frame{
\frametitle{Introduction}

The \emph{Matita} proof assistant supports writing and verification of
functional programs.

\bigskip

We
\begin{itemize}
\item formalise the CerCo compiler in Matita,
\item prove usual \red{extensional} result: \blue{functional correctness}
\item also prove \red{intensional} properties: \blue{cost bound correctness}
\end{itemize}

Talk will only mention \alert{time} costs; but also do stack.

\bigskip
\alert{Extract} compiler code from development for practical execution.

\bigskip
Informed by earlier formal experiment with a toy compiler.
}

\frame{
\frametitle{Motivation for formalisation}

\begin{enumerate}
\item Provide \alert{assurance} about labelling approach
  \begin{itemize}
  \item more complex setting than toy compiler
  \end{itemize}
\item demonstrate feasibility of \alert{certified} WCET toolchain
% Future: proof translating compiler to provide checkable WCET certificate?
\item new experiments with certified compilation:
  \begin{itemize}
  \item deeper use of \alert{dependent types}
  \item \alert{executable} semantics in type theory
  \item certification of \alert{optimising assembler}
  \end{itemize}
\end{enumerate}

\bigskip
\pause
Functional correctness for similar compilers already studied in
Leroy et al.'s \blue{CompCert}.

\bigskip
Concentrate on cost correctness.
\begin{itemize}
\item Keep \alert{extensional} proofs as separate as possible
\end{itemize}
}

\frame{
\frametitle{Outline}
\tableofcontents
}

\section{CerCo Compiler}

\frame{
\frametitle{CerCo compiler}

\begin{center}
\includegraphics[width=0.8\linewidth]{compiler-plain.pdf}
\end{center}

\begin{itemize}
\item Reuse unverified CompCert parser
%\item Transform away troublesome constructs
%  \begin{itemize}
%  \item e.g.~\texttt{switch}
%  \item fallthrough requires slightly more sophisticated labelling
%  \item but not fundamentally different
%  \end{itemize}
\item Intermediate language for most passes
\item Executable semantics for each
\item Outputs
  \begin{itemize}
  \item 8051 machine code
  \item Clight code instrumented with costs in 8051 clock cycles
  \end{itemize}
\end{itemize}
Instrumentation updates global cost variable; suitable for further analysis and
verification.
}

\section{Overall correctness}

\begin{frame}[fragile]
\frametitle{Correctness of labelling approach}

\begin{tabular}{ccc}

\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
char f(char x) {
  char y;
  _cost3:
  if (x>10) {
    _cost1:
    y = g(x);
  } else {
    _cost2:
    y = 5;
  }
  return y+1;
}
\end{lstlisting}

&

\begin{minipage}{9em}
\begin{center}
$\Rightarrow$\\[4ex]
\blue{soundness}\\[2ex]
\red{precision}
\end{center}
\end{minipage}

&

\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
  "f"
    emit _cost3
    *** Prologue ***
    move A, R06
    clear CARRY
    ...
    branch A <> 0, f10
    emit _cost2
    imm R00, 5
    ...
    f10:
    emit _cost1
    call "g"
    ...
\end{lstlisting}


\end{tabular}

From experiments with toy compiler:
\begin{enumerate}
\item Functional correctness, \emph{including trace of labels}
%\item Source labelling function is sound and precise
%\item Preservation of soundness and precision of labelling
\item Target labelling function is sound and precise
% TODO: detail about soundness and precision?
\item Target cost analysis produces a map of labels to times
  \begin{itemize}
  \item Accurate for sound and precise labellings
  \end{itemize}
%\item Correctness of instrumentation
\end{enumerate}

\end{frame}

%\frame{
%\frametitle{}
%
%Due to resource constraints
%\begin{itemize}
%\item Instrumentation is done in language semantics
%\item Soundness and precision of labelling is checked during compilation
%  \begin{itemize}
%  \item c.f.~translation validation
%  \end{itemize}
%\item Focusing effort on novel parts --- cost proofs over functional correctness
%\end{itemize}
%
%}

\begin{frame}[fragile]
\frametitle{Overall correctness statement}

\begin{center}
\fbox{\( \text{machine time} =  \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)}
\end{center}

\pause

\begin{center}
\begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c}

\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
int f(int x) {
  _cost1:
  int y = 0;
  while (x) {
    _cost2:
    y = g(y);
    x = x - 1;
  }
  _cost3:
  return y;
}
\end{lstlisting}

&

\begin{uncoverenv}<2-3>
\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
call f
_cost1
init y
_cost2
call g
...
return g
assign y
decrement x
test x
_cost2
...
_cost3
return f
\end{lstlisting}
\end{uncoverenv}

&

\begin{uncoverenv}<3-5>
\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
call f
_cost1

_cost2
call g
...
return g



_cost2
...
_cost3
return f
\end{lstlisting}
\end{uncoverenv}

\end{tabular}
\end{center}

\begin{overprint}
\onslide<2>
\begin{itemize}
\item Use labels and end of function as measurement points
\item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f'
\end{itemize}

\onslide<3-4>
\begin{itemize}
\item Use labels and end of function as measurement points
\item All costs are considered local to the function
\item Actual position of unobservable computation is unimportant
\end{itemize}

\onslide<5>
\begin{itemize}
\item Use labels and end of function as measurement points
\item[$\star$] Call suitable subtraces \alert{measurable}
\item[$\star$] Core part is a proof of \alert{termination}
\end{itemize}
\end{overprint}

\end{frame}

\begin{frame}[fragile]
\frametitle{Correct cost analysis depends on call structure}

Two straight-line functions:

\begin{center}
\begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}}

\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
"f"
  emit _cost1
  ...
  call "g"
  ...
  return
\end{lstlisting}

&

\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
                   emph={[2]_cost3},emphstyle={[2]\color{blue}},
                   escapechar=\%]
"g"
  emit _cost2
  ...
  %\only<2->{\blue{reduce return address}}%
  return
\end{lstlisting}

\end{tabular}
\end{center}

Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}).

\begin{itemize}
\item<2-> Changing return address reexecutes code from \lstinline'f'
\item<2-> Cost no longer equals sum of cost labels
\end{itemize}

\onslide<2->
\alert{Need to enforce correct call/return structure.}

\onslide<3>
\emph{Not easy to observe at ASM.}

\end{frame}

\section{Front-end correctness}

\frame{
\frametitle{Front-end correctness}

Recalling the toy compiler, need
\begin{enumerate}
\item Functional correctness
\item Cost labelling sound and precise
\item\label{it:return} To demonstrate return addresses are correct
\end{enumerate}
% TODO: stack space?  from obs, from fnl correctness

\bigskip
For~\ref{it:return} we generalise notion of \emph{structured traces}
originally introduced for the correctness of timing analysis.
}

\begin{frame}[fragile]
\frametitle{Structured traces}

\alert{Embed} the call/return structure into execution traces.

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

\begin{itemize}
\item Traces of \alert{called functions} are nested
\item Invariants on positions of cost labels enforced
\item Steps are \alert{grouped} according to cost label
\end{itemize}

\onslide<2>
Construct by folding up \alert{measurable} subtrace, using soundness
and preciseness of labelling.

\end{frame}

\frame{
\frametitle{Front-end correctness statement}

We start with a \blue{measurable} subtrace of an execution, and the
\textbf{prefix} of that trace from initial state.

\medskip
Need:
\begin{itemize}
\item Functional correctness for \textbf{prefix}
\item \red{Structured trace} corresponding to \blue{measurable}
  subtrace
\item Proof that no PC \red{repeats} in structured trace,\\ to ensure
  \blue{sound} labelling
\item \textbf{Observables} preserved
\item \textbf{Stack limit} observed
\end{itemize}

}

\begin{frame}[fragile]
\frametitle{Structure in the compiler proof}

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

%\onslide<1>
%\green{Assembler} provides part of local cost analysis (CPP'12).

%\onslide<2-4>
Switch at RTLabs:
\begin{itemize}
\item from \red{measurable} subtrace of \alert{sound} and \alert{precise}
labelling
\item to \blue{structured trace} where they are embedded
\end{itemize}

%\onslide<3>
%Changes \blue{syntactic} properties of labelling into \blue{semantic}
%properties.

%\onslide<4>
Reason for choice: first language with explicit \alert{addresses}, implicit
\alert{call handling}.

\end{frame}

\section{Correctness proofs}
\subsection{Generic lifting result}

\begin{frame}[fragile]
\frametitle{Front-end measurable traces (Clight to RTLabs)}

There is a \alert{measurable} RTLabs subtrace \alert{equivalent} to any
\alert{measurable} Clight subtrace.

\bigskip

\onslide<2->
Split normal simulation proof into three:
\begin{enumerate}
\item \blue{call/return} steps become a \blue{call/return} step 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}

\bigskip
\onslide<3->
Preserves the essential termination property for \alert{measurable} subtraces.

\bigskip
\onslide<4->
Due to time pressures, check \alert{soundness} and \alert{precision} of cost
labels at RTLabs.

\end{frame}

%\begin{frame}[fragile]
%\frametitle{Structured trace simulation}
%
%Lift \alert{local} simulations to \alert{structured trace} simulations
%similarly.
%
%\bigskip
%\pause
%\begin{itemize}
%\item
%Require local simulations for \alert{normal}, \alert{call} and \alert{return}
%steps
%\item allow traces to expand with extra \alert{normal} steps,
%\item allow us to collapse some \alert{normal} steps
%  \begin{itemize}
%  \item but not collapse \blue{labelled} steps
%  % TODO: why?  avoid larger change in structure
%  \item or change call structure
%  \end{itemize}
%\end{itemize}
%
%\bigskip
%Sufficient to calculate structured trace in target.
%% TODO: pics
%
%\end{frame}
%
%\begin{frame}[fragile]
%\frametitle{Structured trace local simulation example}
%
%For function call steps:
%\begin{center}
%\includegraphics[width=0.7\linewidth]{strcall.pdf}
%\end{center}
%
%\begin{itemize}
%\item May add extra steps before and after
%\item Extra steps must not be call/return
%\item Must call the same function
%\item Cost label must stay at start of function
%\end{itemize}
%
%\end{frame}

\subsection{Simulations for compiler passes}

%\frame{
%\frametitle{TODO: at least two slides on simulations}
%}

% TODO: perhaps much earlier for the pre-measurable bits?
\frame{
\frametitle{Simulation between input and annotated code}

Two stages provide the annotated version of input:

\bigskip
Switch removal
\begin{itemize}
\item \lstinline[language=C]'switch' statement control flow too subtle
  for simple labelling
\item Replaces with \lstinline[language=C]'if ... then ... else' tree
\item Tricky part of proof memory extension for extra variable
\item Partial proof: validate approach, but not relevant to
  intensional properties
\end{itemize}

\bigskip
Cost labelling
\begin{itemize}
\item For simulation don't care \emph{which} labels are added
\item Just have to skip over extra cost label expressions and
  statements
\item Complete simulation proof, simple
\end{itemize}

% TODO: consider whether to mention full simulation
% termination-preserving proof?
}

\frame{
\frametitle{Front-end simulation results}
Cast simplification
\begin{itemize}
\item Simplify expressions for 8-bit target
\item Only expressions change --- statements are in lock-step
\item Difficult part: we allow ill-typed \textbf{Clight} at this stage
\item Simulation proofs complete
\end{itemize}

\textbf{Clight} to \textbf{Cminor}
\begin{itemize}
\item Stack allocation and control flow transformation
\item Similar to \textbf{CompCert}, but produces \lstinline'goto'
  instead of \lstinline'loop'
\item Expressions complete
\item Prove a selection of statements, in particular \lstinline'while'
\item Tricky: Large proof terms for invariant embedded in
  \textbf{Cminor} programs using dependent types;\\
  generalise them away, but difficult under binders
%TODO explain clearly
\end{itemize}
}
\frame{
\frametitle{Front-end simulation results}
\textbf{Cminor} to \textbf{RTLabs}
\begin{itemize}
\item Construction of control-flow graph
\item Axiomatized simulations
\item But do have invariants:
  \begin{itemize}
  \item Statement well-typed with respect to pseudo-register
    environment
  \item CFG complete
  \item Entry and exit nodes complete, unique
  \end{itemize}
\item Translation function is \emph{total} as a result
\end{itemize}
}

% TODO: sloganize: proved more about unusual bits

\section{Checking cost labelling properties}

\frame{
\frametitle{Checking cost labelling properties}

Check cost labelling is \red{sound} and \blue{precise} at
\textbf{RTLabs}.
\begin{itemize}
\item Shortcut; similar to translation validation
\end{itemize}

\medskip
At \textbf{RTLabs} properties become
\begin{description}
\item[\red{soundness}] bound on number of instructions in CFG until label\\
label at start of every function
\item[\blue{precision}]  label after every branch
\end{description}

\medskip
Bound is the hard part; the rest is a simple syntactic check.
}

\begin{frame}[fragile]
\frametitle{Bound on number of instructions until label}

\begin{center}
\includegraphics<1>[width=.4\linewidth]{loop.pdf}
\includegraphics<2>[width=.4\linewidth]{loop1.pdf}
\includegraphics<3>[width=.4\linewidth]{loop2.pdf}
\includegraphics<4>[width=.4\linewidth]{loop3.pdf}
\includegraphics<5>[width=.4\linewidth]{loop4.pdf}
\includegraphics<6>[width=.4\linewidth]{loopx.pdf}
\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} the labelling is unsound,
  report an error
\end{itemize}

\end{frame}

\frame{
\frametitle{Checking cost labelling properties}

This compile-time check is
\begin{itemize}
\item[$-$] partial
\item[$-$] extra work in compilation
\item[$\mp$] not proving anything about compilation passes
\item[$+$] less proof burden
\end{itemize}

\bigskip
Constructing the bound between \textbf{Cminor} and \textbf{RTLabs}
likely to be at least as expensive as this check.

}

\section{Construction of structured traces}

\frame{
\frametitle{Construction of structured traces}
\begin{center}
\includegraphics{strtraces.pdf}
\end{center}
\begin{enumerate}
\item Extend sound and precise labelling to semantic states
\item Prove they are preserved by steps of semantics
\item Prove \textbf{RTLabs} semantics preserve the stack
\item Use \alert{termination} proof from \alert{measurable} subtrace
  to create structure
\item Proof obligations for cost labelling are discharged by semantic
  results above
\end{enumerate}
}

\section{Whole compiler}

\begin{frame}[fragile]
\frametitle{Putting the proof together}

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

\begin{itemize}
\item `Clock' difference in Clight is sum of cost labels
\item Trace of labels is preserved to ASM
\item Labelling at bottom level is sound and precise
\item Sum of labels at ASM is equal to difference in real clock
\end{itemize}

Also preserve observables.

\end{frame}

\frame{
\frametitle{Conclusion}

Sketched proof for formalised CerCo compiler

\begin{itemize}
\item Preserving trace structure provides correctness in more challenging
  setting
\item Finishing off formal proof
  \begin{itemize}
  \item axioms for some regular simulation results
  \item concentrating on intensional proofs
  \end{itemize}
\item[$\star$] Don't need huge changes to extensional proof techniques
\end{itemize}

\pause
Future:
\begin{itemize}
\item Expect results to generalise to more general labelling schemes
  \begin{itemize}
  \item hence more sophisticated targets
  \end{itemize}
\item Other compiler correctness techniques
  \begin{itemize}
  \item Decompilation?
  \end{itemize}
\end{itemize}

}

\end{document}

% LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM
% LocalWords:  reexecutes subtrace RTLabs subtraces