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

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

Structured traces talk with most of the content; not quite final.

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