source: Deliverables/Dissemination/front-end/final-review/front-end.tex @ 3278

Last change on this file since 3278 was 3278, 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: 23.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{WP3: Verified Compiler --- Front End\\[1\jot]
29D3.4: Front-End Correctness Proofs}
30\author{Brian~Campbell, Ilias~Garnier, James~McKinna, \underline{Ian~Stark}}
31\institute{LFCS, University of Edinburgh\\[1ex]
32\includegraphics[width=.3\linewidth]{cerco_logo.png}\\
33\footnotesize Project FP7-ICT-2009-C-243881
34}
35\date{CerCo review meeting\\16th May 2013}
36\maketitle
37
38
39\begin{frame}{CerCo Outcomes}
40
41  The final results of the CerCo project include the following:
42
43  \medskip %
44  \begin{itemize}
45  \item A compiler from C to executable 8051 binaries, formalised in Matita as
46    \blue{\lstinline|compiler.ma|} \dots
47  \item \dots which adds labels and cost information to C source code
48  \item \dots with exact values for time and space used by the binary.
49
50    \medskip %
51  \item A machine-checked proof of this in Matita
52    \blue{\lstinline|correctness.ma|}:
53
54    \smallskip %
55    \begin{itemize}
56    \item Addressing \red{intensional} properties --- clock cycles, stack bytes
57
58      \smallskip %
59    \item As well as \red{extensional} properties --- functional correctness.
60    \end{itemize}
61  \item An executable cost-annotating compiler \blue{\lstinline|cerco|}
62    extracted from the formalisation.
63  \end{itemize}
64
65  \medskip %
66  This talk treats the front-end compiler and proof, describing the technical
67  challenges and contributions from the work in Period~3.
68 
69\end{frame}
70
71\begin{frame}{Compiler}
72
73  The CerCo compiler, given C source code, will generate:
74  \begin{itemize}
75  \item Labelled Clight source code;
76  \item Labelled 8051 object code;
77  \item Cost maps: for each label a count of time (clock cycles) and space
78    (stack bytes) usage.
79  \end{itemize}
80
81  \medskip %
82  The compiler operates in multiple passes, with each intermediate language
83  having an executable semantics in Matita: %
84  \vspace*{-\medskipamount}
85  \begin{center}
86    \includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
87  \end{center}
88  \vspace*{-\medskipamount}
89
90\end{frame}
91
92\begin{frame}{Correctness}
93 
94  Suppose we have C source with labelled Clight, labelled 8051 binary, and
95  cost maps all generated from the CerCo compiler.
96
97  \medskip %
98  Then the Matita theorem for correctness is that:
99  \begin{itemize}
100  \item Executing the original and labelled Clight source gives the same
101    behaviour;
102  \item Executing the 8051 binary gives the same observables: labels and
103    call/return;
104  \item Applying the cost maps to the trace of C labels correctly
105    describes the time and space usage of the 8051 execution.
106  \end{itemize}
107
108  In fact we give an exact result on all \red{measurable subtraces}: from any
109  label to the end of its enclosing function.
110
111  \medskip %
112  The machine-checked proof is the concatenation of correctness results for
113  the front end, the back end, and the assembler.
114
115\end{frame}
116
117\begin{frame}{Front-End Progress}
118 
119  \vspace*{-\bigskipamount}
120  \begin{center}
121    \includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
122  \end{center}
123  \vspace*{-\medskipamount}
124
125  At the start of Period~3 the front end included in Matita:
126  \begin{itemize}
127  \item Executable semantics for source and intermediate languages;
128  \item Labelling and compilation of source through these;
129  \item Innovation of \red{structured traces}, originally to support timing
130    computation in the assembler.
131  \end{itemize}
132
133  At the completion of Period~3, the front end included proofs of correctness
134  for all these, extension to stack usage, and considerable refinement of the
135  existing formal development.
136 
137\end{frame}
138
139\begin{frame}{Front-End Contribution}
140
141  Notable features and original elements of the front-end include:
142  \begin{itemize}
143  \item Proof layering:
144    \begin{itemize}
145    \item A \blue{functional correctness proof};
146    \item A \blue{cost proof}, separate but depending on functional
147      correctness.
148    \end{itemize}
149  \item \blue{Internal checks} as a proof shortcut, like translation
150    validation.
151  \item \blue{Structured traces} for holding detailed data on resource
152    behaviour, not just for assembler cost calculation.
153  \item Introduction of \blue{measurable subtraces} as a unit of cost
154    proof.
155  \end{itemize}
156  These features are significant in particular because:
157  \begin{itemize}
158  \item Compilation is not 1-1 transliteration: code is rearranged and
159    modified, but label sequencing is preserved;
160  \item The source language has implicit control flow constraints not present
161    in the target (call/return, branches, loops).
162  \end{itemize}
163
164\end{frame}
165
166\begin{frame}{Axiomatization}
167
168  The translation in \blue{\lstinline|compile.ma|} is complete --- essential
169  for extracting a compiler.
170
171  \medskip %
172  The simulation results in \blue{\lstinline|correctness.ma|} are fully
173  specified, and with substantially complete proofs.  Some parts, however,
174  have been axiomatized and their correctness assumed.
175
176  \medskip %
177  In the front-end there are two sources of this axiomatisation:
178  \begin{itemize}
179  \item \red{Functional correctness.}  Other projects, notably
180    \blue{CompCert}, provide assurances that such proofs can be completed; so
181    certain parts of this proof have been assumed.
182  \item Simulation steps with \red{many cases}, sometimes similar; here we
183    have identified representative and more challenging cases for detailed
184    proof.
185  \end{itemize}
186 
187\end{frame}
188
189\begin{frame}[fragile]
190\frametitle{Structure of the Proof}
191
192\begin{center}
193\includegraphics[width=0.7\linewidth]{compiler.pdf}
194\end{center}
195
196The transition from front-end to back-end marks the change:
197\begin{itemize}
198\item From a language with explicit call/return structure and high-level
199  control flow;
200\item To a language with explicit addresses and control-flow graph.
201\end{itemize}
202
203Correspondingly, the proof hands over
204\begin{itemize}
205\item From measurable subtraces with labelling that must be checked
206  \blue{sound} and \blue{precise};
207\item To \blue{structured traces} which embed these invariants.
208\end{itemize}
209
210\end{frame}
211
212
213% \frame{
214% \frametitle{Introduction}
215
216% D3.4 is the front-end correctness proofs:
217
218% \begin{description}
219% \item[Primary focus:] novel \red{intensional} properties: \blue{cost
220%     bound correctness}
221% \item[Secondary:] usual \red{extensional} result: \blue{functional correctness}
222% \end{description}
223
224% Functional correctness for similar compilers already studied in
225% Leroy et al.'s \blue{CompCert}.
226% \begin{itemize}
227% \item Axiomatize similar results
228% \end{itemize}
229
230% \medskip
231% Now have \blue{stack} costs as well as \blue{time}
232% \begin{itemize}
233% \item yields stronger overall correctness result
234% \end{itemize}
235
236% \medskip
237% \alert{Extract} compiler code from development for practical execution.
238
239% \medskip
240% Informed by earlier formal experiment with a toy compiler.
241% }
242
243% TODO: could reuse some of this to make stronger intro?
244% \frame{
245% \frametitle{Motivation for formalisation}
246
247% \begin{enumerate}
248% \item Provide \alert{assurance} about labelling approach
249%   \begin{itemize}
250%   \item more complex setting than toy compiler
251%   \end{itemize}
252% \item demonstrate feasibility of \alert{certified} WCET toolchain
253% % Future: proof translating compiler to provide checkable WCET certificate?
254% \item new experiments with certified compilation:
255%   \begin{itemize}
256%   \item deeper use of \alert{dependent types}
257%   \item \alert{executable} semantics in type theory
258%   \item certification of \alert{optimising assembler}
259%   \end{itemize}
260% \end{enumerate}
261
262% \bigskip
263% \pause
264
265% \bigskip
266% Concentrate on cost correctness.
267% \begin{itemize}
268% \item Keep \alert{extensional} proofs as separate as possible
269% \end{itemize}
270% }
271
272% \frame{
273% \frametitle{Outline}
274% \tableofcontents
275% }
276
277% \section{CerCo Compiler}
278
279% \frame{
280% \frametitle{CerCo compiler}
281
282% \begin{center}
283% \includegraphics[width=0.8\linewidth]{compiler-plain.pdf}
284% \end{center}
285
286% \begin{itemize}
287% \item Reuse unverified CompCert parser
288% %\item Transform away troublesome constructs
289% %  \begin{itemize}
290% %  \item e.g.~\texttt{switch}
291% %  \item fallthrough requires slightly more sophisticated labelling
292% %  \item but not fundamentally different
293% %  \end{itemize}
294% \item Intermediate language for most passes
295% \item Executable semantics for each
296% \item Outputs
297%   \begin{itemize}
298%   \item 8051 machine code
299%   \item Clight code instrumented with costs in 8051 clock cycles and
300%     bytes of stack space
301%   \end{itemize}
302% \end{itemize}
303% Instrumentation updates global cost variable; suitable for further analysis and
304% verification.
305% }
306
307% \section{Overall correctness}
308
309% \begin{frame}[fragile]
310% \frametitle{Correctness of labelling approach}
311
312% \begin{tabular}{ccc}
313
314% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
315%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
316% char f(char x) {
317%   char y;
318%   _cost3:
319%   if (x>10) {
320%     _cost1:
321%     y = g(x);
322%   } else {
323%     _cost2:
324%     y = 5;
325%   }
326%   return y+1;
327% }
328% \end{lstlisting}
329
330% &
331
332% \begin{minipage}{9em}
333% \begin{center}
334% $\Rightarrow$\\[4ex]
335% \blue{soundness}\\[2ex]
336% \red{precision}
337% \end{center}
338% \end{minipage}
339
340% &
341
342% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
343%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
344%   "f"
345%     emit _cost3
346%     *** Prologue ***
347%     move A, R06
348%     clear CARRY
349%     ...
350%     branch A <> 0, f10
351%     emit _cost2
352%     imm R00, 5
353%     ...
354%     f10:
355%     emit _cost1
356%     call "g"
357%     ...
358% \end{lstlisting}
359
360
361% \end{tabular}
362
363% From experiments with toy compiler [D2.1, FMICS'12]:
364% \begin{enumerate}
365% \item Functional correctness, \emph{including trace of labels}
366% %\item Source labelling function is sound and precise
367% %\item Preservation of soundness and precision of labelling
368% \item Target labelling function is sound and precise
369% % TODO: detail about soundness and precision?
370% \item Target cost analysis produces a map of labels to times
371%   \begin{itemize}
372%   \item Accurate for sound and precise labellings
373%   \end{itemize}
374% %\item Correctness of instrumentation
375% \end{enumerate}
376
377% \end{frame}
378
379% %\frame{
380% %\frametitle{}
381% %
382% %Due to resource constraints
383% %\begin{itemize}
384% %\item Instrumentation is done in language semantics
385% %\item Soundness and precision of labelling is checked during compilation
386% %  \begin{itemize}
387% %  \item c.f.~translation validation
388% %  \end{itemize}
389% %\item Focusing effort on novel parts --- cost proofs over functional correctness
390% %\end{itemize}
391% %
392% %}
393
394% \begin{frame}[fragile]
395% \frametitle{Overall correctness statement}
396
397% \begin{center}
398% \fbox{\( \text{machine time} =  \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)}
399% \end{center}
400
401% \pause
402
403% \begin{center}
404% \begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c}
405
406% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
407%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
408% int f(int x) {
409%   _cost1:
410%   int y = 0;
411%   while (x) {
412%     _cost2:
413%     y = g(y);
414%     x = x - 1;
415%   }
416%   _cost3:
417%   return y;
418% }
419% \end{lstlisting}
420
421% &
422
423% \begin{uncoverenv}<2-3>
424% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
425%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
426% call f
427% _cost1
428% init y
429% _cost2
430% call g
431% ...
432% return g
433% assign y
434% decrement x
435% test x
436% _cost2
437% ...
438% _cost3
439% return f
440% \end{lstlisting}
441% \end{uncoverenv}
442
443% &
444
445% \begin{uncoverenv}<3-5>
446% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
447%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
448% call f
449% _cost1
450
451% _cost2
452% call g
453% ...
454% return g
455
456
457
458% _cost2
459% ...
460% _cost3
461% return f
462% \end{lstlisting}
463% \end{uncoverenv}
464
465% \end{tabular}
466% \end{center}
467
468% \begin{overprint}
469% \onslide<2>
470% \begin{itemize}
471% \item Use labels and end of function as measurement points
472% \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f'
473% \end{itemize}
474
475% \onslide<3-4>
476% \begin{itemize}
477% \item Use labels and end of function as measurement points
478% \item All costs are considered local to the function
479% \item Actual position of unobservable computation is unimportant
480% \end{itemize}
481
482% \onslide<5>
483% \begin{itemize}
484% \item Use labels and end of function as measurement points
485% \item[$\star$] Call suitable subtraces \alert{measurable}
486% \item[$\star$] Core part is a proof of \alert{termination}
487% \end{itemize}
488% \end{overprint}
489
490% \end{frame}
491
492% \begin{frame}[fragile]
493% \frametitle{Correct cost analysis depends on call structure}
494
495% Two straight-line functions:
496
497% \begin{center}
498% \begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}}
499
500% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
501%                    emph={[2]_cost3},emphstyle={[2]\color{blue}}]
502% "f"
503%   emit _cost1
504%   ...
505%   call "g"
506%   ...
507%   return
508% \end{lstlisting}
509
510% &
511
512% \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
513%                    emph={[2]_cost3},emphstyle={[2]\color{blue}},
514%                    escapechar=\%]
515% "g"
516%   emit _cost2
517%   ...
518%   %\only<2->{\blue{increase return address}}%
519%   return
520% \end{lstlisting}
521
522% \end{tabular}
523% \end{center}
524
525% Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}).
526
527% \begin{itemize}
528% \item<2-> Changing return address skips code from \lstinline'f'
529% \item<2-> Cost no longer equals sum of cost labels
530% \end{itemize}
531
532% \onslide<2->
533% \alert{Need to observe correct call/return structure.}
534
535% \onslide<3>
536% \emph{Not easy at ASM --- observe earlier in compiler \& maintain.}
537
538% \end{frame}
539
540% \section{Front-end correctness}
541
542% \frame{
543% \frametitle{Front-end correctness}
544
545% Recalling the toy compiler, need
546% \begin{enumerate}
547% \item Functional correctness
548% \item Cost labelling sound and precise
549% \item\label{it:return} To demonstrate return addresses are correct
550% \end{enumerate}
551% % TODO: stack space?  from obs, from fnl correctness
552
553% \bigskip
554% For~\ref{it:return} we generalise notion of \emph{structured traces}
555% originally introduced for the correctness of timing analysis.
556% }
557
558\begin{frame}[fragile]
559\frametitle{Structured traces}
560
561Embed call structure and label invariants into execution traces.
562
563\begin{center}
564\includegraphics{strtraces.pdf}
565\end{center}
566
567\begin{itemize}
568\item Enforces \blue{invariants} on positions of cost labels.
569\item \blue{Groups} execution steps according to preceding cost label.
570\item Forbids \blue{repeating} addresses in grouped steps.
571\end{itemize}
572
573Constructed by folding up measurable subtraces, using the fact that labelling
574is sound and precise.
575
576\end{frame}
577
578\begin{frame}{Step-by-Step: Getting to Labelled Source}
579
580\blue{C $\to$ Clight}
581
582\smallskip %
583To translate from C to Clight we reuse the CompCert parser.
584
585\bigskip %
586\blue{Switch Removal}
587
588\smallskip %
589Control flow for \red{\lstinline'switch'} is too subtle for simple labelling;
590we replace with an \red{\lstinline'if .. then .. else'} tree.  Proof requires
591tracking memory extension for an extra test variable.
592
593\bigskip %
594\blue{Cost Labels}
595
596\smallskip %
597Labels added at function start, branch targets, \dots
598
599\smallskip %
600Simulation of execution is exact, just skipping over labels.
601
602\end{frame}
603
604\begin{frame}{Front-End Correctness}
605
606  Suppose we have a \blue{measurable} subtrace of Clight execution, including
607  the \blue{prefix} of that trace from initial state.
608
609  \medskip %
610  Then for handover to the back-end we have in RTLabs:
611  \begin{itemize}
612  \item A corresponding \red{prefix};
613  \item A \red{structured trace} corresponding to the measurable subtrace;
614  \item The required invariants, including \red{no repeating addresses};
615  \item A proof that the same \red{stack limit} is observed.
616  \end{itemize}
617
618  \medskip %
619  In addition, to link this with the source program:
620  \begin{itemize}
621  \item The observables for the RLabs \blue{prefix} and \blue{structured
622      trace} are the same as for their counterparts in Clight.
623  \end{itemize}
624
625\end{frame}
626
627
628% \section{Correctness proofs}
629% \subsection{Generic lifting result}
630
631\begin{frame}[fragile]
632\frametitle{Lifting measurable traces}
633
634For each pass find a target \alert{measurable} subtrace
635\alert{equivalent} to any source \alert{measurable} subtrace.
636
637\bigskip
638
639\onslide<2->
640\begin{center}
641\includegraphics{meassim.pdf}
642\end{center}
643
644Split normal simulation proof:
645\begin{enumerate}
646\item each \blue{call} becomes a \blue{call} step plus zero or
647  more \blue{normal} steps;\\
648  following cost labels should stay next to the call step
649\item each \blue{return} becomes a \blue{return} plus zero or
650  more \blue{normal} steps
651\item \blue{cost} label steps are preserved
652\item other \blue{normal} steps become zero or more \blue{normal} steps
653\end{enumerate}
654
655\bigskip
656\onslide<3->
657Preserves the defining termination property for \alert{measurable} subtraces.
658
659% \bigskip
660% \onslide<4->
661% Due to time pressures, check \alert{soundness} and \alert{precision} of cost
662% labels at RTLabs.
663
664\end{frame}
665
666%\begin{frame}[fragile]
667%\frametitle{Structured trace simulation}
668%
669%Lift \alert{local} simulations to \alert{structured trace} simulations
670%similarly.
671%
672%\bigskip
673%\pause
674%\begin{itemize}
675%\item
676%Require local simulations for \alert{normal}, \alert{call} and \alert{return}
677%steps
678%\item allow traces to expand with extra \alert{normal} steps,
679%\item allow us to collapse some \alert{normal} steps
680%  \begin{itemize}
681%  \item but not collapse \blue{labelled} steps
682%  % TODO: why?  avoid larger change in structure
683%  \item or change call structure
684%  \end{itemize}
685%\end{itemize}
686%
687%\bigskip
688%Sufficient to calculate structured trace in target.
689%% TODO: pics
690%
691%\end{frame}
692%
693%\begin{frame}[fragile]
694%\frametitle{Structured trace local simulation example}
695%
696%For function call steps:
697%\begin{center}
698%\includegraphics[width=0.7\linewidth]{strcall.pdf}
699%\end{center}
700%
701%\begin{itemize}
702%\item May add extra steps before and after
703%\item Extra steps must not be call/return
704%\item Must call the same function
705%\item Cost label must stay at start of function
706%\end{itemize}
707%
708%\end{frame}
709
710% \subsection{Simulations for compiler passes}
711
712%\frame{
713%\frametitle{TODO: at least two slides on simulations}
714%}
715
716% TODO: perhaps much earlier for the pre-measurable bits?
717
718\frame{
719\frametitle{Front-end simulation results}
720Cast simplification
721\begin{itemize}
722\item Simplify expressions for 8-bit target
723\item Only expressions change --- statements are in lock-step
724\item Difficult part: we allow ill-typed \textbf{Clight} at this stage
725\item Simulation proofs complete
726\end{itemize}
727
728\textbf{Clight} to \textbf{Cminor}
729\begin{itemize}
730\item Stack allocation and control flow transformation
731\item Similar to \textbf{CompCert}, but produces \lstinline'goto'
732  instead of \lstinline'loop'
733\item Expressions complete
734\item Prove a selection of statements, in particular \lstinline'while'
735\item Tricky: Large proof terms for invariant embedded in
736  \textbf{Cminor} programs using dependent types;\\
737  generalise them away, but difficult under binders
738%TODO explain clearly
739\end{itemize}
740}
741\frame{
742\frametitle{Front-end simulation results}
743\textbf{Cminor} to \textbf{RTLabs}
744\begin{itemize}
745\item Construction of control-flow graph
746\item Axiomatized simulations
747\item But do have invariants:
748  \begin{itemize}
749  \item Statement well-typed with respect to pseudo-register
750    environment
751  \item CFG complete
752  \item Entry and exit nodes complete, unique
753  \end{itemize}
754\item Translation function is \emph{total} as a result
755\end{itemize}
756}
757
758% TODO: sloganize: proved more about unusual bits
759
760% \section{Checking cost labelling properties}
761
762\frame{
763\frametitle{Checking cost labelling properties}
764
765Check cost labelling is \red{sound} and \blue{precise} at
766\textbf{RTLabs}.
767\begin{itemize}
768\item Shortcut; similar to translation validation
769\end{itemize}
770
771\medskip
772At \textbf{RTLabs} properties become
773\begin{description}
774\item[\red{soundness}] bound on number of instructions in CFG until label\\
775label at start of every function
776\item[\blue{precision}]  label after every branch
777\end{description}
778
779\medskip
780Bound is the hard part; the rest is a simple syntactic check.
781}
782
783\begin{frame}[fragile]
784\frametitle{Bound on number of instructions until label}
785
786\begin{center}
787\includegraphics<1>[width=.4\linewidth]{loop.pdf}
788\includegraphics<2>[width=.4\linewidth]{loop1.pdf}
789\includegraphics<3>[width=.4\linewidth]{loop2.pdf}
790\includegraphics<4>[width=.4\linewidth]{loop3.pdf}
791\includegraphics<5>[width=.4\linewidth]{loop4.pdf}
792\includegraphics<6>[width=.4\linewidth]{loopx.pdf}
793\end{center}
794
795\begin{itemize}
796\item Pick an arbitrary node in the CFG
797\item<2-> Follow successor instructions
798\item<4-> If we find a \alert{cost label} all the traced nodes have a bound\dots
799\item<5-> \dots so remove them and pick a new node, continue
800\item<6-> But if we find an \alert{unlabelled loop} the labelling is unsound,
801  report an error
802\end{itemize}
803
804\end{frame}
805
806\frame{
807\frametitle{Checking cost labelling properties}
808
809This compile-time check is
810\begin{itemize}
811\item[$-$] partial
812\item[$-$] extra work in compilation
813\item[$\mp$] not proving anything about compilation passes
814\item[$+$] less proof burden
815\end{itemize}
816
817\bigskip
818In a full proof would go from
819\begin{quote}
820  cost labels at the head of loops in \textbf{Cminor}
821\end{quote}
822to
823\begin{quote}
824  bound on instructions to cost label in \textbf{RTLabs}
825\end{quote}
826Showing existence of the bound alone likely to require at least as much
827proof effort as this check.
828
829}
830
831% \section{Construction of structured traces}
832
833\frame{
834\frametitle{Construction of structured traces}
835\begin{center}
836\includegraphics{strtraces.pdf}
837\end{center}
838\begin{enumerate}
839\item Extend sound and precise labelling to semantic states
840\item Prove they are preserved by steps of semantics
841\item Prove \textbf{RTLabs} semantics preserve the stack
842\item Use \alert{termination} proof from \alert{measurable} subtrace
843  to create structure
844\item Proof obligations for cost labelling are discharged by semantic
845  results above
846\end{enumerate}
847}
848
849% \section{Whole compiler}
850
851\begin{frame}[fragile]
852\frametitle{Putting the proof together}
853
854\begin{center}
855\includegraphics[width=0.8\linewidth]{compiler.pdf}
856\end{center}
857
858\begin{itemize}
859\item `Clock' difference in Clight is sum of cost labels
860\item Observables, including trace of labels, is preserved to ASM
861\item Labelling at bottom level is sound and precise
862\item Sum of labels at ASM is equal to difference in real clock
863\end{itemize}
864
865\end{frame}
866
867\frame{
868\frametitle{Conclusion}
869
870Sketched proof for formalised CerCo front-end
871
872\begin{itemize}
873\item Intensional proofs can be layered on top of extensional results
874\item Preserving call-structure key ingredient
875\item Compile-time cost labelling checks can reduce proof burden
876\item[$\star$] Don't need huge changes to extensional proof techniques
877\end{itemize}
878
879\pause
880Future:
881\begin{itemize}
882\item Expect results to generalise to more general labelling schemes
883  \begin{itemize}
884  \item hence more sophisticated targets
885  \end{itemize}
886\item Other compiler correctness techniques
887  \begin{itemize}
888  \item Decompilation?
889  \end{itemize}
890\end{itemize}
891
892}
893
894\end{document}
895
896% LocalWords:  LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM
897% LocalWords:  reexecutes subtrace RTLabs subtraces
Note: See TracBrowser for help on using the repository browser.