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 | |
---|
40 | The \emph{Matita} proof assistant supports writing and verification of |
---|
41 | functional programs. |
---|
42 | |
---|
43 | \bigskip |
---|
44 | |
---|
45 | We |
---|
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 | Talk 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 |
---|
58 | Informed 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 |
---|
81 | Functional correctness for similar compilers already studied in |
---|
82 | Leroy et al.'s \blue{CompCert}. |
---|
83 | |
---|
84 | \bigskip |
---|
85 | Concentrate 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} |
---|
114 | Instrumentation updates global cost variable; suitable for further analysis and |
---|
115 | verification. |
---|
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}}] |
---|
125 | char 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 | |
---|
172 | From 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}}] |
---|
217 | int 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}}] |
---|
235 | call f |
---|
236 | _cost1 |
---|
237 | init y |
---|
238 | _cost2 |
---|
239 | call g |
---|
240 | ... |
---|
241 | return g |
---|
242 | assign y |
---|
243 | decrement x |
---|
244 | test x |
---|
245 | _cost2 |
---|
246 | ... |
---|
247 | _cost3 |
---|
248 | return 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}}] |
---|
257 | call f |
---|
258 | _cost1 |
---|
259 | |
---|
260 | _cost2 |
---|
261 | call g |
---|
262 | ... |
---|
263 | return g |
---|
264 | |
---|
265 | |
---|
266 | |
---|
267 | _cost2 |
---|
268 | ... |
---|
269 | _cost3 |
---|
270 | return 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 | |
---|
304 | Two 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 | |
---|
334 | Total 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> |
---|
365 | Construct by folding up \alert{measurable} subtrace, using soundness |
---|
366 | and 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> |
---|
381 | Switch at RTLabs: |
---|
382 | \begin{itemize} |
---|
383 | \item from \red{measurable} subtrace of \alert{sound} and \alert{precise} |
---|
384 | labelling |
---|
385 | \item to \blue{structured trace} where they are embedded |
---|
386 | \end{itemize} |
---|
387 | |
---|
388 | \onslide<3> |
---|
389 | Changes \blue{syntactic} properties of labelling into \blue{semantic} |
---|
390 | properties. |
---|
391 | |
---|
392 | \onslide<4> |
---|
393 | Reason 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 | |
---|
401 | There is a \alert{measurable} RTLabs subtrace \alert{equivalent} to any |
---|
402 | \alert{measurable} Clight subtrace. |
---|
403 | |
---|
404 | \bigskip |
---|
405 | |
---|
406 | \onslide<2-> |
---|
407 | Split 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-> |
---|
417 | Preserves the essential termination property for \alert{measurable} subtraces. |
---|
418 | |
---|
419 | \bigskip |
---|
420 | \onslide<4-> |
---|
421 | Due to time pressures, check \alert{soundness} and \alert{precision} of cost |
---|
422 | labels at RTLabs. |
---|
423 | |
---|
424 | \end{frame} |
---|
425 | |
---|
426 | \begin{frame}[fragile] |
---|
427 | \frametitle{Structured trace simulation} |
---|
428 | |
---|
429 | Lift \alert{local} simulations to \alert{structured trace} simulations |
---|
430 | similarly. |
---|
431 | |
---|
432 | \bigskip |
---|
433 | \pause |
---|
434 | \begin{itemize} |
---|
435 | \item |
---|
436 | Require local simulations for \alert{normal}, \alert{call} and \alert{return} |
---|
437 | steps |
---|
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 |
---|
448 | Sufficient 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 | |
---|
456 | For 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 | |
---|
485 | Also preserve observables. |
---|
486 | |
---|
487 | \end{frame} |
---|
488 | |
---|
489 | \frame{ |
---|
490 | \frametitle{Conclusion} |
---|
491 | |
---|
492 | Sketched 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 |
---|
506 | Future: |
---|
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 Translation validation? |
---|
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 |
---|