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{WP3: Verified Compiler --- Front End\\[1\jot] |
---|
29 | D3.4: Front-End Correctness Proofs} |
---|
30 | \author{Brian~Campbell, Ilias~Garnier, James~McKinna, \underline{Ian~Stark}} |
---|
31 | \institute{LFCS, University of Edinburgh\\[1ex] |
---|
32 | \includegraphics[width=.3\linewidth]{cerco_logo.png}\\ |
---|
33 | \footnotesize Project FP7-ICT-2009-C-243881 |
---|
34 | } |
---|
35 | \date{CerCo review meeting\\16th May 2013} |
---|
36 | \maketitle |
---|
37 | |
---|
38 | |
---|
39 | \begin{frame}{CerCo Outcomes} |
---|
40 | |
---|
41 | The final results of the CerCo project include the following: |
---|
42 | |
---|
43 | \medskip % |
---|
44 | \begin{itemize} |
---|
45 | \item A compiler from C to executable 8051 binaries, formalised in Matita as |
---|
46 | \blue{\lstinline|compiler.ma|} \dots |
---|
47 | \item \dots which adds labels and cost information to C source code |
---|
48 | \item \dots with exact values for time and space used by the binary. |
---|
49 | |
---|
50 | \medskip % |
---|
51 | \item A machine-checked proof of this in Matita |
---|
52 | \blue{\lstinline|correctness.ma|}: |
---|
53 | |
---|
54 | \smallskip % |
---|
55 | \begin{itemize} |
---|
56 | \item Addressing \red{intensional} properties --- clock cycles, stack bytes |
---|
57 | |
---|
58 | \smallskip % |
---|
59 | \item As well as \red{extensional} properties --- functional correctness. |
---|
60 | \end{itemize} |
---|
61 | \item An executable cost-annotating compiler \blue{\lstinline|cerco|} |
---|
62 | extracted from the formalisation. |
---|
63 | \end{itemize} |
---|
64 | |
---|
65 | \medskip % |
---|
66 | This talk treats the front-end compiler and proof, describing the technical |
---|
67 | challenges and contributions from the work in Period~3. |
---|
68 | |
---|
69 | \end{frame} |
---|
70 | |
---|
71 | \begin{frame}{Compiler} |
---|
72 | |
---|
73 | The CerCo compiler, given C source code, will generate: |
---|
74 | \begin{itemize} |
---|
75 | \item Labelled Clight source code; |
---|
76 | \item Labelled 8051 object code; |
---|
77 | \item Cost maps: for each label a count of time (clock cycles) and space |
---|
78 | (stack bytes) usage. |
---|
79 | \end{itemize} |
---|
80 | |
---|
81 | \medskip % |
---|
82 | The compiler operates in multiple passes, with each intermediate language |
---|
83 | having an executable semantics in Matita: % |
---|
84 | \vspace*{-\medskipamount} |
---|
85 | \begin{center} |
---|
86 | \includegraphics[width=0.7\linewidth]{compiler-plain.pdf} |
---|
87 | \end{center} |
---|
88 | \vspace*{-\medskipamount} |
---|
89 | |
---|
90 | \end{frame} |
---|
91 | |
---|
92 | \begin{frame}{Correctness} |
---|
93 | |
---|
94 | Suppose we have C source with labelled Clight, labelled 8051 binary, and |
---|
95 | cost maps all generated from the CerCo compiler. |
---|
96 | |
---|
97 | \medskip % |
---|
98 | Then the Matita theorem for correctness is that: |
---|
99 | \begin{itemize} |
---|
100 | \item Executing the original and labelled Clight source gives the same |
---|
101 | behaviour; |
---|
102 | \item Executing the 8051 binary gives the same observables: labels and |
---|
103 | call/return; |
---|
104 | \item Applying the cost maps to the trace of C labels correctly |
---|
105 | describes the time and space usage of the 8051 execution. |
---|
106 | \end{itemize} |
---|
107 | |
---|
108 | In fact we give an exact result on all \red{measurable subtraces}: from any |
---|
109 | label to the end of its enclosing function. |
---|
110 | |
---|
111 | \medskip % |
---|
112 | The machine-checked proof is the concatenation of correctness results for |
---|
113 | the front end, the back end, and the assembler. |
---|
114 | |
---|
115 | \end{frame} |
---|
116 | |
---|
117 | \begin{frame}{Front-End Progress} |
---|
118 | |
---|
119 | \vspace*{-\bigskipamount} |
---|
120 | \begin{center} |
---|
121 | \includegraphics[width=0.7\linewidth]{compiler-plain.pdf} |
---|
122 | \end{center} |
---|
123 | \vspace*{-\medskipamount} |
---|
124 | |
---|
125 | At the start of Period~3 the front end included in Matita: |
---|
126 | \begin{itemize} |
---|
127 | \item Executable semantics for source and intermediate languages; |
---|
128 | \item Labelling and compilation of source through these; |
---|
129 | \item Innovation of \red{structured traces}, originally to support timing |
---|
130 | computation in the assembler. |
---|
131 | \end{itemize} |
---|
132 | |
---|
133 | At the completion of Period~3, the front end included proofs of correctness |
---|
134 | for all these, extension to stack usage, and considerable refinement of the |
---|
135 | existing formal development. |
---|
136 | |
---|
137 | \end{frame} |
---|
138 | |
---|
139 | \begin{frame}{Front-End Contribution} |
---|
140 | |
---|
141 | Notable features and original elements of the front-end include: |
---|
142 | \begin{itemize} |
---|
143 | \item Proof layering: |
---|
144 | \begin{itemize} |
---|
145 | \item A \blue{functional correctness proof}; |
---|
146 | \item A \blue{cost proof}, separate but depending on functional |
---|
147 | correctness. |
---|
148 | \end{itemize} |
---|
149 | \item \blue{Internal checks} as a proof shortcut, like translation |
---|
150 | validation. |
---|
151 | \item \blue{Structured traces} for holding detailed data on resource |
---|
152 | behaviour, not just for assembler cost calculation. |
---|
153 | \item Introduction of \blue{measurable subtraces} as a unit of cost |
---|
154 | proof. |
---|
155 | \end{itemize} |
---|
156 | These features are significant in particular because: |
---|
157 | \begin{itemize} |
---|
158 | \item Compilation is not 1-1 transliteration: code is rearranged and |
---|
159 | modified, but label sequencing is preserved; |
---|
160 | \item The source language has implicit control flow constraints not present |
---|
161 | in the target (call/return, branches, loops). |
---|
162 | \end{itemize} |
---|
163 | |
---|
164 | \end{frame} |
---|
165 | |
---|
166 | \begin{frame}{Axiomatization} |
---|
167 | |
---|
168 | The translation in \blue{\lstinline|compile.ma|} is complete --- essential |
---|
169 | for extracting a compiler. |
---|
170 | |
---|
171 | \medskip % |
---|
172 | The simulation results in \blue{\lstinline|correctness.ma|} are fully |
---|
173 | specified, and with substantially complete proofs. Some parts, however, |
---|
174 | have been axiomatized and their correctness assumed. |
---|
175 | |
---|
176 | \medskip % |
---|
177 | In the front-end there are two sources of this axiomatisation: |
---|
178 | \begin{itemize} |
---|
179 | \item \red{Functional correctness.} Other projects, notably |
---|
180 | \blue{CompCert}, provide assurances that such proofs can be completed; so |
---|
181 | certain parts of this proof have been assumed. |
---|
182 | \item Simulation steps with \red{many cases}, sometimes similar; here we |
---|
183 | have identified representative and more challenging cases for detailed |
---|
184 | proof. |
---|
185 | \end{itemize} |
---|
186 | |
---|
187 | \end{frame} |
---|
188 | |
---|
189 | \begin{frame}[fragile] |
---|
190 | \frametitle{Structure of the Proof} |
---|
191 | |
---|
192 | \begin{center} |
---|
193 | \includegraphics[width=0.7\linewidth]{compiler.pdf} |
---|
194 | \end{center} |
---|
195 | |
---|
196 | The transition from front-end to back-end marks the change: |
---|
197 | \begin{itemize} |
---|
198 | \item From a language with explicit call/return structure and high-level |
---|
199 | control flow; |
---|
200 | \item To a language with explicit addresses and control-flow graph. |
---|
201 | \end{itemize} |
---|
202 | |
---|
203 | Correspondingly, the proof hands over |
---|
204 | \begin{itemize} |
---|
205 | \item From measurable subtraces with labelling that must be checked |
---|
206 | \blue{sound} and \blue{precise}; |
---|
207 | \item To \blue{structured traces} which embed these invariants. |
---|
208 | \end{itemize} |
---|
209 | |
---|
210 | \end{frame} |
---|
211 | |
---|
212 | |
---|
213 | % \frame{ |
---|
214 | % \frametitle{Introduction} |
---|
215 | |
---|
216 | % D3.4 is the front-end correctness proofs: |
---|
217 | |
---|
218 | % \begin{description} |
---|
219 | % \item[Primary focus:] novel \red{intensional} properties: \blue{cost |
---|
220 | % bound correctness} |
---|
221 | % \item[Secondary:] usual \red{extensional} result: \blue{functional correctness} |
---|
222 | % \end{description} |
---|
223 | |
---|
224 | % Functional correctness for similar compilers already studied in |
---|
225 | % Leroy et al.'s \blue{CompCert}. |
---|
226 | % \begin{itemize} |
---|
227 | % \item Axiomatize similar results |
---|
228 | % \end{itemize} |
---|
229 | |
---|
230 | % \medskip |
---|
231 | % Now have \blue{stack} costs as well as \blue{time} |
---|
232 | % \begin{itemize} |
---|
233 | % \item yields stronger overall correctness result |
---|
234 | % \end{itemize} |
---|
235 | |
---|
236 | % \medskip |
---|
237 | % \alert{Extract} compiler code from development for practical execution. |
---|
238 | |
---|
239 | % \medskip |
---|
240 | % Informed by earlier formal experiment with a toy compiler. |
---|
241 | % } |
---|
242 | |
---|
243 | % TODO: could reuse some of this to make stronger intro? |
---|
244 | % \frame{ |
---|
245 | % \frametitle{Motivation for formalisation} |
---|
246 | |
---|
247 | % \begin{enumerate} |
---|
248 | % \item Provide \alert{assurance} about labelling approach |
---|
249 | % \begin{itemize} |
---|
250 | % \item more complex setting than toy compiler |
---|
251 | % \end{itemize} |
---|
252 | % \item demonstrate feasibility of \alert{certified} WCET toolchain |
---|
253 | % % Future: proof translating compiler to provide checkable WCET certificate? |
---|
254 | % \item new experiments with certified compilation: |
---|
255 | % \begin{itemize} |
---|
256 | % \item deeper use of \alert{dependent types} |
---|
257 | % \item \alert{executable} semantics in type theory |
---|
258 | % \item certification of \alert{optimising assembler} |
---|
259 | % \end{itemize} |
---|
260 | % \end{enumerate} |
---|
261 | |
---|
262 | % \bigskip |
---|
263 | % \pause |
---|
264 | |
---|
265 | % \bigskip |
---|
266 | % Concentrate on cost correctness. |
---|
267 | % \begin{itemize} |
---|
268 | % \item Keep \alert{extensional} proofs as separate as possible |
---|
269 | % \end{itemize} |
---|
270 | % } |
---|
271 | |
---|
272 | % \frame{ |
---|
273 | % \frametitle{Outline} |
---|
274 | % \tableofcontents |
---|
275 | % } |
---|
276 | |
---|
277 | % \section{CerCo Compiler} |
---|
278 | |
---|
279 | % \frame{ |
---|
280 | % \frametitle{CerCo compiler} |
---|
281 | |
---|
282 | % \begin{center} |
---|
283 | % \includegraphics[width=0.8\linewidth]{compiler-plain.pdf} |
---|
284 | % \end{center} |
---|
285 | |
---|
286 | % \begin{itemize} |
---|
287 | % \item Reuse unverified CompCert parser |
---|
288 | % %\item Transform away troublesome constructs |
---|
289 | % % \begin{itemize} |
---|
290 | % % \item e.g.~\texttt{switch} |
---|
291 | % % \item fallthrough requires slightly more sophisticated labelling |
---|
292 | % % \item but not fundamentally different |
---|
293 | % % \end{itemize} |
---|
294 | % \item Intermediate language for most passes |
---|
295 | % \item Executable semantics for each |
---|
296 | % \item Outputs |
---|
297 | % \begin{itemize} |
---|
298 | % \item 8051 machine code |
---|
299 | % \item Clight code instrumented with costs in 8051 clock cycles and |
---|
300 | % bytes of stack space |
---|
301 | % \end{itemize} |
---|
302 | % \end{itemize} |
---|
303 | % Instrumentation updates global cost variable; suitable for further analysis and |
---|
304 | % verification. |
---|
305 | % } |
---|
306 | |
---|
307 | % \section{Overall correctness} |
---|
308 | |
---|
309 | % \begin{frame}[fragile] |
---|
310 | % \frametitle{Correctness of labelling approach} |
---|
311 | |
---|
312 | % \begin{tabular}{ccc} |
---|
313 | |
---|
314 | % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
315 | % emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
316 | % char f(char x) { |
---|
317 | % char y; |
---|
318 | % _cost3: |
---|
319 | % if (x>10) { |
---|
320 | % _cost1: |
---|
321 | % y = g(x); |
---|
322 | % } else { |
---|
323 | % _cost2: |
---|
324 | % y = 5; |
---|
325 | % } |
---|
326 | % return y+1; |
---|
327 | % } |
---|
328 | % \end{lstlisting} |
---|
329 | |
---|
330 | % & |
---|
331 | |
---|
332 | % \begin{minipage}{9em} |
---|
333 | % \begin{center} |
---|
334 | % $\Rightarrow$\\[4ex] |
---|
335 | % \blue{soundness}\\[2ex] |
---|
336 | % \red{precision} |
---|
337 | % \end{center} |
---|
338 | % \end{minipage} |
---|
339 | |
---|
340 | % & |
---|
341 | |
---|
342 | % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
343 | % emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
344 | % "f" |
---|
345 | % emit _cost3 |
---|
346 | % *** Prologue *** |
---|
347 | % move A, R06 |
---|
348 | % clear CARRY |
---|
349 | % ... |
---|
350 | % branch A <> 0, f10 |
---|
351 | % emit _cost2 |
---|
352 | % imm R00, 5 |
---|
353 | % ... |
---|
354 | % f10: |
---|
355 | % emit _cost1 |
---|
356 | % call "g" |
---|
357 | % ... |
---|
358 | % \end{lstlisting} |
---|
359 | |
---|
360 | |
---|
361 | % \end{tabular} |
---|
362 | |
---|
363 | % From experiments with toy compiler [D2.1, FMICS'12]: |
---|
364 | % \begin{enumerate} |
---|
365 | % \item Functional correctness, \emph{including trace of labels} |
---|
366 | % %\item Source labelling function is sound and precise |
---|
367 | % %\item Preservation of soundness and precision of labelling |
---|
368 | % \item Target labelling function is sound and precise |
---|
369 | % % TODO: detail about soundness and precision? |
---|
370 | % \item Target cost analysis produces a map of labels to times |
---|
371 | % \begin{itemize} |
---|
372 | % \item Accurate for sound and precise labellings |
---|
373 | % \end{itemize} |
---|
374 | % %\item Correctness of instrumentation |
---|
375 | % \end{enumerate} |
---|
376 | |
---|
377 | % \end{frame} |
---|
378 | |
---|
379 | % %\frame{ |
---|
380 | % %\frametitle{} |
---|
381 | % % |
---|
382 | % %Due to resource constraints |
---|
383 | % %\begin{itemize} |
---|
384 | % %\item Instrumentation is done in language semantics |
---|
385 | % %\item Soundness and precision of labelling is checked during compilation |
---|
386 | % % \begin{itemize} |
---|
387 | % % \item c.f.~translation validation |
---|
388 | % % \end{itemize} |
---|
389 | % %\item Focusing effort on novel parts --- cost proofs over functional correctness |
---|
390 | % %\end{itemize} |
---|
391 | % % |
---|
392 | % %} |
---|
393 | |
---|
394 | % \begin{frame}[fragile] |
---|
395 | % \frametitle{Overall correctness statement} |
---|
396 | |
---|
397 | % \begin{center} |
---|
398 | % \fbox{\( \text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)} |
---|
399 | % \end{center} |
---|
400 | |
---|
401 | % \pause |
---|
402 | |
---|
403 | % \begin{center} |
---|
404 | % \begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c} |
---|
405 | |
---|
406 | % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
407 | % emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
408 | % int f(int x) { |
---|
409 | % _cost1: |
---|
410 | % int y = 0; |
---|
411 | % while (x) { |
---|
412 | % _cost2: |
---|
413 | % y = g(y); |
---|
414 | % x = x - 1; |
---|
415 | % } |
---|
416 | % _cost3: |
---|
417 | % return y; |
---|
418 | % } |
---|
419 | % \end{lstlisting} |
---|
420 | |
---|
421 | % & |
---|
422 | |
---|
423 | % \begin{uncoverenv}<2-3> |
---|
424 | % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
425 | % emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
426 | % call f |
---|
427 | % _cost1 |
---|
428 | % init y |
---|
429 | % _cost2 |
---|
430 | % call g |
---|
431 | % ... |
---|
432 | % return g |
---|
433 | % assign y |
---|
434 | % decrement x |
---|
435 | % test x |
---|
436 | % _cost2 |
---|
437 | % ... |
---|
438 | % _cost3 |
---|
439 | % return f |
---|
440 | % \end{lstlisting} |
---|
441 | % \end{uncoverenv} |
---|
442 | |
---|
443 | % & |
---|
444 | |
---|
445 | % \begin{uncoverenv}<3-5> |
---|
446 | % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
447 | % emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
448 | % call f |
---|
449 | % _cost1 |
---|
450 | |
---|
451 | % _cost2 |
---|
452 | % call g |
---|
453 | % ... |
---|
454 | % return g |
---|
455 | |
---|
456 | |
---|
457 | |
---|
458 | % _cost2 |
---|
459 | % ... |
---|
460 | % _cost3 |
---|
461 | % return f |
---|
462 | % \end{lstlisting} |
---|
463 | % \end{uncoverenv} |
---|
464 | |
---|
465 | % \end{tabular} |
---|
466 | % \end{center} |
---|
467 | |
---|
468 | % \begin{overprint} |
---|
469 | % \onslide<2> |
---|
470 | % \begin{itemize} |
---|
471 | % \item Use labels and end of function as measurement points |
---|
472 | % \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' |
---|
473 | % \end{itemize} |
---|
474 | |
---|
475 | % \onslide<3-4> |
---|
476 | % \begin{itemize} |
---|
477 | % \item Use labels and end of function as measurement points |
---|
478 | % \item All costs are considered local to the function |
---|
479 | % \item Actual position of unobservable computation is unimportant |
---|
480 | % \end{itemize} |
---|
481 | |
---|
482 | % \onslide<5> |
---|
483 | % \begin{itemize} |
---|
484 | % \item Use labels and end of function as measurement points |
---|
485 | % \item[$\star$] Call suitable subtraces \alert{measurable} |
---|
486 | % \item[$\star$] Core part is a proof of \alert{termination} |
---|
487 | % \end{itemize} |
---|
488 | % \end{overprint} |
---|
489 | |
---|
490 | % \end{frame} |
---|
491 | |
---|
492 | % \begin{frame}[fragile] |
---|
493 | % \frametitle{Correct cost analysis depends on call structure} |
---|
494 | |
---|
495 | % Two straight-line functions: |
---|
496 | |
---|
497 | % \begin{center} |
---|
498 | % \begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}} |
---|
499 | |
---|
500 | % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
501 | % emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
502 | % "f" |
---|
503 | % emit _cost1 |
---|
504 | % ... |
---|
505 | % call "g" |
---|
506 | % ... |
---|
507 | % return |
---|
508 | % \end{lstlisting} |
---|
509 | |
---|
510 | % & |
---|
511 | |
---|
512 | % \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
513 | % emph={[2]_cost3},emphstyle={[2]\color{blue}}, |
---|
514 | % escapechar=\%] |
---|
515 | % "g" |
---|
516 | % emit _cost2 |
---|
517 | % ... |
---|
518 | % %\only<2->{\blue{increase return address}}% |
---|
519 | % return |
---|
520 | % \end{lstlisting} |
---|
521 | |
---|
522 | % \end{tabular} |
---|
523 | % \end{center} |
---|
524 | |
---|
525 | % Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}). |
---|
526 | |
---|
527 | % \begin{itemize} |
---|
528 | % \item<2-> Changing return address skips code from \lstinline'f' |
---|
529 | % \item<2-> Cost no longer equals sum of cost labels |
---|
530 | % \end{itemize} |
---|
531 | |
---|
532 | % \onslide<2-> |
---|
533 | % \alert{Need to observe correct call/return structure.} |
---|
534 | |
---|
535 | % \onslide<3> |
---|
536 | % \emph{Not easy at ASM --- observe earlier in compiler \& maintain.} |
---|
537 | |
---|
538 | % \end{frame} |
---|
539 | |
---|
540 | % \section{Front-end correctness} |
---|
541 | |
---|
542 | % \frame{ |
---|
543 | % \frametitle{Front-end correctness} |
---|
544 | |
---|
545 | % Recalling the toy compiler, need |
---|
546 | % \begin{enumerate} |
---|
547 | % \item Functional correctness |
---|
548 | % \item Cost labelling sound and precise |
---|
549 | % \item\label{it:return} To demonstrate return addresses are correct |
---|
550 | % \end{enumerate} |
---|
551 | % % TODO: stack space? from obs, from fnl correctness |
---|
552 | |
---|
553 | % \bigskip |
---|
554 | % For~\ref{it:return} we generalise notion of \emph{structured traces} |
---|
555 | % originally introduced for the correctness of timing analysis. |
---|
556 | % } |
---|
557 | |
---|
558 | \begin{frame}[fragile] |
---|
559 | \frametitle{Structured traces} |
---|
560 | |
---|
561 | Embed call structure and label invariants into execution traces. |
---|
562 | |
---|
563 | \begin{center} |
---|
564 | \includegraphics{strtraces.pdf} |
---|
565 | \end{center} |
---|
566 | |
---|
567 | \begin{itemize} |
---|
568 | \item Enforces \blue{invariants} on positions of cost labels. |
---|
569 | \item \blue{Groups} execution steps according to preceding cost label. |
---|
570 | \item Forbids \blue{repeating} addresses in grouped steps. |
---|
571 | \end{itemize} |
---|
572 | |
---|
573 | Constructed by folding up measurable subtraces, using the fact that labelling |
---|
574 | is sound and precise. |
---|
575 | |
---|
576 | \end{frame} |
---|
577 | |
---|
578 | \begin{frame}{Step-by-Step: Getting to Labelled Source} |
---|
579 | |
---|
580 | \blue{C $\to$ Clight} |
---|
581 | |
---|
582 | \smallskip % |
---|
583 | To translate from C to Clight we reuse the CompCert parser. |
---|
584 | |
---|
585 | \bigskip % |
---|
586 | \blue{Switch Removal} |
---|
587 | |
---|
588 | \smallskip % |
---|
589 | Control flow for \red{\lstinline'switch'} is too subtle for simple labelling; |
---|
590 | we replace with an \red{\lstinline'if .. then .. else'} tree. Proof requires |
---|
591 | tracking memory extension for an extra test variable. |
---|
592 | |
---|
593 | \bigskip % |
---|
594 | \blue{Cost Labels} |
---|
595 | |
---|
596 | \smallskip % |
---|
597 | Labels added at function start, branch targets, \dots |
---|
598 | |
---|
599 | \smallskip % |
---|
600 | Simulation of execution is exact, just skipping over labels. |
---|
601 | |
---|
602 | \end{frame} |
---|
603 | |
---|
604 | \begin{frame}{Front-End Correctness} |
---|
605 | |
---|
606 | Suppose we have a \blue{measurable} subtrace of Clight execution, including |
---|
607 | the \blue{prefix} of that trace from initial state. |
---|
608 | |
---|
609 | \medskip % |
---|
610 | Then for handover to the back-end we have in RTLabs: |
---|
611 | \begin{itemize} |
---|
612 | \item A corresponding \red{prefix}; |
---|
613 | \item A \red{structured trace} corresponding to the measurable subtrace; |
---|
614 | \item The required invariants, including \red{no repeating addresses}; |
---|
615 | \item A proof that the same \red{stack limit} is observed. |
---|
616 | \end{itemize} |
---|
617 | |
---|
618 | \medskip % |
---|
619 | In addition, to link this with the source program: |
---|
620 | \begin{itemize} |
---|
621 | \item The observables for the RLabs \blue{prefix} and \blue{structured |
---|
622 | trace} are the same as for their counterparts in Clight. |
---|
623 | \end{itemize} |
---|
624 | |
---|
625 | \end{frame} |
---|
626 | |
---|
627 | |
---|
628 | % \section{Correctness proofs} |
---|
629 | % \subsection{Generic lifting result} |
---|
630 | |
---|
631 | \begin{frame}[fragile] |
---|
632 | \frametitle{Lifting measurable traces} |
---|
633 | |
---|
634 | For each pass find a target \alert{measurable} subtrace |
---|
635 | \alert{equivalent} to any source \alert{measurable} subtrace. |
---|
636 | |
---|
637 | \bigskip |
---|
638 | |
---|
639 | \onslide<2-> |
---|
640 | \begin{center} |
---|
641 | \includegraphics{meassim.pdf} |
---|
642 | \end{center} |
---|
643 | |
---|
644 | Split normal simulation proof: |
---|
645 | \begin{enumerate} |
---|
646 | \item each \blue{call} becomes a \blue{call} step plus zero or |
---|
647 | more \blue{normal} steps;\\ |
---|
648 | following cost labels should stay next to the call step |
---|
649 | \item each \blue{return} becomes a \blue{return} plus zero or |
---|
650 | more \blue{normal} steps |
---|
651 | \item \blue{cost} label steps are preserved |
---|
652 | \item other \blue{normal} steps become zero or more \blue{normal} steps |
---|
653 | \end{enumerate} |
---|
654 | |
---|
655 | \bigskip |
---|
656 | \onslide<3-> |
---|
657 | Preserves the defining termination property for \alert{measurable} subtraces. |
---|
658 | |
---|
659 | % \bigskip |
---|
660 | % \onslide<4-> |
---|
661 | % Due to time pressures, check \alert{soundness} and \alert{precision} of cost |
---|
662 | % labels at RTLabs. |
---|
663 | |
---|
664 | \end{frame} |
---|
665 | |
---|
666 | %\begin{frame}[fragile] |
---|
667 | %\frametitle{Structured trace simulation} |
---|
668 | % |
---|
669 | %Lift \alert{local} simulations to \alert{structured trace} simulations |
---|
670 | %similarly. |
---|
671 | % |
---|
672 | %\bigskip |
---|
673 | %\pause |
---|
674 | %\begin{itemize} |
---|
675 | %\item |
---|
676 | %Require local simulations for \alert{normal}, \alert{call} and \alert{return} |
---|
677 | %steps |
---|
678 | %\item allow traces to expand with extra \alert{normal} steps, |
---|
679 | %\item allow us to collapse some \alert{normal} steps |
---|
680 | % \begin{itemize} |
---|
681 | % \item but not collapse \blue{labelled} steps |
---|
682 | % % TODO: why? avoid larger change in structure |
---|
683 | % \item or change call structure |
---|
684 | % \end{itemize} |
---|
685 | %\end{itemize} |
---|
686 | % |
---|
687 | %\bigskip |
---|
688 | %Sufficient to calculate structured trace in target. |
---|
689 | %% TODO: pics |
---|
690 | % |
---|
691 | %\end{frame} |
---|
692 | % |
---|
693 | %\begin{frame}[fragile] |
---|
694 | %\frametitle{Structured trace local simulation example} |
---|
695 | % |
---|
696 | %For function call steps: |
---|
697 | %\begin{center} |
---|
698 | %\includegraphics[width=0.7\linewidth]{strcall.pdf} |
---|
699 | %\end{center} |
---|
700 | % |
---|
701 | %\begin{itemize} |
---|
702 | %\item May add extra steps before and after |
---|
703 | %\item Extra steps must not be call/return |
---|
704 | %\item Must call the same function |
---|
705 | %\item Cost label must stay at start of function |
---|
706 | %\end{itemize} |
---|
707 | % |
---|
708 | %\end{frame} |
---|
709 | |
---|
710 | % \subsection{Simulations for compiler passes} |
---|
711 | |
---|
712 | %\frame{ |
---|
713 | %\frametitle{TODO: at least two slides on simulations} |
---|
714 | %} |
---|
715 | |
---|
716 | % TODO: perhaps much earlier for the pre-measurable bits? |
---|
717 | |
---|
718 | \frame{ |
---|
719 | \frametitle{Front-end simulation results} |
---|
720 | Cast simplification |
---|
721 | \begin{itemize} |
---|
722 | \item Simplify expressions for 8-bit target |
---|
723 | \item Only expressions change --- statements are in lock-step |
---|
724 | \item Difficult part: we allow ill-typed \textbf{Clight} at this stage |
---|
725 | \item Simulation proofs complete |
---|
726 | \end{itemize} |
---|
727 | |
---|
728 | \textbf{Clight} to \textbf{Cminor} |
---|
729 | \begin{itemize} |
---|
730 | \item Stack allocation and control flow transformation |
---|
731 | \item Similar to \textbf{CompCert}, but produces \lstinline'goto' |
---|
732 | instead of \lstinline'loop' |
---|
733 | \item Expressions complete |
---|
734 | \item Prove a selection of statements, in particular \lstinline'while' |
---|
735 | \item Tricky: Large proof terms for invariant embedded in |
---|
736 | \textbf{Cminor} programs using dependent types;\\ |
---|
737 | generalise them away, but difficult under binders |
---|
738 | %TODO explain clearly |
---|
739 | \end{itemize} |
---|
740 | } |
---|
741 | \frame{ |
---|
742 | \frametitle{Front-end simulation results} |
---|
743 | \textbf{Cminor} to \textbf{RTLabs} |
---|
744 | \begin{itemize} |
---|
745 | \item Construction of control-flow graph |
---|
746 | \item Axiomatized simulations |
---|
747 | \item But do have invariants: |
---|
748 | \begin{itemize} |
---|
749 | \item Statement well-typed with respect to pseudo-register |
---|
750 | environment |
---|
751 | \item CFG complete |
---|
752 | \item Entry and exit nodes complete, unique |
---|
753 | \end{itemize} |
---|
754 | \item Translation function is \emph{total} as a result |
---|
755 | \end{itemize} |
---|
756 | } |
---|
757 | |
---|
758 | % TODO: sloganize: proved more about unusual bits |
---|
759 | |
---|
760 | % \section{Checking cost labelling properties} |
---|
761 | |
---|
762 | \frame{ |
---|
763 | \frametitle{Checking cost labelling properties} |
---|
764 | |
---|
765 | Check cost labelling is \red{sound} and \blue{precise} at |
---|
766 | \textbf{RTLabs}. |
---|
767 | \begin{itemize} |
---|
768 | \item Shortcut; similar to translation validation |
---|
769 | \end{itemize} |
---|
770 | |
---|
771 | \medskip |
---|
772 | At \textbf{RTLabs} properties become |
---|
773 | \begin{description} |
---|
774 | \item[\red{soundness}] bound on number of instructions in CFG until label\\ |
---|
775 | label at start of every function |
---|
776 | \item[\blue{precision}] label after every branch |
---|
777 | \end{description} |
---|
778 | |
---|
779 | \medskip |
---|
780 | Bound is the hard part; the rest is a simple syntactic check. |
---|
781 | } |
---|
782 | |
---|
783 | \begin{frame}[fragile] |
---|
784 | \frametitle{Bound on number of instructions until label} |
---|
785 | |
---|
786 | \begin{center} |
---|
787 | \includegraphics<1>[width=.4\linewidth]{loop.pdf} |
---|
788 | \includegraphics<2>[width=.4\linewidth]{loop1.pdf} |
---|
789 | \includegraphics<3>[width=.4\linewidth]{loop2.pdf} |
---|
790 | \includegraphics<4>[width=.4\linewidth]{loop3.pdf} |
---|
791 | \includegraphics<5>[width=.4\linewidth]{loop4.pdf} |
---|
792 | \includegraphics<6>[width=.4\linewidth]{loopx.pdf} |
---|
793 | \end{center} |
---|
794 | |
---|
795 | \begin{itemize} |
---|
796 | \item Pick an arbitrary node in the CFG |
---|
797 | \item<2-> Follow successor instructions |
---|
798 | \item<4-> If we find a \alert{cost label} all the traced nodes have a bound\dots |
---|
799 | \item<5-> \dots so remove them and pick a new node, continue |
---|
800 | \item<6-> But if we find an \alert{unlabelled loop} the labelling is unsound, |
---|
801 | report an error |
---|
802 | \end{itemize} |
---|
803 | |
---|
804 | \end{frame} |
---|
805 | |
---|
806 | \frame{ |
---|
807 | \frametitle{Checking cost labelling properties} |
---|
808 | |
---|
809 | This compile-time check is |
---|
810 | \begin{itemize} |
---|
811 | \item[$-$] partial |
---|
812 | \item[$-$] extra work in compilation |
---|
813 | \item[$\mp$] not proving anything about compilation passes |
---|
814 | \item[$+$] less proof burden |
---|
815 | \end{itemize} |
---|
816 | |
---|
817 | \bigskip |
---|
818 | In a full proof would go from |
---|
819 | \begin{quote} |
---|
820 | cost labels at the head of loops in \textbf{Cminor} |
---|
821 | \end{quote} |
---|
822 | to |
---|
823 | \begin{quote} |
---|
824 | bound on instructions to cost label in \textbf{RTLabs} |
---|
825 | \end{quote} |
---|
826 | Showing existence of the bound alone likely to require at least as much |
---|
827 | proof effort as this check. |
---|
828 | |
---|
829 | } |
---|
830 | |
---|
831 | % \section{Construction of structured traces} |
---|
832 | |
---|
833 | \frame{ |
---|
834 | \frametitle{Construction of structured traces} |
---|
835 | \begin{center} |
---|
836 | \includegraphics{strtraces.pdf} |
---|
837 | \end{center} |
---|
838 | \begin{enumerate} |
---|
839 | \item Extend sound and precise labelling to semantic states |
---|
840 | \item Prove they are preserved by steps of semantics |
---|
841 | \item Prove \textbf{RTLabs} semantics preserve the stack |
---|
842 | \item Use \alert{termination} proof from \alert{measurable} subtrace |
---|
843 | to create structure |
---|
844 | \item Proof obligations for cost labelling are discharged by semantic |
---|
845 | results above |
---|
846 | \end{enumerate} |
---|
847 | } |
---|
848 | |
---|
849 | % \section{Whole compiler} |
---|
850 | |
---|
851 | \begin{frame}[fragile] |
---|
852 | \frametitle{Putting the proof together} |
---|
853 | |
---|
854 | \begin{center} |
---|
855 | \includegraphics[width=0.8\linewidth]{compiler.pdf} |
---|
856 | \end{center} |
---|
857 | |
---|
858 | \begin{itemize} |
---|
859 | \item `Clock' difference in Clight is sum of cost labels |
---|
860 | \item Observables, including trace of labels, is preserved to ASM |
---|
861 | \item Labelling at bottom level is sound and precise |
---|
862 | \item Sum of labels at ASM is equal to difference in real clock |
---|
863 | \end{itemize} |
---|
864 | |
---|
865 | \end{frame} |
---|
866 | |
---|
867 | \frame{ |
---|
868 | \frametitle{Conclusion} |
---|
869 | |
---|
870 | Sketched proof for formalised CerCo front-end |
---|
871 | |
---|
872 | \begin{itemize} |
---|
873 | \item Intensional proofs can be layered on top of extensional results |
---|
874 | \item Preserving call-structure key ingredient |
---|
875 | \item Compile-time cost labelling checks can reduce proof burden |
---|
876 | \item[$\star$] Don't need huge changes to extensional proof techniques |
---|
877 | \end{itemize} |
---|
878 | |
---|
879 | \pause |
---|
880 | Future: |
---|
881 | \begin{itemize} |
---|
882 | \item Expect results to generalise to more general labelling schemes |
---|
883 | \begin{itemize} |
---|
884 | \item hence more sophisticated targets |
---|
885 | \end{itemize} |
---|
886 | \item Other compiler correctness techniques |
---|
887 | \begin{itemize} |
---|
888 | \item Decompilation? |
---|
889 | \end{itemize} |
---|
890 | \end{itemize} |
---|
891 | |
---|
892 | } |
---|
893 | |
---|
894 | \end{document} |
---|
895 | |
---|
896 | % LocalWords: LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM |
---|
897 | % LocalWords: reexecutes subtrace RTLabs subtraces |
---|