source: Deliverables/D1.2/Presentations/WP4-dominic.tex @ 1829

Last change on this file since 1829 was 1829, checked in by mulligan, 8 years ago

changes to my presentation, just one point left to consider

File size: 25.1 KB
Line 
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}
37Relevant tasks: T4.2 and T4.3 (from the CerCo Contract):
38\begin{quotation}
39\textbf{Task 4.2}
40Functional 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}
45Formal 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}
51Task 4.2 in detail (from the CerCo Contract):
52\begin{quotation}
53\textbf{CIC encoding: Back-end}:
54Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler.
55This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2.
56A 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}
62Task 4.3 in detail (from the CerCo contract):
63\begin{quotation}
64\textbf{Executable Formal Semantics of back-end intermediate languages}:
65This 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
73O'Caml prototype has five backend intermediate languages: RTLabs, RTL, ERTL, LTL, LIN
74\item
75RTLabs is the `frontier' between backend and frontend, last abstract language
76\item
77RTLabs, RTL, ERTL and LTL are graph based languages: functions represented as graphs of statements, with entry and exit points
78\item
79LIN is a linearised form of LTL, and is the exit point of the compiler's backend
80\item
81In 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
114Consecutive languages in backend must be similar
115\item
116Transformations between languages translate away some small specific set of features
117\item
118But looking at O'Caml code, not clear precisely what differences between languages are, as code is repeated
119\item
120Not clear if translation passes can commute, for instance
121\item
122CerCo passes are in a different order to CompCert (calling convention and register allocation done in different places)
123\item
124Instruction 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
132Idea: all of these languages are just instances of a single language
133\item
134This language \texttt{Joint} is parameterised by a type of registers to be used in instructions, and so forth
135\item
136Each language after RTLabs is now just defined as the \texttt{Joint} language instantiated with some concrete types
137\item
138Similarly 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}
146inductive 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}
155inductive 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}
164For example, the definition of the \texttt{ERTL} language is now:
165\begin{lstlisting}
166inductive move_registers: Type[0] :=
167 | pseudo: register $\rightarrow$ move_registers
168 | hardware: Register $\rightarrow$ move_registers.
169
170definition ertl_params__: params__ :=
171 mk_params__ register register register register
172  (move_registers $\times$ move_registers)
173   register nat unit ertl_statement_extension.
174definition ertl_params_: params_ :=
175 graph_params_ ertl_params__.
176definition ertl_params0: params0 :=
177 mk_params0 ertl_params__ (list register) nat.
178definition ertl_params1: params1 :=
179 rtl_ertl_params1 ertl_params0.
180definition 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}
188inductive 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
196RTLabs (not a \texttt{Joint} language) to RTL is where instruction selection takes place
197\item
198Instructions 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
206Why use \texttt{Joint}, as opposed to defining all languages individually?
207\item
208Reduces repeated code (fewer bugs, or places to change)
209\item
210Unify some proofs, making correctness proof easier
211\item
212Easier to add new intermediate languages as needed
213\item
214Easier to see relationship between consecutive languages at a glance
215\item
216Simplifies instruction selection (i.e. porting to a new platform, or expanding subset of instructions emitted)
217\item
218We 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
226As mentioned, use of \texttt{Joint} also unifies semantics of these languages
227\item
228We use several sets of records, which represent the state that a program is in
229\item
230These 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}
237record 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}
253Generic functions:
254\begin{lstlisting}
255definition 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}
261definition 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}
272Individual semantics obtained by instantiating records to concrete types (ERTL here):
273\begin{lstlisting}
274definition 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}
295For languages with `extensions', we provide a semantics:
296\begin{lstlisting}
297definition 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
319Using \texttt{Joint} we get a modular semantics
320\item
321`Common' semantics are shared amongst all languages
322\item
323Specific languages are responsible for providing the semantics of the extensions that they provide
324\item
325Show differences (and similarities) between languages clearly
326\item
327Reduces proofs
328\item
329Easy 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
337Matita backend includes a new intermediate language: RTLntc
338\item
339Sits between RTL and ERTL
340\item
341RTLntc is the RTL language where all tailcalls have been eliminated
342\item
343This language is `implicit' in the O'Caml compiler
344\item
345There, the RTL to ERTL transformation eliminates tailcalls as part of translation
346\item
347But 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
357We can vary how one works whilst fixing the other
358\item
359Linearisation is moving from fetching from a graph-based language to fetching from a list-based program representation
360\item
361The order of transformations in O'Caml prototype is fixed
362\item
363Linearisation takes place at a fixed place, in the translation between LTL and LIN
364\item
365The Matita compiler is different: linearisation is a generic process
366\item
367Any 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
375The CompCert backend linearises much sooner than CerCo's
376\item
377We can now experiment with linearising much earlier
378\item
379Many transformations and optimisations can work fine on a linearised form
380\item
381The 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
389We had six months of time which is not reported on in any deliverable
390\item
391We invested this time working on:
392\begin{itemize}
393\item
394The global proof sketch
395\item
396The setup of `proof infrastructure', common definitions, lemmas, invariants etc. required for main body of proof
397\item
398The proof of correctness for the assembler
399\item
400A notion of `structured traces', used throughout the compiler formalisation, as a means of eventually proving that the compiler correctly preserves costs
401\item
402Structured traces were defined in collaboration with the team at UEDIN
403\end{itemize}
404\item
405I 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
413After LIN, compiler spits out assembly language for MCS-51
414\item
415Assembler has pseudoinstructions similar to many commercial assembly languages
416\item
417For 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
419Simplifies 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
429Given 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
431Problem also applies to conditional jumps
432\item
433Problem 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
435But 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
443We employed the following tactic: split the decision over how any particular pseudoinstruction is expanded from pseudoinstruction expansion
444\item
445Call the decision maker a `policy'
446\item
447We started the proof of correctness for the assembler based on the premise that a correct policy exists
448\item
449Further, 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
451A 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
459Boender at UNIBO has been working on a verified implementation of a good jump expansion policy for the MCS-51
460\item
461The strategy initially translates all pseudojumps as \texttt{SJMP} and then increases their size if necessary
462\item
463Termination 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
465His strategy is not optimal (though the computed solution is optimal for the strategy employed)
466\item
467Boender'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
475Assuming the existence of a good jump expansion property, we completed about 75\% of the correctness proof for the assembler
476\item
477Boender's work has just been completed (modulo a few missing lemmas)
478\item
479We abandoned the main assembler proof to start work on other tasks (and wait for Boender to finish)
480\item
481However, 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}
488int main(int argc, char** argv) {
489  label1:
490    ...
491    some_function();
492  label2:
493    ...
494}
495\end{lstlisting}
496\begin{itemize}
497\item
498Question: where do we put cost labels to capture execution costs?
499\item
500Proof obligations complicated by panoply of labels
501\item
502Doesn't work well with \texttt{g(h() + 2 + f())}
503\item
504To 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
514Solution: omit \texttt{label2} and just keep \texttt{label1}
515\item
516We pay for everything `up front' when entering a function
517\item
518No need to prove \texttt{some\_function()} terminates
519\item
520But now execution of functions in CerCo takes a particular form
521\item
522Functions 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
532We introduced a notion of `structured traces'
533\item
534These are intended to statically capture the (good) execution traces of a program
535\item
536That is, functions return to where they ought
537\item
538Come in two variants: inductive and coinductive
539\item
540Inductive is meant to capture program execution traces that eventually halt
541\item
542Coinductive 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
550Here, I focus on the inductive variety
551\item
552Used the most (for now) in the backend
553\item
554In particular, used in the proof that static and dynamic cost computations coincide
555\item
556This will be explained later
557\end{itemize}
558\end{frame}
559
560\begin{frame}
561\frametitle{Structured traces III}
562\begin{itemize}
563\item
564Central insight is that program execution is always in the body of some function (from \texttt{main} onwards)
565\item
566A well formed program must have labels appearing at certain spots
567\item
568Similarly, the final instruction executed when executing a function must be a \texttt{RET}
569\item
570Execution must then continue in body of calling function, at correct place
571\item
572These invariants, and others, are crystalised in the specific syntactic form of a structured trace
573\item
574Some examples...
575\end{itemize}
576\end{frame}
577
578\begin{frame}[fragile]
579\frametitle{Structured trace examples I}
580Traces end with a return being executed, or not:
581\begin{lstlisting}
582inductive 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}
586A trace starting with a label and ending with a return:
587\begin{lstlisting}
588inductive 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}
600A trace starting and ending with a cost label:
601\begin{lstlisting}
602...
603with 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}
617A call followed by a label on return:
618\begin{lstlisting}
619...
620with 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}
638A 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
662Given a structured trace, we can compute its associated cost
663\item
664This is the \emph{static} cost of a program execution
665\item
666Similarly, 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
668Do this by repeatedly fetching, obtaining the next instruction, and a new program counter
669\item
670This 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
678We aim to prove that the dynamic and static cost calculations coincide
679\item
680This would imply that the static cost computation is correct
681\item
682This proof is surprisingly tricky to complete (about 3 man months of work so far)
683\item
684Is 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
692Bug fixes spotted in the formalisation so far have been merged back into the O'Caml compiler
693\item
694Larger changes like the \texttt{Joint} machinery have so far not
695\item
696It is unclear whether they will be
697\item
698Just a generalisation of what is already there
699\item
700Supposed to make formalisation easier
701\item
702Further, we want to ensure that the untrusted compiler is as correct as possible, for experiments in e.g. Frama-C
703\item
704Porting 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
712Part of the motivation for using Matita was for CerCo to act a `stress test'
713\item
714The proofs talked about in this talk have done this
715\item
716Many improvements to Matita have been made since the last project meeting
717\item
718These 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}
724UNIBO has following pool of remaining manpower (postdocs):
725\begin{center}
726\begin{tabular}{ll}
727Person & Man months remaining \\
728\hline
729Boender & 14 months \\
730Mulligan & 6 months \\
731Tranquilli & 10 months \\
732\end{tabular}
733\end{center}
734\begin{itemize}
735\item
736Boender finishing assembler correctness proof
737\item
738Mulligan proofs of correctness for 1 intermediate language
739\item
740Tranquilli proofs of correctness for 2 intermediate languages
741\item
742Sacerdoti Coen `floating'
743\item
744Believe we have enough manpower to complete backend
745\end{itemize}
746\end{frame}
747
748\begin{frame}
749\frametitle{Summary}
750We have:
751\begin{itemize}
752\item
753Translated the O'Caml prototype's backend intermediate languages into Matita
754\item
755Implemented the translations between languages, and given the intermediate languages a semantics
756\item
757Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised
758\item
759Spotted opportunities for possibly commuting backend translation passes
760\item
761Used six months to define structured traces and start the proof of correctness for the assembler
762\item
763Distinguished our proof from CompCert's by heavy use of dependent types throughout whole compiler
764\end{itemize}
765\end{frame}
766
767\end{document}
Note: See TracBrowser for help on using the repository browser.