source: Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex @ 2941

\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{A certified proof based on structured traces}
\author{Brian Campbell}
\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{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.
}

\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{Goal}

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

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

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

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


\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 Translation validation?
  \end{itemize}
\end{itemize}

}

\end{document}

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