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

Last change on this file was 3277, checked in by Ian Stark, 7 years ago

Renaming and moving

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