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

Last change on this file since 3264 was 3264, checked in by campbell, 8 years ago

Draft a bit of missing content for front-end slides.

File size: 17.5 KB
Line 
1\documentclass[nopanel]{beamer}
2\usepackage{graphicx,color}
3\usepackage{amsfonts}
4\usepackage{listings}
5
6\lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
7        keywordstyle=\color{red}\bfseries,
8        keywordstyle=[2]\color{blue},
9        commentstyle=\color{green},
10        stringstyle=\color{blue},
11        showspaces=false,showstringspaces=false}
12
13
14\setbeamertemplate{footline}[page number]
15\setbeamertemplate{sidebar right}{}
16
17\setbeamercolor{alerted text}{fg=red!70!orange}
18
19\newcommand{\red}[1]{\textcolor{red}{#1}}
20\newcommand{\blue}[1]{\textcolor{blue}{#1}}
21\newcommand{\green}[1]{\textcolor{green}{#1}}
22\newcommand{\grey}[1]{\textcolor{grey}{#1}}
23
24\addtolength{\parskip}{0.3em}
25
26\begin{document}
27
28\title{Front-end Correctness Proofs}
29\author{Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark}
30\institute{LFCS, University of Edinburgh\\[1ex]
31\includegraphics[width=.3\linewidth]{cerco_logo.png}\\
32\footnotesize Project FP7-ICT-2009-C-243881
33}
34\date{CerCo workshop\\23rd March 2013}
35\maketitle
36
37\frame{
38\frametitle{Introduction}
39
40The \emph{Matita} proof assistant supports writing and verification of
41functional programs.
42
43\bigskip
44
45We
46\begin{itemize}
47\item formalise the CerCo compiler in Matita,
48\item prove usual \red{extensional} result: \blue{functional correctness}
49\item also prove \red{intensional} properties: \blue{cost bound correctness}
50\end{itemize}
51
52Talk will only mention \alert{time} costs; but also do stack.
53
54\bigskip
55\alert{Extract} compiler code from development for practical execution.
56
57\bigskip
58Informed by earlier formal experiment with a toy compiler.
59}
60
61\frame{
62\frametitle{Motivation for formalisation}
63
64\begin{enumerate}
65\item Provide \alert{assurance} about labelling approach
66  \begin{itemize}
67  \item more complex setting than toy compiler
68  \end{itemize}
69\item demonstrate feasibility of \alert{certified} WCET toolchain
70% Future: proof translating compiler to provide checkable WCET certificate?
71\item new experiments with certified compilation:
72  \begin{itemize}
73  \item deeper use of \alert{dependent types}
74  \item \alert{executable} semantics in type theory
75  \item certification of \alert{optimising assembler}
76  \end{itemize}
77\end{enumerate}
78
79\bigskip
80\pause
81Functional correctness for similar compilers already studied in
82Leroy et al.'s \blue{CompCert}.
83
84\bigskip
85Concentrate on cost correctness.
86\begin{itemize}
87\item Keep \alert{extensional} proofs as separate as possible
88\end{itemize}
89}
90
91\frame{
92\frametitle{Outline}
93\tableofcontents
94}
95
96\section{CerCo Compiler}
97
98\frame{
99\frametitle{CerCo compiler}
100
101\begin{center}
102\includegraphics[width=0.8\linewidth]{compiler-plain.pdf}
103\end{center}
104
105\begin{itemize}
106\item Reuse unverified CompCert parser
107%\item Transform away troublesome constructs
108%  \begin{itemize}
109%  \item e.g.~\texttt{switch}
110%  \item fallthrough requires slightly more sophisticated labelling
111%  \item but not fundamentally different
112%  \end{itemize}
113\item Intermediate language for most passes
114\item Executable semantics for each
115\item Outputs
116  \begin{itemize}
117  \item 8051 machine code
118  \item Clight code instrumented with costs in 8051 clock cycles
119  \end{itemize}
120\end{itemize}
121Instrumentation updates global cost variable; suitable for further analysis and
122verification.
123}
124
125\section{Overall correctness}
126
127\begin{frame}[fragile]
128\frametitle{Correctness of labelling approach}
129
130\begin{tabular}{ccc}
131
132\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
133                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
134char f(char x) {
135  char y;
136  _cost3:
137  if (x>10) {
138    _cost1:
139    y = g(x);
140  } else {
141    _cost2:
142    y = 5;
143  }
144  return y+1;
145}
146\end{lstlisting}
147
148&
149
150\begin{minipage}{9em}
151\begin{center}
152$\Rightarrow$\\[4ex]
153\blue{soundness}\\[2ex]
154\red{precision}
155\end{center}
156\end{minipage}
157
158&
159
160\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
161                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
162  "f"
163    emit _cost3
164    *** Prologue ***
165    move A, R06
166    clear CARRY
167    ...
168    branch A <> 0, f10
169    emit _cost2
170    imm R00, 5
171    ...
172    f10:
173    emit _cost1
174    call "g"
175    ...
176\end{lstlisting}
177
178
179\end{tabular}
180
181From experiments with toy compiler:
182\begin{enumerate}
183\item Functional correctness, \emph{including trace of labels}
184%\item Source labelling function is sound and precise
185%\item Preservation of soundness and precision of labelling
186\item Target labelling function is sound and precise
187% TODO: detail about soundness and precision?
188\item Target cost analysis produces a map of labels to times
189  \begin{itemize}
190  \item Accurate for sound and precise labellings
191  \end{itemize}
192%\item Correctness of instrumentation
193\end{enumerate}
194
195\end{frame}
196
197%\frame{
198%\frametitle{}
199%
200%Due to resource constraints
201%\begin{itemize}
202%\item Instrumentation is done in language semantics
203%\item Soundness and precision of labelling is checked during compilation
204%  \begin{itemize}
205%  \item c.f.~translation validation
206%  \end{itemize}
207%\item Focusing effort on novel parts --- cost proofs over functional correctness
208%\end{itemize}
209%
210%}
211
212\begin{frame}[fragile]
213\frametitle{Overall correctness statement}
214
215\begin{center}
216\fbox{\( \text{machine time} =  \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)}
217\end{center}
218
219\pause
220
221\begin{center}
222\begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c}
223
224\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
225                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
226int f(int x) {
227  _cost1:
228  int y = 0;
229  while (x) {
230    _cost2:
231    y = g(y);
232    x = x - 1;
233  }
234  _cost3:
235  return y;
236}
237\end{lstlisting}
238
239&
240
241\begin{uncoverenv}<2-3>
242\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
243                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
244call f
245_cost1
246init y
247_cost2
248call g
249...
250return g
251assign y
252decrement x
253test x
254_cost2
255...
256_cost3
257return f
258\end{lstlisting}
259\end{uncoverenv}
260
261&
262
263\begin{uncoverenv}<3-5>
264\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
265                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
266call f
267_cost1
268
269_cost2
270call g
271...
272return g
273
274
275
276_cost2
277...
278_cost3
279return f
280\end{lstlisting}
281\end{uncoverenv}
282
283\end{tabular}
284\end{center}
285
286\begin{overprint}
287\onslide<2>
288\begin{itemize}
289\item Use labels and end of function as measurement points
290\item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f'
291\end{itemize}
292
293\onslide<3-4>
294\begin{itemize}
295\item Use labels and end of function as measurement points
296\item All costs are considered local to the function
297\item Actual position of unobservable computation is unimportant
298\end{itemize}
299
300\onslide<5>
301\begin{itemize}
302\item Use labels and end of function as measurement points
303\item[$\star$] Call suitable subtraces \alert{measurable}
304\item[$\star$] Core part is a proof of \alert{termination}
305\end{itemize}
306\end{overprint}
307
308\end{frame}
309
310\begin{frame}[fragile]
311\frametitle{Correct cost analysis depends on call structure}
312
313Two straight-line functions:
314
315\begin{center}
316\begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}}
317
318\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
319                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
320"f"
321  emit _cost1
322  ...
323  call "g"
324  ...
325  return
326\end{lstlisting}
327
328&
329
330\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
331                   emph={[2]_cost3},emphstyle={[2]\color{blue}},
332                   escapechar=\%]
333"g"
334  emit _cost2
335  ...
336  %\only<2->{\blue{reduce return address}}%
337  return
338\end{lstlisting}
339
340\end{tabular}
341\end{center}
342
343Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}).
344
345\begin{itemize}
346\item<2-> Changing return address reexecutes code from \lstinline'f'
347\item<2-> Cost no longer equals sum of cost labels
348\end{itemize}
349
350\onslide<2->
351\alert{Need to enforce correct call/return structure.}
352
353\onslide<3>
354\emph{Not easy to observe at ASM.}
355
356\end{frame}
357
358\section{Front-end correctness}
359
360\frame{
361\frametitle{Front-end correctness}
362
363Recalling the toy compiler, need
364\begin{enumerate}
365\item Functional correctness
366\item Cost labelling sound and precise
367\item\label{it:return} To demonstrate return addresses are correct
368\end{enumerate}
369% TODO: stack space?  from obs, from fnl correctness
370
371\bigskip
372For~\ref{it:return} we generalise notion of \emph{structured traces}
373originally introduced for the correctness of timing analysis.
374}
375
376\begin{frame}[fragile]
377\frametitle{Structured traces}
378
379\alert{Embed} the call/return structure into execution traces.
380
381\begin{center}
382\includegraphics{strtraces.pdf}
383\end{center}
384
385\begin{itemize}
386\item Traces of \alert{called functions} are nested
387\item Invariants on positions of cost labels enforced
388\item Steps are \alert{grouped} according to cost label
389\end{itemize}
390
391\onslide<2>
392Construct by folding up \alert{measurable} subtrace, using soundness
393and preciseness of labelling.
394
395\end{frame}
396
397\frame{
398\frametitle{Front-end correctness statement}
399
400We start with a \blue{measurable} subtrace of an execution, and the
401\textbf{prefix} of that trace from initial state.
402
403\medskip
404Need:
405\begin{itemize}
406\item Functional correctness for \textbf{prefix}
407\item \red{Structured trace} corresponding to \blue{measurable}
408  subtrace
409\item Proof that no PC \red{repeats} in structured trace,\\ to ensure
410  \blue{sound} labelling
411\item \textbf{Observables} preserved
412\item \textbf{Stack limit} observed
413\end{itemize}
414
415}
416
417\begin{frame}[fragile]
418\frametitle{Structure in the compiler proof}
419
420\begin{center}
421\includegraphics[width=0.8\linewidth]{compiler.pdf}
422\end{center}
423
424%\onslide<1>
425%\green{Assembler} provides part of local cost analysis (CPP'12).
426
427%\onslide<2-4>
428Switch at RTLabs:
429\begin{itemize}
430\item from \red{measurable} subtrace of \alert{sound} and \alert{precise}
431labelling
432\item to \blue{structured trace} where they are embedded
433\end{itemize}
434
435%\onslide<3>
436%Changes \blue{syntactic} properties of labelling into \blue{semantic}
437%properties.
438
439%\onslide<4>
440Reason for choice: first language with explicit \alert{addresses}, implicit
441\alert{call handling}.
442
443\end{frame}
444
445\section{Correctness proofs}
446\subsection{Generic lifting result}
447
448\begin{frame}[fragile]
449\frametitle{Front-end measurable traces (Clight to RTLabs)}
450
451There is a \alert{measurable} RTLabs subtrace \alert{equivalent} to any
452\alert{measurable} Clight subtrace.
453
454\bigskip
455
456\onslide<2->
457Split normal simulation proof into three:
458\begin{enumerate}
459\item \blue{call/return} steps become a \blue{call/return} step plus zero or
460  more \blue{normal} steps
461\item \blue{cost} label steps are preserved
462\item other \blue{normal} steps become zero or more \blue{normal} steps
463\end{enumerate}
464
465\bigskip
466\onslide<3->
467Preserves the essential termination property for \alert{measurable} subtraces.
468
469\bigskip
470\onslide<4->
471Due to time pressures, check \alert{soundness} and \alert{precision} of cost
472labels at RTLabs.
473
474\end{frame}
475
476%\begin{frame}[fragile]
477%\frametitle{Structured trace simulation}
478%
479%Lift \alert{local} simulations to \alert{structured trace} simulations
480%similarly.
481%
482%\bigskip
483%\pause
484%\begin{itemize}
485%\item
486%Require local simulations for \alert{normal}, \alert{call} and \alert{return}
487%steps
488%\item allow traces to expand with extra \alert{normal} steps,
489%\item allow us to collapse some \alert{normal} steps
490%  \begin{itemize}
491%  \item but not collapse \blue{labelled} steps
492%  % TODO: why?  avoid larger change in structure
493%  \item or change call structure
494%  \end{itemize}
495%\end{itemize}
496%
497%\bigskip
498%Sufficient to calculate structured trace in target.
499%% TODO: pics
500%
501%\end{frame}
502%
503%\begin{frame}[fragile]
504%\frametitle{Structured trace local simulation example}
505%
506%For function call steps:
507%\begin{center}
508%\includegraphics[width=0.7\linewidth]{strcall.pdf}
509%\end{center}
510%
511%\begin{itemize}
512%\item May add extra steps before and after
513%\item Extra steps must not be call/return
514%\item Must call the same function
515%\item Cost label must stay at start of function
516%\end{itemize}
517%
518%\end{frame}
519
520\subsection{Simulations for compiler passes}
521
522%\frame{
523%\frametitle{TODO: at least two slides on simulations}
524%}
525
526% TODO: perhaps much earlier for the pre-measurable bits?
527\frame{
528\frametitle{Simulation between input and annotated code}
529
530Two stages provide the annotated version of input:
531
532\bigskip
533Switch removal
534\begin{itemize}
535\item \lstinline[language=C]'switch' statement control flow too subtle
536  for simple labelling
537\item Replaces with \lstinline[language=C]'if ... then ... else' tree
538\item Tricky part of proof memory extension for extra variable
539\item Partial proof: validate approach, but not relevant to
540  intensional properties
541\end{itemize}
542
543\bigskip
544Cost labelling
545\begin{itemize}
546\item For simulation don't care \emph{which} labels are added
547\item Just have to skip over extra cost label expressions and
548  statements
549\item Complete simulation proof, simple
550\end{itemize}
551
552% TODO: consider whether to mention full simulation
553% termination-preserving proof?
554}
555
556\frame{
557\frametitle{Front-end simulation results}
558Cast simplification
559\begin{itemize}
560\item Simplify expressions for 8-bit target
561\item Only expressions change --- statements are in lock-step
562\item Difficult part: we allow ill-typed \textbf{Clight} at this stage
563\item Simulation proofs complete
564\end{itemize}
565
566\textbf{Clight} to \textbf{Cminor}
567\begin{itemize}
568\item Stack allocation and control flow transformation
569\item Similar to \textbf{CompCert}, but produces \lstinline'goto'
570  instead of \lstinline'loop'
571\item Expressions complete
572\item Prove a selection of statements, in particular \lstinline'while'
573\item Tricky: Large proof terms for invariant embedded in
574  \textbf{Cminor} programs using dependent types;\\
575  generalise them away, but difficult under binders
576%TODO explain clearly
577\end{itemize}
578}
579\frame{
580\frametitle{Front-end simulation results}
581\textbf{Cminor} to \textbf{RTLabs}
582\begin{itemize}
583\item Construction of control-flow graph
584\item Axiomatized simulations
585\item But do have invariants:
586  \begin{itemize}
587  \item Statement well-typed with respect to pseudo-register
588    environment
589  \item CFG complete
590  \item Entry and exit nodes complete, unique
591  \end{itemize}
592\item Translation function is \emph{total} as a result
593\end{itemize}
594}
595
596% TODO: sloganize: proved more about unusual bits
597
598\section{Checking cost labelling properties}
599
600\frame{
601\frametitle{Checking cost labelling properties}
602
603Check cost labelling is \red{sound} and \blue{precise} at
604\textbf{RTLabs}.
605\begin{itemize}
606\item Shortcut; similar to translation validation
607\end{itemize}
608
609\medskip
610At \textbf{RTLabs} properties become
611\begin{description}
612\item[\red{soundness}] bound on number of instructions in CFG until label\\
613label at start of every function
614\item[\blue{precision}]  label after every branch
615\end{description}
616
617\medskip
618Bound is the hard part; the rest is a simple syntactic check.
619}
620
621\begin{frame}[fragile]
622\frametitle{Bound on number of instructions until label}
623
624\begin{center}
625\includegraphics<1>[width=.4\linewidth]{loop.pdf}
626\includegraphics<2>[width=.4\linewidth]{loop1.pdf}
627\includegraphics<3>[width=.4\linewidth]{loop2.pdf}
628\includegraphics<4>[width=.4\linewidth]{loop3.pdf}
629\includegraphics<5>[width=.4\linewidth]{loop4.pdf}
630\includegraphics<6>[width=.4\linewidth]{loopx.pdf}
631\end{center}
632
633\begin{itemize}
634\item Pick an arbitrary node in the CFG
635\item<2-> Follow successor instructions
636\item<4-> If we find a \alert{cost label} all the traced nodes have a bound\dots
637\item<5-> \dots so remove them and pick a new node, continue
638\item<6-> But if we find an \alert{unlabelled loop} the labelling is unsound,
639  report an error
640\end{itemize}
641
642\end{frame}
643
644\frame{
645\frametitle{Checking cost labelling properties}
646
647This compile-time check is
648\begin{itemize}
649\item[$-$] partial
650\item[$-$] extra work in compilation
651\item[$\mp$] not proving anything about compilation passes
652\item[$+$] less proof burden
653\end{itemize}
654
655\bigskip
656Constructing the bound between \textbf{Cminor} and \textbf{RTLabs}
657likely to be at least as expensive as this check.
658
659}
660
661\section{Construction of structured traces}
662
663\frame{
664\frametitle{Construction of structured traces}
665\begin{center}
666\includegraphics{strtraces.pdf}
667\end{center}
668\begin{enumerate}
669\item Extend sound and precise labelling to semantic states
670\item Prove they are preserved by steps of semantics
671\item Prove \textbf{RTLabs} semantics preserve the stack
672\item Use \alert{termination} proof from \alert{measurable} subtrace
673  to create structure
674\item Proof obligations for cost labelling are discharged by semantic
675  results above
676\end{enumerate}
677}
678
679\section{Whole compiler}
680
681\begin{frame}[fragile]
682\frametitle{Putting the proof together}
683
684\begin{center}
685\includegraphics[width=0.8\linewidth]{compiler.pdf}
686\end{center}
687
688\begin{itemize}
689\item `Clock' difference in Clight is sum of cost labels
690\item Trace of labels is preserved to ASM
691\item Labelling at bottom level is sound and precise
692\item Sum of labels at ASM is equal to difference in real clock
693\end{itemize}
694
695Also preserve observables.
696
697\end{frame}
698
699\frame{
700\frametitle{Conclusion}
701
702Sketched proof for formalised CerCo compiler
703
704\begin{itemize}
705\item Preserving trace structure provides correctness in more challenging
706  setting
707\item Finishing off formal proof
708  \begin{itemize}
709  \item axioms for some regular simulation results
710  \item concentrating on intensional proofs
711  \end{itemize}
712\item[$\star$] Don't need huge changes to extensional proof techniques
713\end{itemize}
714
715\pause
716Future:
717\begin{itemize}
718\item Expect results to generalise to more general labelling schemes
719  \begin{itemize}
720  \item hence more sophisticated targets
721  \end{itemize}
722\item Other compiler correctness techniques
723  \begin{itemize}
724  \item Decompilation?
725  \end{itemize}
726\end{itemize}
727
728}
729
730\end{document}
731
732% LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM
733% LocalWords:  reexecutes subtrace RTLabs subtraces
Note: See TracBrowser for help on using the repository browser.