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

\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 review meeting\\16th May 2013}
\maketitle

\frame{
\frametitle{Introduction}

D3.4 is the front-end correctness proofs:

\begin{description}
\item[Primary focus:] novel \red{intensional} properties: \blue{cost
    bound correctness}
\item[Secondary:] usual \red{extensional} result: \blue{functional correctness}
\end{description}

Functional correctness for similar compilers already studied in
Leroy et al.'s \blue{CompCert}.
\begin{itemize}
\item Axiomatize similar results
\end{itemize}

\medskip
Now have \blue{stack} costs as well as \blue{time}
\begin{itemize}
\item yields stronger overall correctness result
\end{itemize}

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

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

% TODO: could reuse some of this to make stronger intro?
% \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

% \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 and
    bytes of stack space
  \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 [D2.1, FMICS'12]:
\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{increase 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 skips code from \lstinline'f'
\item<2-> Cost no longer equals sum of cost labels
\end{itemize}

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

\onslide<3>
\emph{Not easy at ASM --- observe earlier in compiler \& maintain.}

\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
\item Forbid \alert{repeating} addresses in grouped steps for
  \blue{sound} labelling
\end{itemize}

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

\end{frame}

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

Given a \blue{measurable} subtrace of a \textbf{Clight} execution, including
the \textbf{prefix} of that trace from initial state,

\medskip
we have in \textbf{RTLabs}
\begin{itemize}
\item a new \textbf{prefix}
\item a \red{structured trace} corresponding to \blue{measurable}
  subtrace
\item the no \red{repeating} addresses property
\item proof that the same \textbf{stack limit} is observed
\end{itemize}
which the back-end requires, and
\begin{itemize}
\item the observables for the \textbf{prefix} and \red{structured
    trace} are the same as their \textbf{Clight} counterparts
\end{itemize}
which links the behaviour and costs to the original program.
}

\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{Lifting measurable traces}

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

\bigskip

\onslide<2->
\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}

\bigskip
\onslide<3->
Preserves the defining 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
In a full proof would go from
\begin{quote}
  cost labels at the head of loops in \textbf{Cminor}
\end{quote}
to
\begin{quote}
  bound on instructions to cost label in \textbf{RTLabs}
\end{quote}
Showing existence of the bound alone likely to require at least as much
proof effort 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 Observables, including 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}

\end{frame}

\frame{
\frametitle{Conclusion}

Sketched proof for formalised CerCo front-end

\begin{itemize}
\item Intensional proofs can be layered on top of extensional results
\item Preserving call-structure key ingredient
\item Compile-time cost labelling checks can reduce proof burden
\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