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

Last change on this file since 1824 was 1824, checked in by mulligan, 7 years ago

More changes to presentation, following Claudio's comments

File size: 23.4 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}
486\frametitle{Structured traces I}
487\begin{itemize}
488\item
489We introduced a notion of `structured traces'
490\item
491These are intended to statically capture the execution trace of a program
492\item
493Come in two variants: inductive and coinductive
494\item
495Inductive is meant to capture program execution traces that eventually halt
496\item
497Coinductive is meant to capture program execution traces that diverge
498\end{itemize}
499\end{frame}
500
501\begin{frame}
502\frametitle{Structured traces II}
503\begin{itemize}
504\item
505Here, I focus on the inductive variety
506\item
507Used the most (for now) in the backend
508\item
509In particular, used in the proof that static and dynamic cost computations coincide
510\item
511This will be explained later
512\end{itemize}
513\end{frame}
514
515\begin{frame}
516\frametitle{Structured traces III}
517\begin{itemize}
518\item
519Central insight is that program execution is always in the body of some function (from \texttt{main} onwards)
520\item
521A well formed program must have labels appearing at certain spots
522\item
523Similarly, the final instruction executed when executing a function must be a \texttt{RET} instruction
524\item
525These invariants, and others, are crystalised in the specific syntactic form of a structured trace
526\item
527Some examples...
528\end{itemize}
529\end{frame}
530
531\begin{frame}[fragile]
532\frametitle{Structured trace examples I}
533Traces end with a return being executed, or not:
534\begin{lstlisting}
535inductive trace_ends_with_ret: Type[0] :=
536 | ends_with_ret: trace_ends_with_ret
537 | doesnt_end_with_ret: trace_ends_with_ret.
538\end{lstlisting}
539A trace starting with a label and ending with a return:
540\begin{lstlisting}
541inductive trace_label_return (S: abstract_status): S $\rightarrow$ S $\rightarrow$ Type[0] :=
542 | tlr_base:
543  $\forall$status_before: S.
544  $\forall$status_after: S.
545   trace_label_label S ends_with_ret status_before status_after $\rightarrow$
546    trace_label_return S status_before status_after
547  ...
548\end{lstlisting}
549\end{frame}
550
551\begin{frame}[fragile]
552\frametitle{Structured trace examples II}
553A trace starting and ending with a cost label:
554\begin{lstlisting}
555...
556with trace_label_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] :=
557 | tll_base:
558  $\forall$ends_flag: trace_ends_with_ret.
559  $\forall$start_status: S.
560  $\forall$end_status: S.
561   trace_any_label S ends_flag start_status end_status $\rightarrow$
562   as_costed S start_status $\rightarrow$
563    trace_label_label S ends_flag start_status end_status
564...
565\end{lstlisting}
566\end{frame}
567
568\begin{frame}[fragile]
569\frametitle{Structured trace examples III}
570A call followed by a label on return:
571\begin{lstlisting}
572...
573with trace_any_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] :=
574...
575 | tal_base_call:
576  $\forall$status_pre_fun_call: S.   
577  $\forall$status_start_fun_call: S.
578  $\forall$status_final: S.
579   as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$
580   $\forall$H:as_classifier S status_pre_fun_call cl_call.
581    as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final $\rightarrow$
582    trace_label_return S status_start_fun_call status_final $\rightarrow$
583    as_costed S status_final $\rightarrow$
584     trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
585...
586\end{lstlisting}
587\end{frame}
588
589\begin{frame}[fragile]
590\frametitle{Structured trace examples IV}
591A call followed by a non-empty trace:
592\begin{lstlisting}
593...
594| tal_step_call:
595 $\forall$end_flag: trace_ends_with_ret.
596 $\forall$status_pre_fun_call: S.
597 $\forall$status_start_fun_call: S.
598 $\forall$status_after_fun_call: S.
599 $\forall$status_final: S.
600  as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$
601  $\forall$H:as_classifier S status_pre_fun_call cl_call.
602   as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call $\rightarrow$
603   trace_label_return S status_start_fun_call status_after_fun_call $\rightarrow$
604   ¬ as_costed S status_after_fun_call $\rightarrow$
605   trace_any_label S end_flag status_after_fun_call status_final $\rightarrow$
606    trace_any_label S end_flag status_pre_fun_call status_final
607...
608\end{lstlisting}
609\end{frame}
610
611\begin{frame}
612\frametitle{Static and dynamic costs I}
613\begin{itemize}
614\item
615Given a structured trace, we can compute its associated cost
616\item
617This is the \emph{static} cost of a program execution
618\item
619Similarly, given a program counter and a code memory (corresponding to the trace), we can compute a \emph{dynamic cost} of a simple block
620\item
621Do this by repeatedly fetching, obtaining the next instruction, and a new program counter
622\item
623This requires some predicates defining what a `good program' and what a `good program counter' are
624\end{itemize}
625\end{frame}
626
627\begin{frame}
628\frametitle{Static and dynamic costs II}
629\begin{itemize}
630\item
631We aim to prove that the dynamic and static cost calculations coincide
632\item
633This would imply that the static cost computation is correct
634\item
635This proof is surprisingly tricky to complete (about 3 man months of work so far)
636\item
637Is now about 95\% complete
638\end{itemize}
639\end{frame}
640
641\begin{frame}
642\frametitle{Changes ported to O'Caml prototype}
643\begin{itemize}
644\item
645Bug fixes spotted in the formalisation so far have been merged back into the O'Caml compiler
646\item
647Larger changes like the \texttt{Joint} machinery have so far not
648\item
649It is unclear whether they will be
650\item
651Just a generalisation of what is already there
652\item
653Supposed to make formalisation easier
654\item
655Further, we want to ensure that the untrusted compiler is as correct as possible, for experiments in e.g. Frama-C
656\item
657Porting a large change to the untrusted compiler would jeopardise these experiments
658\end{itemize}
659\end{frame}
660
661\begin{frame}
662\frametitle{Improvements in Matita}
663\begin{itemize}
664\item
665Part of the motivation for using Matita was for CerCo to act a `stress test'
666\item
667The proofs talked about in this talk have done this
668\item
669Many improvements to Matita have been made since the last project meeting
670\item
671These 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
672\end{itemize}
673\end{frame}
674
675\begin{frame}
676\frametitle{The next period}
677% XXX: todo
678\end{frame}
679
680\begin{frame}
681\frametitle{Summary}
682We have:
683\begin{itemize}
684\item
685Translated the O'Caml prototype's backend intermediate languages into Matita
686\item
687Implemented the translations between languages, and given the intermediate languages a semantics
688\item
689Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised
690\item
691Spotted opportunities for possibly commuting backend translation passes
692\item
693Used six months to define structured traces and start the proof of correctness for the assembler
694\item
695Distinguished our proof from CompCert's by heavy use of dependent types throughout whole compiler
696\end{itemize}
697\end{frame}
698
699\end{document}
Note: See TracBrowser for help on using the repository browser.