source: Deliverables/Dissemination/proof-structured-traces/proof-structured-traces.tex @ 2585

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

Many improvements to proof/structured traces talk.

File size: 10.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{A certified proof based on structured traces}
29\author{Brian Campbell}
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{23rd January 2013}
35\maketitle
36
37\frame{
38\frametitle{Introduction}
39
40The \emph{Matita} proof assistant supports writing and verified functional
41programs.
42
43\bigskip
44
45We
46
47\begin{itemize}
48\item formalise the CerCo compiler in Matita,
49\item prove usual \red{extensional} result: \blue{functional correctness}
50\item also prove \red{intensional} properties: \blue{cost bound correctness}
51\end{itemize}
52
53\bigskip
54\alert{Extract} compiler code from development for practical execution.
55
56\bigskip
57Informed by earlier formal experiment with a toy compiler.
58}
59
60\frame{
61\frametitle{Motivation for formalisation}
62
63\begin{enumerate}
64\item Provide \alert{assurance} about labelling approach
65  \begin{itemize}
66  \item more complex setting than toy compiler
67  \end{itemize}
68\item demonstrate feasibility of \alert{certified} WCET toolchain
69% Future: proof translating compiler to provide checkable WCET certificate?
70\item new experiments with certified compilation:
71  \begin{itemize}
72  \item deeper use of \alert{dependent types}
73  \item \alert{executable} semantics in type theory
74  \item certification of \alert{optimising assembler}
75  \end{itemize}
76\end{enumerate}
77
78\bigskip
79\pause
80Functional correctness for similar compilers already studied in
81Leroy et al.'s \blue{CompCert}.
82
83Concentrate on cost correctness.
84}
85
86\frame{
87\frametitle{CerCo compiler}
88
89\begin{center}
90\includegraphics[width=0.7\linewidth]{compiler-plain.pdf}
91\end{center}
92
93\begin{itemize}
94\item Reuse unverified CompCert parser
95%\item Transform away troublesome constructs
96%  \begin{itemize}
97%  \item e.g.~\texttt{switch}
98%  \item fallthrough requires slightly more sophisticated labelling
99%  \item but not fundamentally different
100%  \end{itemize}
101\item Intermediate language for most passes
102\item Executable semantics for each
103\item Outputs
104  \begin{itemize}
105  \item 8051 machine code
106  \item Clight code annotated with \alert{cost labels}
107  \item \alert{Cost map} of cost labels to 8051 clock cycles
108  \end{itemize}
109\end{itemize}
110}
111
112\begin{frame}[fragile]
113\frametitle{Correctness of labelling approach}
114
115\begin{tabular}{ccc}
116
117\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
118                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
119char f(char x) {
120  char y;
121  _cost3:
122  if (x>10) {
123    _cost1:
124    y = g(x);
125  } else {
126    _cost2:
127    y = 5;
128  }
129  return y+1;
130}
131\end{lstlisting}
132
133&
134
135\begin{minipage}{9em}
136\begin{center}
137$\Rightarrow$\\[4ex]
138\blue{soundness}\\[2ex]
139\red{precision}
140\end{center}
141\end{minipage}
142
143&
144
145\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
146                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
147  "f"
148    emit _cost3
149    *** Prologue ***
150    move A, R06
151    clear CARRY
152    ...
153    branch A <> 0, f10
154    emit _cost2
155    imm R00, 5
156    ...
157    f10:
158    emit _cost1
159    call "g"
160    ...
161\end{lstlisting}
162
163
164\end{tabular}
165
166From experiments with toy compiler:
167\begin{enumerate}
168\item Functional correctness, \emph{including trace of labels}
169%\item Source labelling function is sound and precise
170%\item Preservation of soundness and precision of labelling
171\item Target labelling function is sound and precise
172% TODO: detail about soundness and precision?
173\item Target cost analysis produces a map of labels to times
174  \begin{itemize}
175  \item Accurate for sound and precise labellings
176  \end{itemize}
177%\item Correctness of instrumentation
178\end{enumerate}
179
180\end{frame}
181
182%\frame{
183%\frametitle{}
184%
185%Due to resource constraints
186%\begin{itemize}
187%\item Instrumentation is done in language semantics
188%\item Soundness and precision of labelling is checked during compilation
189%  \begin{itemize}
190%  \item c.f.~translation validation
191%  \end{itemize}
192%\item Focusing effort on novel parts --- cost proofs over functional correctness
193%\end{itemize}
194%
195%}
196
197\begin{frame}[fragile]
198\frametitle{Goal}
199
200\begin{center}
201\fbox{\( \text{machine time} =  \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)}
202\end{center}
203
204\pause
205
206\begin{center}
207\begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c}
208
209\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
210                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
211int f(int x) {
212  _cost1:
213  int y = 0;
214  while (x) {
215    _cost2:
216    y = g(y);
217    x = x - 1;
218  }
219  _cost3:
220  return y;
221}
222\end{lstlisting}
223
224&
225
226\begin{uncoverenv}<2-3>
227\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
228                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
229call f
230_cost1
231init y
232_cost2
233call g
234...
235return g
236assign y
237decrement x
238test x
239_cost2
240...
241_cost3
242return f
243\end{lstlisting}
244\end{uncoverenv}
245
246&
247
248\begin{uncoverenv}<3-4>
249\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
250                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
251call f
252_cost1
253
254_cost2
255call g
256...
257return g
258
259
260
261_cost2
262...
263_cost3
264return f
265\end{lstlisting}
266\end{uncoverenv}
267
268\end{tabular}
269\end{center}
270
271\begin{overprint}
272\onslide<2>
273\begin{itemize}
274\item Use labels and end of function as measurement points
275\item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of whole function
276\end{itemize}
277
278\onslide<3>
279\begin{itemize}
280\item Use labels and end of function as measurement points
281\item Actual position of unobservable computation is unimportant
282\item All costs are considered local to the function
283\end{itemize}
284
285\onslide<4>
286\begin{itemize}
287\item Use labels and end of function as measurement points
288\item[$\star$] Call suitable subtraces \alert{measurable}
289\item[$\star$] Core part is a proof of \alert{termination}
290\end{itemize}
291\end{overprint}
292
293\end{frame}
294
295\begin{frame}[fragile]
296\frametitle{Correct cost analysis depends on call structure}
297
298Two straight-line functions:
299
300\begin{center}
301\begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}}
302
303\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
304                   emph={[2]_cost3},emphstyle={[2]\color{blue}}]
305"f"
306  emit _cost1
307  ...
308  call "g"
309  ...
310  return
311\end{lstlisting}
312
313&
314
315\begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf},
316                   emph={[2]_cost3},emphstyle={[2]\color{blue}},
317                   escapechar=\%]
318"g"
319  emit _cost2
320  ...
321  %\only<2->{\blue{reduce return address}}%
322  return
323\end{lstlisting}
324
325\end{tabular}
326\end{center}
327
328Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}).
329
330\begin{itemize}
331\item<2-> Changing return address reexecutes code from \lstinline'f'
332\item<2-> Cost no longer equals sum of cost labels
333\end{itemize}
334
335\onslide<2->
336Need to enforce correct call/return structure.
337
338\onslide<3>
339\emph{Not easy to observe at ASM.}
340
341\end{frame}
342
343\begin{frame}[fragile]
344\frametitle{Structured traces}
345
346\alert{Embed} the call/return structure into execution traces.
347
348\begin{center}
349\includegraphics{strtraces.pdf}
350\end{center}
351
352\begin{itemize}
353\item Traces of \alert{called functions} are nested
354\item Invariants on positions of cost labels enforced
355\item Steps are \alert{grouped} according to cost label
356\end{itemize}
357
358\onslide<2>
359Construct by folding up \alert{measurable} subtrace, using soundness
360and preciseness of labelling.
361
362\end{frame}
363
364\begin{frame}[fragile]
365\frametitle{Structure in the compiler proof}
366
367\begin{center}
368\includegraphics[width=0.7\linewidth]{compiler.pdf}
369\end{center}
370
371\onslide<1>
372\green{Assembler} provides part of local cost analysis (CPP'12).
373
374\onslide<2-4>
375Switch at RTLabs:
376\begin{itemize}
377\item from \red{measurable} subtrace of \alert{sound} and \alert{precise}
378labelling
379\item to \blue{structured trace} where they are embedded
380\end{itemize}
381
382\onslide<3>
383Changes \blue{syntactic} properties of labelling into \blue{semantic}
384properties.
385
386\onslide<4>
387Reason for choice: first language with explicit \alert{addresses}, implicit
388\alert{call handling}.
389
390\end{frame}
391
392\begin{frame}[fragile]
393\frametitle{Front-end measurable traces (Clight to RTLabs)}
394
395There is a \alert{measurable} RTLabs subtrace \alert{equivalent} to any
396\alert{measurable} Clight subtrace.
397
398\bigskip
399
400\onslide<2->
401Split normal simulation proof into three:
402\begin{enumerate}
403\item \blue{normal} steps become zero or more \blue{normal} steps
404\item \blue{call/return} steps become a \blue{call/return} step plus zero or
405  more \blue{normal} steps
406\item \blue{cost} steps are preserved
407\end{enumerate}
408
409\bigskip
410\onslide<3->
411Preserves the essential termination property for \alert{measurable} subtraces.
412
413\bigskip
414\onslide<4->
415Due to time pressures, check \alert{soundness} and \alert{precision} of cost
416labels at RTLabs.
417
418\end{frame}
419
420\begin{frame}[fragile]
421\frametitle{Structured trace simulation}
422
423Lift \alert{local} simulations to \alert{structured trace} simulations
424similarly.
425
426\bigskip
427\pause
428\begin{itemize}
429\item
430Require local simulations for \alert{normal}, \alert{call} and \alert{return}
431steps
432\item allow traces to expand with extra \alert{normal} steps,
433\item allow us to collapse some \alert{normal} steps
434  \begin{itemize}
435  \item but not collapse \blue{labelled} steps
436  % TODO: why?  avoid larger change in structure
437  \item or change call structure
438  \end{itemize}
439\end{itemize}
440
441\bigskip
442Sufficient to calculate structured trace in target.
443% TODO: pics
444
445\end{frame}
446
447\begin{frame}[fragile]
448\frametitle{Putting the proof together}
449
450\begin{center}
451\includegraphics[width=0.7\linewidth]{compiler.pdf}
452\end{center}
453
454\begin{itemize}
455\item `Clock' difference in Clight is sum of cost labels
456\item Trace of labels is preserved to ASM
457\item Labelling at bottom level is sound and precise
458\item Sum of labels at ASM is equal to difference in real clock
459\end{itemize}
460
461Also preserve observables.
462
463\end{frame}
464
465\frame{
466\frametitle{Conclusion}
467
468Sketched proof for formalised CerCo compiler
469
470\bigskip
471\begin{itemize}
472\item Preserving trace structure provides correctness in more challenging
473  setting
474\item Formal proof still in progress
475  \begin{itemize}
476  \item key definitions, structured trace lifting, some simulations done
477  \item increasing confidence in approach
478  \end{itemize}
479\item Expect results to generalise to more general labelling schemes
480  \begin{itemize}
481  \item hence more sophisticated targets
482  \end{itemize}
483\end{itemize}
484
485}
486
487\end{document}
488
489% LocalWords:  LFCS Matita CerCo intensional
Note: See TracBrowser for help on using the repository browser.