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{Front-end Correctness Proofs} |
---|
29 | \author{Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark} |
---|
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 review meeting\\16th May 2013} |
---|
35 | \maketitle |
---|
36 | |
---|
37 | \frame{ |
---|
38 | \frametitle{Introduction} |
---|
39 | |
---|
40 | D3.4 is the front-end correctness proofs: |
---|
41 | |
---|
42 | \begin{description} |
---|
43 | \item[Primary focus:] novel \red{intensional} properties: \blue{cost |
---|
44 | bound correctness} |
---|
45 | \item[Secondary:] usual \red{extensional} result: \blue{functional correctness} |
---|
46 | \end{description} |
---|
47 | |
---|
48 | Functional correctness for similar compilers already studied in |
---|
49 | Leroy et al.'s \blue{CompCert}. |
---|
50 | \begin{itemize} |
---|
51 | \item Axiomatize similar results |
---|
52 | \end{itemize} |
---|
53 | |
---|
54 | \medskip |
---|
55 | Now have \blue{stack} costs as well as \blue{time} |
---|
56 | \begin{itemize} |
---|
57 | \item yields stronger overall correctness result |
---|
58 | \end{itemize} |
---|
59 | |
---|
60 | \medskip |
---|
61 | \alert{Extract} compiler code from development for practical execution. |
---|
62 | |
---|
63 | \medskip |
---|
64 | Informed by earlier formal experiment with a toy compiler. |
---|
65 | } |
---|
66 | |
---|
67 | % TODO: could reuse some of this to make stronger intro? |
---|
68 | % \frame{ |
---|
69 | % \frametitle{Motivation for formalisation} |
---|
70 | |
---|
71 | % \begin{enumerate} |
---|
72 | % \item Provide \alert{assurance} about labelling approach |
---|
73 | % \begin{itemize} |
---|
74 | % \item more complex setting than toy compiler |
---|
75 | % \end{itemize} |
---|
76 | % \item demonstrate feasibility of \alert{certified} WCET toolchain |
---|
77 | % % Future: proof translating compiler to provide checkable WCET certificate? |
---|
78 | % \item new experiments with certified compilation: |
---|
79 | % \begin{itemize} |
---|
80 | % \item deeper use of \alert{dependent types} |
---|
81 | % \item \alert{executable} semantics in type theory |
---|
82 | % \item certification of \alert{optimising assembler} |
---|
83 | % \end{itemize} |
---|
84 | % \end{enumerate} |
---|
85 | |
---|
86 | % \bigskip |
---|
87 | % \pause |
---|
88 | |
---|
89 | % \bigskip |
---|
90 | % Concentrate on cost correctness. |
---|
91 | % \begin{itemize} |
---|
92 | % \item Keep \alert{extensional} proofs as separate as possible |
---|
93 | % \end{itemize} |
---|
94 | % } |
---|
95 | |
---|
96 | \frame{ |
---|
97 | \frametitle{Outline} |
---|
98 | \tableofcontents |
---|
99 | } |
---|
100 | |
---|
101 | \section{CerCo Compiler} |
---|
102 | |
---|
103 | \frame{ |
---|
104 | \frametitle{CerCo compiler} |
---|
105 | |
---|
106 | \begin{center} |
---|
107 | \includegraphics[width=0.8\linewidth]{compiler-plain.pdf} |
---|
108 | \end{center} |
---|
109 | |
---|
110 | \begin{itemize} |
---|
111 | \item Reuse unverified CompCert parser |
---|
112 | %\item Transform away troublesome constructs |
---|
113 | % \begin{itemize} |
---|
114 | % \item e.g.~\texttt{switch} |
---|
115 | % \item fallthrough requires slightly more sophisticated labelling |
---|
116 | % \item but not fundamentally different |
---|
117 | % \end{itemize} |
---|
118 | \item Intermediate language for most passes |
---|
119 | \item Executable semantics for each |
---|
120 | \item Outputs |
---|
121 | \begin{itemize} |
---|
122 | \item 8051 machine code |
---|
123 | \item Clight code instrumented with costs in 8051 clock cycles and |
---|
124 | bytes of stack space |
---|
125 | \end{itemize} |
---|
126 | \end{itemize} |
---|
127 | Instrumentation updates global cost variable; suitable for further analysis and |
---|
128 | verification. |
---|
129 | } |
---|
130 | |
---|
131 | \section{Overall correctness} |
---|
132 | |
---|
133 | \begin{frame}[fragile] |
---|
134 | \frametitle{Correctness of labelling approach} |
---|
135 | |
---|
136 | \begin{tabular}{ccc} |
---|
137 | |
---|
138 | \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
139 | emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
140 | char f(char x) { |
---|
141 | char y; |
---|
142 | _cost3: |
---|
143 | if (x>10) { |
---|
144 | _cost1: |
---|
145 | y = g(x); |
---|
146 | } else { |
---|
147 | _cost2: |
---|
148 | y = 5; |
---|
149 | } |
---|
150 | return y+1; |
---|
151 | } |
---|
152 | \end{lstlisting} |
---|
153 | |
---|
154 | & |
---|
155 | |
---|
156 | \begin{minipage}{9em} |
---|
157 | \begin{center} |
---|
158 | $\Rightarrow$\\[4ex] |
---|
159 | \blue{soundness}\\[2ex] |
---|
160 | \red{precision} |
---|
161 | \end{center} |
---|
162 | \end{minipage} |
---|
163 | |
---|
164 | & |
---|
165 | |
---|
166 | \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
167 | emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
168 | "f" |
---|
169 | emit _cost3 |
---|
170 | *** Prologue *** |
---|
171 | move A, R06 |
---|
172 | clear CARRY |
---|
173 | ... |
---|
174 | branch A <> 0, f10 |
---|
175 | emit _cost2 |
---|
176 | imm R00, 5 |
---|
177 | ... |
---|
178 | f10: |
---|
179 | emit _cost1 |
---|
180 | call "g" |
---|
181 | ... |
---|
182 | \end{lstlisting} |
---|
183 | |
---|
184 | |
---|
185 | \end{tabular} |
---|
186 | |
---|
187 | From experiments with toy compiler [D2.1, FMICS'12]: |
---|
188 | \begin{enumerate} |
---|
189 | \item Functional correctness, \emph{including trace of labels} |
---|
190 | %\item Source labelling function is sound and precise |
---|
191 | %\item Preservation of soundness and precision of labelling |
---|
192 | \item Target labelling function is sound and precise |
---|
193 | % TODO: detail about soundness and precision? |
---|
194 | \item Target cost analysis produces a map of labels to times |
---|
195 | \begin{itemize} |
---|
196 | \item Accurate for sound and precise labellings |
---|
197 | \end{itemize} |
---|
198 | %\item Correctness of instrumentation |
---|
199 | \end{enumerate} |
---|
200 | |
---|
201 | \end{frame} |
---|
202 | |
---|
203 | %\frame{ |
---|
204 | %\frametitle{} |
---|
205 | % |
---|
206 | %Due to resource constraints |
---|
207 | %\begin{itemize} |
---|
208 | %\item Instrumentation is done in language semantics |
---|
209 | %\item Soundness and precision of labelling is checked during compilation |
---|
210 | % \begin{itemize} |
---|
211 | % \item c.f.~translation validation |
---|
212 | % \end{itemize} |
---|
213 | %\item Focusing effort on novel parts --- cost proofs over functional correctness |
---|
214 | %\end{itemize} |
---|
215 | % |
---|
216 | %} |
---|
217 | |
---|
218 | \begin{frame}[fragile] |
---|
219 | \frametitle{Overall correctness statement} |
---|
220 | |
---|
221 | \begin{center} |
---|
222 | \fbox{\( \text{machine time} = \Sigma_{l\in\text{source trace}} \text{costmap}(l) \)} |
---|
223 | \end{center} |
---|
224 | |
---|
225 | \pause |
---|
226 | |
---|
227 | \begin{center} |
---|
228 | \begin{tabular}{c@{\hspace{3em}}c@{\hspace{2em}}c} |
---|
229 | |
---|
230 | \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
231 | emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
232 | int f(int x) { |
---|
233 | _cost1: |
---|
234 | int y = 0; |
---|
235 | while (x) { |
---|
236 | _cost2: |
---|
237 | y = g(y); |
---|
238 | x = x - 1; |
---|
239 | } |
---|
240 | _cost3: |
---|
241 | return y; |
---|
242 | } |
---|
243 | \end{lstlisting} |
---|
244 | |
---|
245 | & |
---|
246 | |
---|
247 | \begin{uncoverenv}<2-3> |
---|
248 | \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
249 | emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
250 | call f |
---|
251 | _cost1 |
---|
252 | init y |
---|
253 | _cost2 |
---|
254 | call g |
---|
255 | ... |
---|
256 | return g |
---|
257 | assign y |
---|
258 | decrement x |
---|
259 | test x |
---|
260 | _cost2 |
---|
261 | ... |
---|
262 | _cost3 |
---|
263 | return f |
---|
264 | \end{lstlisting} |
---|
265 | \end{uncoverenv} |
---|
266 | |
---|
267 | & |
---|
268 | |
---|
269 | \begin{uncoverenv}<3-5> |
---|
270 | \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
271 | emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
272 | call f |
---|
273 | _cost1 |
---|
274 | |
---|
275 | _cost2 |
---|
276 | call g |
---|
277 | ... |
---|
278 | return g |
---|
279 | |
---|
280 | |
---|
281 | |
---|
282 | _cost2 |
---|
283 | ... |
---|
284 | _cost3 |
---|
285 | return f |
---|
286 | \end{lstlisting} |
---|
287 | \end{uncoverenv} |
---|
288 | |
---|
289 | \end{tabular} |
---|
290 | \end{center} |
---|
291 | |
---|
292 | \begin{overprint} |
---|
293 | \onslide<2> |
---|
294 | \begin{itemize} |
---|
295 | \item Use labels and end of function as measurement points |
---|
296 | \item[$\star$] From \red{\bf\_cost1} to \lstinline'return f' is cost of \lstinline'f' |
---|
297 | \end{itemize} |
---|
298 | |
---|
299 | \onslide<3-4> |
---|
300 | \begin{itemize} |
---|
301 | \item Use labels and end of function as measurement points |
---|
302 | \item All costs are considered local to the function |
---|
303 | \item Actual position of unobservable computation is unimportant |
---|
304 | \end{itemize} |
---|
305 | |
---|
306 | \onslide<5> |
---|
307 | \begin{itemize} |
---|
308 | \item Use labels and end of function as measurement points |
---|
309 | \item[$\star$] Call suitable subtraces \alert{measurable} |
---|
310 | \item[$\star$] Core part is a proof of \alert{termination} |
---|
311 | \end{itemize} |
---|
312 | \end{overprint} |
---|
313 | |
---|
314 | \end{frame} |
---|
315 | |
---|
316 | \begin{frame}[fragile] |
---|
317 | \frametitle{Correct cost analysis depends on call structure} |
---|
318 | |
---|
319 | Two straight-line functions: |
---|
320 | |
---|
321 | \begin{center} |
---|
322 | \begin{tabular}{p{0.4\linewidth}p{0.4\linewidth}} |
---|
323 | |
---|
324 | \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
325 | emph={[2]_cost3},emphstyle={[2]\color{blue}}] |
---|
326 | "f" |
---|
327 | emit _cost1 |
---|
328 | ... |
---|
329 | call "g" |
---|
330 | ... |
---|
331 | return |
---|
332 | \end{lstlisting} |
---|
333 | |
---|
334 | & |
---|
335 | |
---|
336 | \begin{lstlisting}[emph={_cost1,_cost2},emphstyle={\color{red}\bf}, |
---|
337 | emph={[2]_cost3},emphstyle={[2]\color{blue}}, |
---|
338 | escapechar=\%] |
---|
339 | "g" |
---|
340 | emit _cost2 |
---|
341 | ... |
---|
342 | %\only<2->{\blue{increase return address}}% |
---|
343 | return |
---|
344 | \end{lstlisting} |
---|
345 | |
---|
346 | \end{tabular} |
---|
347 | \end{center} |
---|
348 | |
---|
349 | Total cost should be costmap(\red{\bf\_cost1}) + costmap(\red{\bf\_cost2}). |
---|
350 | |
---|
351 | \begin{itemize} |
---|
352 | \item<2-> Changing return address skips code from \lstinline'f' |
---|
353 | \item<2-> Cost no longer equals sum of cost labels |
---|
354 | \end{itemize} |
---|
355 | |
---|
356 | \onslide<2-> |
---|
357 | \alert{Need to observe correct call/return structure.} |
---|
358 | |
---|
359 | \onslide<3> |
---|
360 | \emph{Not easy at ASM --- observe earlier in compiler \& maintain.} |
---|
361 | |
---|
362 | \end{frame} |
---|
363 | |
---|
364 | \section{Front-end correctness} |
---|
365 | |
---|
366 | \frame{ |
---|
367 | \frametitle{Front-end correctness} |
---|
368 | |
---|
369 | Recalling the toy compiler, need |
---|
370 | \begin{enumerate} |
---|
371 | \item Functional correctness |
---|
372 | \item Cost labelling sound and precise |
---|
373 | \item\label{it:return} To demonstrate return addresses are correct |
---|
374 | \end{enumerate} |
---|
375 | % TODO: stack space? from obs, from fnl correctness |
---|
376 | |
---|
377 | \bigskip |
---|
378 | For~\ref{it:return} we generalise notion of \emph{structured traces} |
---|
379 | originally introduced for the correctness of timing analysis. |
---|
380 | } |
---|
381 | |
---|
382 | \begin{frame}[fragile] |
---|
383 | \frametitle{Structured traces} |
---|
384 | |
---|
385 | \alert{Embed} the call/return structure into execution traces. |
---|
386 | |
---|
387 | \begin{center} |
---|
388 | \includegraphics{strtraces.pdf} |
---|
389 | \end{center} |
---|
390 | |
---|
391 | \begin{itemize} |
---|
392 | \item Traces of \alert{called functions} are nested |
---|
393 | \item Invariants on positions of cost labels enforced |
---|
394 | \item Steps are \alert{grouped} according to cost label |
---|
395 | \item Forbid \alert{repeating} addresses in grouped steps for |
---|
396 | \blue{sound} labelling |
---|
397 | \end{itemize} |
---|
398 | |
---|
399 | % moved later |
---|
400 | %\onslide<2> |
---|
401 | %Construct by folding up \alert{measurable} subtrace, using soundness |
---|
402 | %and preciseness of labelling. |
---|
403 | |
---|
404 | \end{frame} |
---|
405 | |
---|
406 | \frame{ |
---|
407 | \frametitle{Front-end correctness statement} |
---|
408 | |
---|
409 | Given a \blue{measurable} subtrace of a \textbf{Clight} execution, including |
---|
410 | the \textbf{prefix} of that trace from initial state, |
---|
411 | |
---|
412 | \medskip |
---|
413 | we have in \textbf{RTLabs} |
---|
414 | \begin{itemize} |
---|
415 | \item a new \textbf{prefix} |
---|
416 | \item a \red{structured trace} corresponding to \blue{measurable} |
---|
417 | subtrace |
---|
418 | \item the no \red{repeating} addresses property |
---|
419 | \item proof that the same \textbf{stack limit} is observed |
---|
420 | \end{itemize} |
---|
421 | which the back-end requires, and |
---|
422 | \begin{itemize} |
---|
423 | \item the observables for the \textbf{prefix} and \red{structured |
---|
424 | trace} are the same as their \textbf{Clight} counterparts |
---|
425 | \end{itemize} |
---|
426 | which links the behaviour and costs to the original program. |
---|
427 | } |
---|
428 | |
---|
429 | \begin{frame}[fragile] |
---|
430 | \frametitle{Structure in the compiler proof} |
---|
431 | |
---|
432 | \begin{center} |
---|
433 | \includegraphics[width=0.8\linewidth]{compiler.pdf} |
---|
434 | \end{center} |
---|
435 | |
---|
436 | %\onslide<1> |
---|
437 | %\green{Assembler} provides part of local cost analysis (CPP'12). |
---|
438 | |
---|
439 | %\onslide<2-4> |
---|
440 | Switch at RTLabs: |
---|
441 | \begin{itemize} |
---|
442 | \item from \red{measurable} subtrace of \alert{sound} and \alert{precise} |
---|
443 | labelling |
---|
444 | \item to \blue{structured trace} where they are embedded |
---|
445 | \end{itemize} |
---|
446 | |
---|
447 | %\onslide<3> |
---|
448 | %Changes \blue{syntactic} properties of labelling into \blue{semantic} |
---|
449 | %properties. |
---|
450 | |
---|
451 | %\onslide<4> |
---|
452 | Reason for choice: first language with explicit \alert{addresses}, implicit |
---|
453 | \alert{call handling}. |
---|
454 | |
---|
455 | \end{frame} |
---|
456 | |
---|
457 | \section{Correctness proofs} |
---|
458 | \subsection{Generic lifting result} |
---|
459 | |
---|
460 | \begin{frame}[fragile] |
---|
461 | \frametitle{Lifting measurable traces} |
---|
462 | |
---|
463 | For each pass find a target \alert{measurable} subtrace |
---|
464 | \alert{equivalent} to any source \alert{measurable} subtrace. |
---|
465 | |
---|
466 | \bigskip |
---|
467 | |
---|
468 | \onslide<2-> |
---|
469 | \begin{center} |
---|
470 | \includegraphics{meassim.pdf} |
---|
471 | \end{center} |
---|
472 | |
---|
473 | Split normal simulation proof: |
---|
474 | \begin{enumerate} |
---|
475 | \item each \blue{call} becomes a \blue{call} step plus zero or |
---|
476 | more \blue{normal} steps;\\ |
---|
477 | following cost labels should stay next to the call step |
---|
478 | \item each \blue{return} becomes a \blue{return} plus zero or |
---|
479 | more \blue{normal} steps |
---|
480 | \item \blue{cost} label steps are preserved |
---|
481 | \item other \blue{normal} steps become zero or more \blue{normal} steps |
---|
482 | \end{enumerate} |
---|
483 | |
---|
484 | \bigskip |
---|
485 | \onslide<3-> |
---|
486 | Preserves the defining termination property for \alert{measurable} subtraces. |
---|
487 | |
---|
488 | % \bigskip |
---|
489 | % \onslide<4-> |
---|
490 | % Due to time pressures, check \alert{soundness} and \alert{precision} of cost |
---|
491 | % labels at RTLabs. |
---|
492 | |
---|
493 | \end{frame} |
---|
494 | |
---|
495 | %\begin{frame}[fragile] |
---|
496 | %\frametitle{Structured trace simulation} |
---|
497 | % |
---|
498 | %Lift \alert{local} simulations to \alert{structured trace} simulations |
---|
499 | %similarly. |
---|
500 | % |
---|
501 | %\bigskip |
---|
502 | %\pause |
---|
503 | %\begin{itemize} |
---|
504 | %\item |
---|
505 | %Require local simulations for \alert{normal}, \alert{call} and \alert{return} |
---|
506 | %steps |
---|
507 | %\item allow traces to expand with extra \alert{normal} steps, |
---|
508 | %\item allow us to collapse some \alert{normal} steps |
---|
509 | % \begin{itemize} |
---|
510 | % \item but not collapse \blue{labelled} steps |
---|
511 | % % TODO: why? avoid larger change in structure |
---|
512 | % \item or change call structure |
---|
513 | % \end{itemize} |
---|
514 | %\end{itemize} |
---|
515 | % |
---|
516 | %\bigskip |
---|
517 | %Sufficient to calculate structured trace in target. |
---|
518 | %% TODO: pics |
---|
519 | % |
---|
520 | %\end{frame} |
---|
521 | % |
---|
522 | %\begin{frame}[fragile] |
---|
523 | %\frametitle{Structured trace local simulation example} |
---|
524 | % |
---|
525 | %For function call steps: |
---|
526 | %\begin{center} |
---|
527 | %\includegraphics[width=0.7\linewidth]{strcall.pdf} |
---|
528 | %\end{center} |
---|
529 | % |
---|
530 | %\begin{itemize} |
---|
531 | %\item May add extra steps before and after |
---|
532 | %\item Extra steps must not be call/return |
---|
533 | %\item Must call the same function |
---|
534 | %\item Cost label must stay at start of function |
---|
535 | %\end{itemize} |
---|
536 | % |
---|
537 | %\end{frame} |
---|
538 | |
---|
539 | \subsection{Simulations for compiler passes} |
---|
540 | |
---|
541 | %\frame{ |
---|
542 | %\frametitle{TODO: at least two slides on simulations} |
---|
543 | %} |
---|
544 | |
---|
545 | % TODO: perhaps much earlier for the pre-measurable bits? |
---|
546 | \frame{ |
---|
547 | \frametitle{Simulation between input and annotated code} |
---|
548 | |
---|
549 | Two stages provide the annotated version of input: |
---|
550 | |
---|
551 | \bigskip |
---|
552 | Switch removal |
---|
553 | \begin{itemize} |
---|
554 | \item \lstinline[language=C]'switch' statement control flow too subtle |
---|
555 | for simple labelling |
---|
556 | \item Replaces with \lstinline[language=C]'if ... then ... else' tree |
---|
557 | \item Tricky part of proof memory extension for extra variable |
---|
558 | \item Partial proof: validate approach, but not relevant to |
---|
559 | intensional properties |
---|
560 | \end{itemize} |
---|
561 | |
---|
562 | \bigskip |
---|
563 | Cost labelling |
---|
564 | \begin{itemize} |
---|
565 | \item For simulation don't care \emph{which} labels are added |
---|
566 | \item Just have to skip over extra cost label expressions and |
---|
567 | statements |
---|
568 | \item Complete simulation proof, simple |
---|
569 | \end{itemize} |
---|
570 | |
---|
571 | % TODO: consider whether to mention full simulation |
---|
572 | % termination-preserving proof? |
---|
573 | } |
---|
574 | |
---|
575 | \frame{ |
---|
576 | \frametitle{Front-end simulation results} |
---|
577 | Cast simplification |
---|
578 | \begin{itemize} |
---|
579 | \item Simplify expressions for 8-bit target |
---|
580 | \item Only expressions change --- statements are in lock-step |
---|
581 | \item Difficult part: we allow ill-typed \textbf{Clight} at this stage |
---|
582 | \item Simulation proofs complete |
---|
583 | \end{itemize} |
---|
584 | |
---|
585 | \textbf{Clight} to \textbf{Cminor} |
---|
586 | \begin{itemize} |
---|
587 | \item Stack allocation and control flow transformation |
---|
588 | \item Similar to \textbf{CompCert}, but produces \lstinline'goto' |
---|
589 | instead of \lstinline'loop' |
---|
590 | \item Expressions complete |
---|
591 | \item Prove a selection of statements, in particular \lstinline'while' |
---|
592 | \item Tricky: Large proof terms for invariant embedded in |
---|
593 | \textbf{Cminor} programs using dependent types;\\ |
---|
594 | generalise them away, but difficult under binders |
---|
595 | %TODO explain clearly |
---|
596 | \end{itemize} |
---|
597 | } |
---|
598 | \frame{ |
---|
599 | \frametitle{Front-end simulation results} |
---|
600 | \textbf{Cminor} to \textbf{RTLabs} |
---|
601 | \begin{itemize} |
---|
602 | \item Construction of control-flow graph |
---|
603 | \item Axiomatized simulations |
---|
604 | \item But do have invariants: |
---|
605 | \begin{itemize} |
---|
606 | \item Statement well-typed with respect to pseudo-register |
---|
607 | environment |
---|
608 | \item CFG complete |
---|
609 | \item Entry and exit nodes complete, unique |
---|
610 | \end{itemize} |
---|
611 | \item Translation function is \emph{total} as a result |
---|
612 | \end{itemize} |
---|
613 | } |
---|
614 | |
---|
615 | % TODO: sloganize: proved more about unusual bits |
---|
616 | |
---|
617 | \section{Checking cost labelling properties} |
---|
618 | |
---|
619 | \frame{ |
---|
620 | \frametitle{Checking cost labelling properties} |
---|
621 | |
---|
622 | Check cost labelling is \red{sound} and \blue{precise} at |
---|
623 | \textbf{RTLabs}. |
---|
624 | \begin{itemize} |
---|
625 | \item Shortcut; similar to translation validation |
---|
626 | \end{itemize} |
---|
627 | |
---|
628 | \medskip |
---|
629 | At \textbf{RTLabs} properties become |
---|
630 | \begin{description} |
---|
631 | \item[\red{soundness}] bound on number of instructions in CFG until label\\ |
---|
632 | label at start of every function |
---|
633 | \item[\blue{precision}] label after every branch |
---|
634 | \end{description} |
---|
635 | |
---|
636 | \medskip |
---|
637 | Bound is the hard part; the rest is a simple syntactic check. |
---|
638 | } |
---|
639 | |
---|
640 | \begin{frame}[fragile] |
---|
641 | \frametitle{Bound on number of instructions until label} |
---|
642 | |
---|
643 | \begin{center} |
---|
644 | \includegraphics<1>[width=.4\linewidth]{loop.pdf} |
---|
645 | \includegraphics<2>[width=.4\linewidth]{loop1.pdf} |
---|
646 | \includegraphics<3>[width=.4\linewidth]{loop2.pdf} |
---|
647 | \includegraphics<4>[width=.4\linewidth]{loop3.pdf} |
---|
648 | \includegraphics<5>[width=.4\linewidth]{loop4.pdf} |
---|
649 | \includegraphics<6>[width=.4\linewidth]{loopx.pdf} |
---|
650 | \end{center} |
---|
651 | |
---|
652 | \begin{itemize} |
---|
653 | \item Pick an arbitrary node in the CFG |
---|
654 | \item<2-> Follow successor instructions |
---|
655 | \item<4-> If we find a \alert{cost label} all the traced nodes have a bound\dots |
---|
656 | \item<5-> \dots so remove them and pick a new node, continue |
---|
657 | \item<6-> But if we find an \alert{unlabelled loop} the labelling is unsound, |
---|
658 | report an error |
---|
659 | \end{itemize} |
---|
660 | |
---|
661 | \end{frame} |
---|
662 | |
---|
663 | \frame{ |
---|
664 | \frametitle{Checking cost labelling properties} |
---|
665 | |
---|
666 | This compile-time check is |
---|
667 | \begin{itemize} |
---|
668 | \item[$-$] partial |
---|
669 | \item[$-$] extra work in compilation |
---|
670 | \item[$\mp$] not proving anything about compilation passes |
---|
671 | \item[$+$] less proof burden |
---|
672 | \end{itemize} |
---|
673 | |
---|
674 | \bigskip |
---|
675 | In a full proof would go from |
---|
676 | \begin{quote} |
---|
677 | cost labels at the head of loops in \textbf{Cminor} |
---|
678 | \end{quote} |
---|
679 | to |
---|
680 | \begin{quote} |
---|
681 | bound on instructions to cost label in \textbf{RTLabs} |
---|
682 | \end{quote} |
---|
683 | Showing existence of the bound alone likely to require at least as much |
---|
684 | proof effort as this check. |
---|
685 | |
---|
686 | } |
---|
687 | |
---|
688 | \section{Construction of structured traces} |
---|
689 | |
---|
690 | \frame{ |
---|
691 | \frametitle{Construction of structured traces} |
---|
692 | \begin{center} |
---|
693 | \includegraphics{strtraces.pdf} |
---|
694 | \end{center} |
---|
695 | \begin{enumerate} |
---|
696 | \item Extend sound and precise labelling to semantic states |
---|
697 | \item Prove they are preserved by steps of semantics |
---|
698 | \item Prove \textbf{RTLabs} semantics preserve the stack |
---|
699 | \item Use \alert{termination} proof from \alert{measurable} subtrace |
---|
700 | to create structure |
---|
701 | \item Proof obligations for cost labelling are discharged by semantic |
---|
702 | results above |
---|
703 | \end{enumerate} |
---|
704 | } |
---|
705 | |
---|
706 | \section{Whole compiler} |
---|
707 | |
---|
708 | \begin{frame}[fragile] |
---|
709 | \frametitle{Putting the proof together} |
---|
710 | |
---|
711 | \begin{center} |
---|
712 | \includegraphics[width=0.8\linewidth]{compiler.pdf} |
---|
713 | \end{center} |
---|
714 | |
---|
715 | \begin{itemize} |
---|
716 | \item `Clock' difference in Clight is sum of cost labels |
---|
717 | \item Observables, including trace of labels, is preserved to ASM |
---|
718 | \item Labelling at bottom level is sound and precise |
---|
719 | \item Sum of labels at ASM is equal to difference in real clock |
---|
720 | \end{itemize} |
---|
721 | |
---|
722 | \end{frame} |
---|
723 | |
---|
724 | \frame{ |
---|
725 | \frametitle{Conclusion} |
---|
726 | |
---|
727 | Sketched proof for formalised CerCo front-end |
---|
728 | |
---|
729 | \begin{itemize} |
---|
730 | \item Intensional proofs can be layered on top of extensional results |
---|
731 | \item Preserving call-structure key ingredient |
---|
732 | \item Compile-time cost labelling checks can reduce proof burden |
---|
733 | \item[$\star$] Don't need huge changes to extensional proof techniques |
---|
734 | \end{itemize} |
---|
735 | |
---|
736 | \pause |
---|
737 | Future: |
---|
738 | \begin{itemize} |
---|
739 | \item Expect results to generalise to more general labelling schemes |
---|
740 | \begin{itemize} |
---|
741 | \item hence more sophisticated targets |
---|
742 | \end{itemize} |
---|
743 | \item Other compiler correctness techniques |
---|
744 | \begin{itemize} |
---|
745 | \item Decompilation? |
---|
746 | \end{itemize} |
---|
747 | \end{itemize} |
---|
748 | |
---|
749 | } |
---|
750 | |
---|
751 | \end{document} |
---|
752 | |
---|
753 | % LocalWords: LFCS Matita CerCo intensional WCET toolchain CompCert Clight ASM |
---|
754 | % LocalWords: reexecutes subtrace RTLabs subtraces |
---|