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

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

Minor tweak.

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