1 | \documentclass[serif]{beamer} |
---|
2 | |
---|
3 | \usepackage[english]{babel} |
---|
4 | \usepackage{listings} |
---|
5 | \usepackage{microtype} |
---|
6 | |
---|
7 | \usetheme{Frankfurt} |
---|
8 | \logo{\includegraphics[height=1.0cm]{fetopen.png}} |
---|
9 | |
---|
10 | \author{Dominic Mulligan} |
---|
11 | \title{CerCo Work Package 4} |
---|
12 | \date{CerCo project review meeting\\March 2012} |
---|
13 | |
---|
14 | \lstdefinelanguage{matita-ocaml} |
---|
15 | {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try}, |
---|
16 | morekeywords={[2]whd,normalize,elim,cases,destruct}, |
---|
17 | morekeywords={[3]type,of}, |
---|
18 | mathescape=true, |
---|
19 | } |
---|
20 | |
---|
21 | \lstset{language=matita-ocaml,basicstyle=\scriptsize\tt,columns=flexible,breaklines=false, |
---|
22 | keywordstyle=\color{red}\bfseries, |
---|
23 | keywordstyle=[2]\color{blue}, |
---|
24 | keywordstyle=[3]\color{blue}\bfseries, |
---|
25 | commentstyle=\color{green}, |
---|
26 | stringstyle=\color{blue}, |
---|
27 | showspaces=false,showstringspaces=false} |
---|
28 | |
---|
29 | \begin{document} |
---|
30 | |
---|
31 | \begin{frame} |
---|
32 | \maketitle |
---|
33 | \end{frame} |
---|
34 | |
---|
35 | \begin{frame} |
---|
36 | \frametitle{Summary I} |
---|
37 | Relevant tasks: T4.2 and T4.3 (from the CerCo Contract): |
---|
38 | \begin{quotation} |
---|
39 | \textbf{Task 4.2} |
---|
40 | Functional encoding in the Calculus of Inductive Construction (indicative effort: UNIBO: 8; UDP: 2; UEDIN: 0) |
---|
41 | \end{quotation} |
---|
42 | |
---|
43 | \begin{quotation} |
---|
44 | \textbf{Task 4.3} |
---|
45 | Formal semantics of intermediate languages (indicative effort: UNIBO: 4; UDP: 0; UEDIN: 0) |
---|
46 | \end{quotation} |
---|
47 | \end{frame} |
---|
48 | |
---|
49 | \begin{frame} |
---|
50 | \frametitle{Summary II} |
---|
51 | Task 4.2 in detail (from the CerCo Contract): |
---|
52 | \begin{quotation} |
---|
53 | \textbf{CIC encoding: Back-end}: |
---|
54 | Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler. |
---|
55 | This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2. |
---|
56 | A first validation of the design principles and implementation choices for the Untrusted Cost-annotating OCaml Compiler D2.2 is achieved and reported in the deliverable, possibly triggering updates of the Untrusted Cost-annotating OCaml Compiler sources. |
---|
57 | \end{quotation} |
---|
58 | \end{frame} |
---|
59 | |
---|
60 | \begin{frame} |
---|
61 | \frametitle{Summary III} |
---|
62 | Task 4.3 in detail (from the CerCo contract): |
---|
63 | \begin{quotation} |
---|
64 | \textbf{Executable Formal Semantics of back-end intermediate languages}: |
---|
65 | This prototype is the formal counterpart of deliverable D2.1 for the back end side of the compiler and validates it. |
---|
66 | \end{quotation} |
---|
67 | \end{frame} |
---|
68 | |
---|
69 | \begin{frame} |
---|
70 | \frametitle{Backend intermediate languages I} |
---|
71 | \begin{itemize} |
---|
72 | \item |
---|
73 | O'Caml prototype has five backend intermediate languages: RTLabs, RTL, ERTL, LTL, LIN |
---|
74 | \item |
---|
75 | RTLabs is the `frontier' between backend and frontend, last abstract language |
---|
76 | \item |
---|
77 | RTLabs, RTL, ERTL and LTL are graph based languages: functions represented as graphs of statements, with entry and exit points |
---|
78 | \item |
---|
79 | LIN is a linearised form of LTL, and is the exit point of the compiler's backend |
---|
80 | \item |
---|
81 | In contrast to frontend, backend is very different to CompCert's |
---|
82 | \end{itemize} |
---|
83 | \end{frame} |
---|
84 | |
---|
85 | \begin{frame} |
---|
86 | \frametitle{Backend intermediate languages II} |
---|
87 | \begin{small} |
---|
88 | \begin{tabbing} |
---|
89 | \quad \=\,\quad \= \\ |
---|
90 | \textsf{RTLabs}\\ |
---|
91 | \> $\downarrow$ \> copy propagation (an endo-transformation, yet to be ported) \\ |
---|
92 | \> $\downarrow$ \> instruction selection\\ |
---|
93 | \> $\downarrow$ \> change of memory models in compiler\\ |
---|
94 | \textsf{RTL}\\ |
---|
95 | \> $\downarrow$ \> constant propagation (an endo-transformation, yet to be ported) \\ |
---|
96 | \> $\downarrow$ \> calling convention made explicit \\ |
---|
97 | \> $\downarrow$ \> layout of activation records \\ |
---|
98 | \textsf{ERTL}\\ |
---|
99 | \> $\downarrow$ \> register allocation and spilling\\ |
---|
100 | \> $\downarrow$ \> dead code elimination\\ |
---|
101 | \textsf{LTL}\\ |
---|
102 | \> $\downarrow$ \> function linearisation\\ |
---|
103 | \> $\downarrow$ \> branch compression (an endo-transformation) \\ |
---|
104 | \textsf{LIN}\\ |
---|
105 | \> $\downarrow$ \> relabeling\\ |
---|
106 | \end{tabbing} |
---|
107 | \end{small} |
---|
108 | \end{frame} |
---|
109 | |
---|
110 | \begin{frame} |
---|
111 | \frametitle{\texttt{Joint}: a new approach I} |
---|
112 | \begin{itemize} |
---|
113 | \item |
---|
114 | Consecutive languages in backend must be similar |
---|
115 | \item |
---|
116 | Transformations between languages translate away some small specific set of features |
---|
117 | \item |
---|
118 | But looking at O'Caml code, not clear precisely what differences between languages are, as code is repeated |
---|
119 | \item |
---|
120 | Not clear if translation passes can commute, for instance |
---|
121 | \item |
---|
122 | CerCo passes are in a different order to CompCert (calling convention and register allocation done in different places) |
---|
123 | \item |
---|
124 | Instruction selection done early: changing subset of instructions used would require instructions to be duplicated everywhere in backend |
---|
125 | \end{itemize} |
---|
126 | \end{frame} |
---|
127 | |
---|
128 | \begin{frame} |
---|
129 | \frametitle{\texttt{Joint}: a new approach II} |
---|
130 | \begin{itemize} |
---|
131 | \item |
---|
132 | Idea: all of these languages are just instances of a single language |
---|
133 | \item |
---|
134 | This language \texttt{Joint} is parameterised by a type of registers to be used in instructions, and so forth |
---|
135 | \item |
---|
136 | Each language after RTLabs is now just defined as the \texttt{Joint} language instantiated with some concrete types |
---|
137 | \item |
---|
138 | Similarly for semantics: common definitions that take e.g. type representing program counters as parameters |
---|
139 | \end{itemize} |
---|
140 | \end{frame} |
---|
141 | |
---|
142 | \begin{frame}[fragile] |
---|
143 | \frametitle{\texttt{Joint}: a new approach III} |
---|
144 | \texttt{Joint} instructions allow us to embed language-specific instructions: |
---|
145 | \begin{lstlisting} |
---|
146 | inductive joint_instruction (p: params__) (globals: list ident): Type[0] := |
---|
147 | | COMMENT: String $\rightarrow$ joint_instruction p globals |
---|
148 | | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals |
---|
149 | ... |
---|
150 | | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals |
---|
151 | | extension: extend_statements p $\rightarrow$ joint_instruction p globals. |
---|
152 | \end{lstlisting} |
---|
153 | |
---|
154 | \begin{lstlisting} |
---|
155 | inductive ertl_statement_extension: Type[0] := |
---|
156 | | ertl_st_ext_new_frame: ertl_statement_extension |
---|
157 | | ertl_st_ext_del_frame: ertl_statement_extension |
---|
158 | | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension. |
---|
159 | \end{lstlisting} |
---|
160 | \end{frame} |
---|
161 | |
---|
162 | \begin{frame}[fragile] |
---|
163 | \frametitle{\texttt{Joint}: a new approach IV} |
---|
164 | For example, the definition of the \texttt{ERTL} language is now: |
---|
165 | \begin{lstlisting} |
---|
166 | inductive move_registers: Type[0] := |
---|
167 | | pseudo: register $\rightarrow$ move_registers |
---|
168 | | hardware: Register $\rightarrow$ move_registers. |
---|
169 | |
---|
170 | definition ertl_params__: params__ := |
---|
171 | mk_params__ register register register register |
---|
172 | (move_registers $\times$ move_registers) |
---|
173 | register nat unit ertl_statement_extension. |
---|
174 | definition ertl_params_: params_ := |
---|
175 | graph_params_ ertl_params__. |
---|
176 | definition ertl_params0: params0 := |
---|
177 | mk_params0 ertl_params__ (list register) nat. |
---|
178 | definition ertl_params1: params1 := |
---|
179 | rtl_ertl_params1 ertl_params0. |
---|
180 | definition ertl_params: $\forall$globals. params globals ≝ |
---|
181 | rtl_ertl_params ertl_params0. |
---|
182 | \end{lstlisting} |
---|
183 | \end{frame} |
---|
184 | |
---|
185 | \begin{frame}[fragile] |
---|
186 | \frametitle{Instruction embedding in \texttt{Joint}} |
---|
187 | \begin{lstlisting} |
---|
188 | inductive joint_instruction (p:params__) (globals: list ident): Type[0] := |
---|
189 | ... |
---|
190 | | POP: acc_a_reg p $\rightarrow$ joint_instruction p globals |
---|
191 | | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals |
---|
192 | ... |
---|
193 | \end{lstlisting} |
---|
194 | \begin{itemize} |
---|
195 | \item |
---|
196 | RTLabs (not a \texttt{Joint} language) to RTL is where instruction selection takes place |
---|
197 | \item |
---|
198 | Instructions from the MCS-51 instruction set embedded in \texttt{Joint} syntax |
---|
199 | \end{itemize} |
---|
200 | \end{frame} |
---|
201 | |
---|
202 | \begin{frame} |
---|
203 | \frametitle{\texttt{Joint}: advantages} |
---|
204 | \begin{itemize} |
---|
205 | \item |
---|
206 | Why use \texttt{Joint}, as opposed to defining all languages individually? |
---|
207 | \item |
---|
208 | Reduces repeated code (fewer bugs, or places to change) |
---|
209 | \item |
---|
210 | Unify some proofs, making correctness proof easier |
---|
211 | \item |
---|
212 | Easier to add new intermediate languages as needed |
---|
213 | \item |
---|
214 | Easier to see relationship between consecutive languages at a glance |
---|
215 | \item |
---|
216 | Simplifies instruction selection (i.e. porting to a new platform, or expanding subset of instructions emitted) |
---|
217 | \item |
---|
218 | We can investigate which translation passes commute much more easily |
---|
219 | \end{itemize} |
---|
220 | \end{frame} |
---|
221 | |
---|
222 | \begin{frame} |
---|
223 | \frametitle{Semantics of \texttt{Joint} I} |
---|
224 | \begin{itemize} |
---|
225 | \item |
---|
226 | As mentioned, use of \texttt{Joint} also unifies semantics of these languages |
---|
227 | \item |
---|
228 | We use several sets of records, which represent the state that a program is in |
---|
229 | \item |
---|
230 | These records are parametric in representations for e.g. frames |
---|
231 | \end{itemize} |
---|
232 | \end{frame} |
---|
233 | |
---|
234 | \begin{frame}[fragile] |
---|
235 | \frametitle{Semantics of \texttt{Joint} II} |
---|
236 | \begin{lstlisting} |
---|
237 | record more_sem_params (p:params_): Type[1] := |
---|
238 | { |
---|
239 | framesT: Type[0]; |
---|
240 | empty_framesT: framesT; |
---|
241 | regsT: Type[0]; |
---|
242 | ... |
---|
243 | acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; |
---|
244 | acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval; |
---|
245 | ... |
---|
246 | pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT |
---|
247 | }. |
---|
248 | \end{lstlisting} |
---|
249 | \end{frame} |
---|
250 | |
---|
251 | \begin{frame}[fragile] |
---|
252 | \frametitle{Semantics of \texttt{Joint} III} |
---|
253 | Generic functions: |
---|
254 | \begin{lstlisting} |
---|
255 | definition set_carry: $\forall$p. beval $\rightarrow$ state p $\rightarrow$ state p := |
---|
256 | $\lambda$p, carry, st. |
---|
257 | mk_state $\ldots$ (st_frms $\ldots$ st) (pc $\ldots$ st) |
---|
258 | (sp $\ldots$ st) (isp $\ldots$ st) carry (regs $\ldots$ st) (m $\ldots$ st). |
---|
259 | \end{lstlisting} |
---|
260 | \begin{lstlisting} |
---|
261 | definition goto: $\forall$globals. $\forall$p:sem_params1 globals. genv globals p $\rightarrow$ |
---|
262 | label $\rightarrow$ state p $\rightarrow$ res (state p) := |
---|
263 | $\lambda$globals, p, ge, l, st. |
---|
264 | do oldpc $\leftarrow$ pointer_of_address (pc $\ldots$ st) ; |
---|
265 | do newpc $\leftarrow$ address_of_label $\ldots$ ge oldpc l ; |
---|
266 | OK $\ldots$ (set_pc $\ldots$ newpc st). |
---|
267 | \end{lstlisting} |
---|
268 | \end{frame} |
---|
269 | |
---|
270 | \begin{frame}[fragile] |
---|
271 | \frametitle{Semantics of \texttt{Joint} IV} |
---|
272 | Individual semantics obtained by instantiating records to concrete types (ERTL here): |
---|
273 | \begin{lstlisting} |
---|
274 | definition ertl_more_sem_params: more_sem_params ertl_params_ := |
---|
275 | mk_more_sem_params ertl_params_ |
---|
276 | (list (register_env beval)) [] ((register_env beval) $\times$ hw_register_env) |
---|
277 | ($\lambda$sp. $\langle$empty_map $\ldots$,init_hw_register_env sp$\rangle$) 0 it |
---|
278 | ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store |
---|
279 | ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve |
---|
280 | ($\lambda$locals,dest_src. |
---|
281 | do v $\leftarrow$ |
---|
282 | match \snd dest_src with |
---|
283 | [ pseudo reg $\Rightarrow$ ps_reg_retrieve locals reg |
---|
284 | | hardware reg $\Rightarrow$ hw_reg_retrieve locals reg |
---|
285 | ]; |
---|
286 | match \fst dest_src with |
---|
287 | [ pseudo reg $\Rightarrow$ ps_reg_store reg v locals |
---|
288 | | hardware reg $\Rightarrow$ hw_reg_store reg v locals |
---|
289 | ]). |
---|
290 | \end{lstlisting} |
---|
291 | \end{frame} |
---|
292 | |
---|
293 | \begin{frame}[fragile] |
---|
294 | \frametitle{Semantics of \texttt{Joint} V} |
---|
295 | For languages with `extensions', we provide a semantics: |
---|
296 | \begin{lstlisting} |
---|
297 | definition ertl_exec_extended: |
---|
298 | $\forall$globals. genv globals (ertl_params globals) $\rightarrow$ |
---|
299 | ertl_statement_extension $\rightarrow$ label $\rightarrow$ state ertl_sem_params $\rightarrow$ |
---|
300 | IO io_out io_in (trace $\times$ (state ertl_sem_params)) := |
---|
301 | $\lambda$globals, ge, stm, l, st. |
---|
302 | match stm with |
---|
303 | [ ertl_st_ext_new_frame $\Rightarrow$ |
---|
304 | ! v $\leftarrow$ framesize globals $\ldots$ ge st; |
---|
305 | let sp := get_hwsp st in |
---|
306 | ! newsp $\leftarrow$ addr_sub sp v; |
---|
307 | let st := set_hwsp newsp st in |
---|
308 | ! st $\leftarrow$ next $\ldots$ (ertl_sem_params1 globals) l st ; |
---|
309 | ret ? $\langle$E0, st$\rangle$ |
---|
310 | | ... |
---|
311 | ]. |
---|
312 | \end{lstlisting} |
---|
313 | \end{frame} |
---|
314 | |
---|
315 | \begin{frame} |
---|
316 | \frametitle{\texttt{Joint} summary} |
---|
317 | \begin{itemize} |
---|
318 | \item |
---|
319 | Using \texttt{Joint} we get a modular semantics |
---|
320 | \item |
---|
321 | `Common' semantics are shared amongst all languages |
---|
322 | \item |
---|
323 | Specific languages are responsible for providing the semantics of the extensions that they provide |
---|
324 | \item |
---|
325 | Show differences (and similarities) between languages clearly |
---|
326 | \item |
---|
327 | Reduces proofs |
---|
328 | \item |
---|
329 | Easy to add new languages |
---|
330 | \end{itemize} |
---|
331 | \end{frame} |
---|
332 | |
---|
333 | \begin{frame} |
---|
334 | \frametitle{A new intermediate language} |
---|
335 | \begin{itemize} |
---|
336 | \item |
---|
337 | Matita backend includes a new intermediate language: RTLntc |
---|
338 | \item |
---|
339 | Sits between RTL and ERTL |
---|
340 | \item |
---|
341 | RTLntc is the RTL language where all tailcalls have been eliminated |
---|
342 | \item |
---|
343 | This language is `implicit' in the O'Caml compiler |
---|
344 | \item |
---|
345 | There, the RTL to ERTL transformation eliminates tailcalls as part of translation |
---|
346 | \item |
---|
347 | But including an extra, explicit intermediate language is `almost free' using the \texttt{Joint} language approach |
---|
348 | \end{itemize} |
---|
349 | \end{frame} |
---|
350 | |
---|
351 | \begin{frame} |
---|
352 | \frametitle{The LTL to LIN transform I} |
---|
353 | \begin{itemize} |
---|
354 | \item |
---|
355 | \texttt{Joint} clearly separates fetching from program execution |
---|
356 | \item |
---|
357 | We can vary how one works whilst fixing the other |
---|
358 | \item |
---|
359 | Linearisation is moving from fetching from a graph-based language to fetching from a list-based program representation |
---|
360 | \item |
---|
361 | The order of transformations in O'Caml prototype is fixed |
---|
362 | \item |
---|
363 | Linearisation takes place at a fixed place, in the translation between LTL and LIN |
---|
364 | \item |
---|
365 | The Matita compiler is different: linearisation is a generic process |
---|
366 | \item |
---|
367 | Any graph-based language can now be linearised |
---|
368 | \end{itemize} |
---|
369 | \end{frame} |
---|
370 | |
---|
371 | \begin{frame} |
---|
372 | \frametitle{The LTL to LIN transform II} |
---|
373 | \begin{itemize} |
---|
374 | \item |
---|
375 | The CompCert backend linearises much sooner than CerCo's |
---|
376 | \item |
---|
377 | We can now experiment with linearising much earlier |
---|
378 | \item |
---|
379 | Many transformations and optimisations can work fine on a linearised form |
---|
380 | \item |
---|
381 | The only place in the backend that requires a graph-based language is in the ERTL pass, where we do a dataflow analysis |
---|
382 | \end{itemize} |
---|
383 | \end{frame} |
---|
384 | |
---|
385 | \begin{frame} |
---|
386 | \frametitle{`Free time'} |
---|
387 | \begin{itemize} |
---|
388 | \item |
---|
389 | We had six months of time which is not reported on in any deliverable |
---|
390 | \item |
---|
391 | We invested this time working on: |
---|
392 | \begin{itemize} |
---|
393 | \item |
---|
394 | The global proof sketch |
---|
395 | \item |
---|
396 | The setup of `proof infrastructure', common definitions, lemmas, invariants etc. required for main body of proof |
---|
397 | \item |
---|
398 | The proof of correctness for the assembler |
---|
399 | \item |
---|
400 | A notion of `structured traces', used throughout the compiler formalisation, as a means of eventually proving that the compiler correctly preserves costs |
---|
401 | \item |
---|
402 | Structured traces were defined in collaboration with the team at UEDIN |
---|
403 | \end{itemize} |
---|
404 | \item |
---|
405 | I now explain in more detail how this time was used |
---|
406 | \end{itemize} |
---|
407 | \end{frame} |
---|
408 | |
---|
409 | \begin{frame} |
---|
410 | \frametitle{Assembler} |
---|
411 | \begin{itemize} |
---|
412 | \item |
---|
413 | After LIN, compiler spits out assembly language for MCS-51 |
---|
414 | \item |
---|
415 | Assembler has pseudoinstructions similar to many commercial assembly languages |
---|
416 | \item |
---|
417 | For instance, instead of computed jumps (e.g. \texttt{SJMP} to a specific address), compiler can simply spit out a generic jump instruction to a label |
---|
418 | \item |
---|
419 | Simplifies the compiler, at the expense of introducing more proof obligations |
---|
420 | \end{itemize} |
---|
421 | \end{frame} |
---|
422 | |
---|
423 | \begin{frame} |
---|
424 | \frametitle{A problem: jump expansion} |
---|
425 | \begin{itemize} |
---|
426 | \item |
---|
427 | `Jump expansion' is our name for the standard `branch displacement' problem |
---|
428 | \item |
---|
429 | Given a pseudojump to a label $l$, how best can this be expanded into an assembly instruction \texttt{SJMP}, \texttt{AJMP} or \texttt{LJMP} to a concrete address? |
---|
430 | \item |
---|
431 | Problem also applies to conditional jumps |
---|
432 | \item |
---|
433 | Problem especially relevant for MCS-51 as it has a small code memory, therefore aggressive expansion of jumps into smallest possible concrete jump instruction needed |
---|
434 | \item |
---|
435 | But a known hard problem (NP-complete depending on architecture), and easy to imagine knotty configurations where size of jumps are interdependent |
---|
436 | \end{itemize} |
---|
437 | \end{frame} |
---|
438 | |
---|
439 | \begin{frame} |
---|
440 | \frametitle{Jump expansion I} |
---|
441 | \begin{itemize} |
---|
442 | \item |
---|
443 | We employed the following tactic: split the decision over how any particular pseudoinstruction is expanded from pseudoinstruction expansion |
---|
444 | \item |
---|
445 | Call the decision maker a `policy' |
---|
446 | \item |
---|
447 | We started the proof of correctness for the assembler based on the premise that a correct policy exists |
---|
448 | \item |
---|
449 | Further, we know that the assembler only fails to assemble a program if a good policy does not exist (a side-effect of using dependent types) |
---|
450 | \item |
---|
451 | A bad policy is a function that expands a given pseudojump into a concrete jump instruction that is `too small' for the distance to be jumped, or makes the program consume too much memory |
---|
452 | \end{itemize} |
---|
453 | \end{frame} |
---|
454 | |
---|
455 | \begin{frame} |
---|
456 | \frametitle{Jump expansion II} |
---|
457 | \begin{itemize} |
---|
458 | \item |
---|
459 | Boender at UNIBO has been working on a verified implementation of a good jump expansion policy for the MCS-51 |
---|
460 | \item |
---|
461 | The strategy initially translates all pseudojumps as \texttt{SJMP} and then increases their size if necessary |
---|
462 | \item |
---|
463 | Termination of the procedure is proved, as well as a safety property, stating that jumps are not expanded into jumps that are too long |
---|
464 | \item |
---|
465 | His strategy is not optimal (though the computed solution is optimal for the strategy employed) |
---|
466 | \item |
---|
467 | Boender's work is the first formal treatment of the `jump expansion problem' |
---|
468 | \end{itemize} |
---|
469 | \end{frame} |
---|
470 | |
---|
471 | \begin{frame} |
---|
472 | \frametitle{Assembler correctness proof} |
---|
473 | \begin{itemize} |
---|
474 | \item |
---|
475 | Assuming the existence of a good jump expansion property, we completed about 75\% of the correctness proof for the assembler |
---|
476 | \item |
---|
477 | Boender's work has just been completed (modulo a few missing lemmas) |
---|
478 | \item |
---|
479 | We abandoned the main assembler proof to start work on other tasks (and wait for Boender to finish) |
---|
480 | \item |
---|
481 | However, we intend to return to the proof, and publishing an account of the work (possibly) as a journal paper |
---|
482 | \end{itemize} |
---|
483 | \end{frame} |
---|
484 | |
---|
485 | \begin{frame}[fragile] |
---|
486 | \frametitle{Who pays? I} |
---|
487 | \begin{lstlisting} |
---|
488 | int main(int argc, char** argv) { |
---|
489 | label1: |
---|
490 | ... |
---|
491 | some_function(); |
---|
492 | label2: |
---|
493 | ... |
---|
494 | } |
---|
495 | \end{lstlisting} |
---|
496 | \begin{itemize} |
---|
497 | \item |
---|
498 | Question: where do we put cost labels to capture execution costs? |
---|
499 | \item |
---|
500 | Proof obligations complicated by panoply of labels |
---|
501 | \item |
---|
502 | Doesn't work well with \texttt{g(h() + 2 + f())} |
---|
503 | \item |
---|
504 | To prove accuracy we need to show \texttt{some\_function()} terminates! |
---|
505 | \item |
---|
506 | \texttt{some\_function()} may not return correctly |
---|
507 | \end{itemize} |
---|
508 | \end{frame} |
---|
509 | |
---|
510 | \begin{frame} |
---|
511 | \frametitle{Who pays? II} |
---|
512 | \begin{itemize} |
---|
513 | \item |
---|
514 | Solution: omit \texttt{label2} and just keep \texttt{label1} |
---|
515 | \item |
---|
516 | We pay for everything `up front' when entering a function |
---|
517 | \item |
---|
518 | No need to prove \texttt{some\_function()} terminates |
---|
519 | \item |
---|
520 | But now execution of functions in CerCo takes a particular form |
---|
521 | \item |
---|
522 | Functions begin with a label, call other functions that begin with a label, eventually return, but \emph{return} to the correct place |
---|
523 | \item |
---|
524 | `Recursive structure' |
---|
525 | \end{itemize} |
---|
526 | \end{frame} |
---|
527 | |
---|
528 | \begin{frame} |
---|
529 | \frametitle{Structured traces I} |
---|
530 | \begin{itemize} |
---|
531 | \item |
---|
532 | We introduced a notion of `structured traces' |
---|
533 | \item |
---|
534 | These are intended to statically capture the (good) execution traces of a program |
---|
535 | \item |
---|
536 | That is, functions return to where they ought |
---|
537 | \item |
---|
538 | Come in two variants: inductive and coinductive |
---|
539 | \item |
---|
540 | Inductive is meant to capture program execution traces that eventually halt |
---|
541 | \item |
---|
542 | Coinductive is meant to capture program execution traces that diverge |
---|
543 | \end{itemize} |
---|
544 | \end{frame} |
---|
545 | |
---|
546 | \begin{frame} |
---|
547 | \frametitle{Structured traces II} |
---|
548 | \begin{itemize} |
---|
549 | \item |
---|
550 | Here, I focus on the inductive variety |
---|
551 | \item |
---|
552 | Used the most (for now) in the backend |
---|
553 | \item |
---|
554 | In particular, used in the proof that static and dynamic cost computations coincide |
---|
555 | \item |
---|
556 | This will be explained later |
---|
557 | \end{itemize} |
---|
558 | \end{frame} |
---|
559 | |
---|
560 | \begin{frame} |
---|
561 | \frametitle{Structured traces III} |
---|
562 | \begin{itemize} |
---|
563 | \item |
---|
564 | Central insight is that program execution is always in the body of some function (from \texttt{main} onwards) |
---|
565 | \item |
---|
566 | A well formed program must have labels appearing at certain spots |
---|
567 | \item |
---|
568 | Similarly, the final instruction executed when executing a function must be a \texttt{RET} |
---|
569 | \item |
---|
570 | Execution must then continue in body of calling function, at correct place |
---|
571 | \item |
---|
572 | These invariants, and others, are crystalised in the specific syntactic form of a structured trace |
---|
573 | \item |
---|
574 | Some examples... |
---|
575 | \end{itemize} |
---|
576 | \end{frame} |
---|
577 | |
---|
578 | \begin{frame}[fragile] |
---|
579 | \frametitle{Structured trace examples I} |
---|
580 | Traces end with a return being executed, or not: |
---|
581 | \begin{lstlisting} |
---|
582 | inductive trace_ends_with_ret: Type[0] := |
---|
583 | | ends_with_ret: trace_ends_with_ret |
---|
584 | | doesnt_end_with_ret: trace_ends_with_ret. |
---|
585 | \end{lstlisting} |
---|
586 | A trace starting with a label and ending with a return: |
---|
587 | \begin{lstlisting} |
---|
588 | inductive trace_label_return (S: abstract_status): S $\rightarrow$ S $\rightarrow$ Type[0] := |
---|
589 | | tlr_base: |
---|
590 | $\forall$status_before: S. |
---|
591 | $\forall$status_after: S. |
---|
592 | trace_label_label S ends_with_ret status_before status_after $\rightarrow$ |
---|
593 | trace_label_return S status_before status_after |
---|
594 | ... |
---|
595 | \end{lstlisting} |
---|
596 | \end{frame} |
---|
597 | |
---|
598 | \begin{frame}[fragile] |
---|
599 | \frametitle{Structured trace examples II} |
---|
600 | A trace starting and ending with a cost label: |
---|
601 | \begin{lstlisting} |
---|
602 | ... |
---|
603 | with trace_label_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] := |
---|
604 | | tll_base: |
---|
605 | $\forall$ends_flag: trace_ends_with_ret. |
---|
606 | $\forall$start_status: S. |
---|
607 | $\forall$end_status: S. |
---|
608 | trace_any_label S ends_flag start_status end_status $\rightarrow$ |
---|
609 | as_costed S start_status $\rightarrow$ |
---|
610 | trace_label_label S ends_flag start_status end_status |
---|
611 | ... |
---|
612 | \end{lstlisting} |
---|
613 | \end{frame} |
---|
614 | |
---|
615 | \begin{frame}[fragile] |
---|
616 | \frametitle{Structured trace examples III} |
---|
617 | A call followed by a label on return: |
---|
618 | \begin{lstlisting} |
---|
619 | ... |
---|
620 | with trace_any_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] := |
---|
621 | ... |
---|
622 | | tal_base_call: |
---|
623 | $\forall$status_pre_fun_call: S. |
---|
624 | $\forall$status_start_fun_call: S. |
---|
625 | $\forall$status_final: S. |
---|
626 | as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$ |
---|
627 | $\forall$H:as_classifier S status_pre_fun_call cl_call. |
---|
628 | as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final $\rightarrow$ |
---|
629 | trace_label_return S status_start_fun_call status_final $\rightarrow$ |
---|
630 | as_costed S status_final $\rightarrow$ |
---|
631 | trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final |
---|
632 | ... |
---|
633 | \end{lstlisting} |
---|
634 | \end{frame} |
---|
635 | |
---|
636 | \begin{frame}[fragile] |
---|
637 | \frametitle{Structured trace examples IV} |
---|
638 | A call followed by a non-empty trace: |
---|
639 | \begin{lstlisting} |
---|
640 | ... |
---|
641 | | tal_step_call: |
---|
642 | $\forall$end_flag: trace_ends_with_ret. |
---|
643 | $\forall$status_pre_fun_call: S. |
---|
644 | $\forall$status_start_fun_call: S. |
---|
645 | $\forall$status_after_fun_call: S. |
---|
646 | $\forall$status_final: S. |
---|
647 | as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$ |
---|
648 | $\forall$H:as_classifier S status_pre_fun_call cl_call. |
---|
649 | as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call $\rightarrow$ |
---|
650 | trace_label_return S status_start_fun_call status_after_fun_call $\rightarrow$ |
---|
651 | ¬ as_costed S status_after_fun_call $\rightarrow$ |
---|
652 | trace_any_label S end_flag status_after_fun_call status_final $\rightarrow$ |
---|
653 | trace_any_label S end_flag status_pre_fun_call status_final |
---|
654 | ... |
---|
655 | \end{lstlisting} |
---|
656 | \end{frame} |
---|
657 | |
---|
658 | \begin{frame} |
---|
659 | \frametitle{Static and dynamic costs I} |
---|
660 | \begin{itemize} |
---|
661 | \item |
---|
662 | Given a structured trace, we can compute its associated cost |
---|
663 | \item |
---|
664 | This is the \emph{static} cost of a program execution |
---|
665 | \item |
---|
666 | Similarly, given a program counter and a code memory (corresponding to the trace), we can compute a \emph{dynamic cost} of a simple block |
---|
667 | \item |
---|
668 | Do this by repeatedly fetching, obtaining the next instruction, and a new program counter |
---|
669 | \item |
---|
670 | This requires some predicates defining what a `good program' and what a `good program counter' are |
---|
671 | \end{itemize} |
---|
672 | \end{frame} |
---|
673 | |
---|
674 | \begin{frame} |
---|
675 | \frametitle{Static and dynamic costs II} |
---|
676 | \begin{itemize} |
---|
677 | \item |
---|
678 | We aim to prove that the dynamic and static cost calculations coincide |
---|
679 | \item |
---|
680 | This would imply that the static cost computation is correct |
---|
681 | \item |
---|
682 | This proof is surprisingly tricky to complete (about 3 man months of work so far) |
---|
683 | \item |
---|
684 | Is now about 95\% complete |
---|
685 | \end{itemize} |
---|
686 | \end{frame} |
---|
687 | |
---|
688 | \begin{frame} |
---|
689 | \frametitle{Changes ported to O'Caml prototype} |
---|
690 | \begin{itemize} |
---|
691 | \item |
---|
692 | Bug fixes spotted in the formalisation so far have been merged back into the O'Caml compiler |
---|
693 | \item |
---|
694 | Larger changes like the \texttt{Joint} machinery have so far not |
---|
695 | \item |
---|
696 | It is unclear whether they will be |
---|
697 | \item |
---|
698 | Just a generalisation of what is already there |
---|
699 | \item |
---|
700 | Supposed to make formalisation easier |
---|
701 | \item |
---|
702 | Further, we want to ensure that the untrusted compiler is as correct as possible, for experiments in e.g. Frama-C |
---|
703 | \item |
---|
704 | Porting a large change to the untrusted compiler would jeopardise these experiments |
---|
705 | \end{itemize} |
---|
706 | \end{frame} |
---|
707 | |
---|
708 | \begin{frame} |
---|
709 | \frametitle{Improvements in Matita} |
---|
710 | \begin{itemize} |
---|
711 | \item |
---|
712 | Part of the motivation for using Matita was for CerCo to act a `stress test' |
---|
713 | \item |
---|
714 | The proofs talked about in this talk have done this |
---|
715 | \item |
---|
716 | Many improvements to Matita have been made since the last project meeting |
---|
717 | \item |
---|
718 | These include major speed-ups of e.g. printing large goals, bug fixes, the porting of CerCo code to standard library, and more options for passing to tactics |
---|
719 | \end{itemize} |
---|
720 | \end{frame} |
---|
721 | |
---|
722 | \begin{frame} |
---|
723 | \frametitle{The next period} |
---|
724 | UNIBO has following pool of remaining manpower (postdocs): |
---|
725 | \begin{center} |
---|
726 | \begin{tabular}{ll} |
---|
727 | Person & Man months remaining \\ |
---|
728 | \hline |
---|
729 | Boender & 14 months \\ |
---|
730 | Mulligan & 6 months \\ |
---|
731 | Tranquilli & 10 months \\ |
---|
732 | \end{tabular} |
---|
733 | \end{center} |
---|
734 | \begin{itemize} |
---|
735 | \item |
---|
736 | Boender finishing assembler correctness proof |
---|
737 | \item |
---|
738 | Mulligan proofs of correctness for 1 intermediate language |
---|
739 | \item |
---|
740 | Tranquilli proofs of correctness for 2 intermediate languages |
---|
741 | \item |
---|
742 | Sacerdoti Coen `floating' |
---|
743 | \item |
---|
744 | Believe we have enough manpower to complete backend |
---|
745 | \end{itemize} |
---|
746 | \end{frame} |
---|
747 | |
---|
748 | \begin{frame} |
---|
749 | \frametitle{Summary} |
---|
750 | We have: |
---|
751 | \begin{itemize} |
---|
752 | \item |
---|
753 | Translated the O'Caml prototype's backend intermediate languages into Matita |
---|
754 | \item |
---|
755 | Implemented the translations between languages, and given the intermediate languages a semantics |
---|
756 | \item |
---|
757 | Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised |
---|
758 | \item |
---|
759 | Spotted opportunities for possibly commuting backend translation passes |
---|
760 | \item |
---|
761 | Used six months to define structured traces and start the proof of correctness for the assembler |
---|
762 | \item |
---|
763 | Distinguished our proof from CompCert's by heavy use of dependent types throughout whole compiler |
---|
764 | \end{itemize} |
---|
765 | \end{frame} |
---|
766 | |
---|
767 | \end{document} |
---|