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

Last change on this file since 3267 was 3267, checked in by campbell, 7 years ago

Improve a few awkward parts of front-end slides.

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