Changeset 3280 for Deliverables/Dissemination

Timestamp:

May 14, 2013, 12:11:54 PM (7 years ago)

Author:

Ian Stark

Message:

Front end final review talk?

Location:

Deliverables/Dissemination/front-end/final-review

Files:

• front-end.tex (modified) (6 diffs)
• front-end.vrb (modified) (1 diff)

Deliverables/Dissemination/front-end/final-review/front-end.tex

@@ -131 +131 @@
   \end{itemize}
 
-  At the completion of Period~3, the front end included proofs of correctness
-  for all these, extension to stack usage, and considerable refinement of the
-  existing formal development.
+  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}
@@ -180 +180 @@
     \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}, sometimes similar; here we
+  \item Simulation steps with \red{many cases}, some very similar; here we
     have identified representative and more challenging cases for detailed
     proof.
@@ -187 +187 @@
 \end{frame}
 
-\begin{frame}[fragile]
-\frametitle{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
-  control flow;
-\item To a language with explicit addresses and control-flow graph.
-\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}
-
-
-% \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}
-
-Embed call structure and label invariants into execution traces.
-
-\begin{center}
-\includegraphics{strtraces.pdf}
-\end{center}
-
-\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 measurable subtraces, using the fact that labelling
-is sound and precise.
+\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 where all control flow is unconstrained jumps.
+  \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}
@@ -578 +230 @@
 \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.
+  \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}
@@ -619 +271 @@
   In addition, to link this with the source program:
   \begin{itemize}
-  \item The observables for the RLabs \blue{prefix} and \blue{structured
+  \item The observables for the RTLabs \blue{prefix} and \blue{structured
       trace} are the same as for their counterparts in Clight.
   \end{itemize}
@@ -625 +277 @@
 \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{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}
-
-}
-
+\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 Is partial --- will only succeed when invariants hold;
+  \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 that proving existence in general of this bound alone to be
+  considerably harder than the whole check.
+
+\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
+% LocalWords:  reexecutes subtrace RTLabs subtraces Garnier McKinna cerco
+%  LocalWords:  Axiomatization axiomatized Cminor goto

Deliverables/Dissemination/front-end/final-review/front-end.vrb

@@ -1 @@
-\frametitle {Putting the proof together}
+\frametitle {Checking Bound to Next Label}\par     \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}
 
-\begin{center}
-\includegraphics[width=0.8\linewidth]{compiler.pdf}
-\end{center}
+  \onslide<7->
+  When complete, we have a proof that every loop contains a label.
 
-\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}
-