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

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

Tweak talk a little.

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