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

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

Finished presentation, added proper CerCo? style.

File size: 21.9 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\end{itemize}
81\end{frame}
82
83\begin{frame}
84\frametitle{Backend intermediate languages II}
85\begin{small}
86\begin{tabbing}
87\quad \=\,\quad \= \\
88\textsf{RTLabs}\\
89\> $\downarrow$ \> copy propagation (an endo-transformation, yet to be ported) \\
90\> $\downarrow$ \> instruction selection\\
91\> $\downarrow$ \> change of memory models in compiler\\
92\textsf{RTL}\\
93\> $\downarrow$ \> constant propagation (an endo-transformation, yet to be ported) \\
94\> $\downarrow$ \> calling convention made explicit \\
95\> $\downarrow$ \> layout of activation records \\
96\textsf{ERTL}\\
97\> $\downarrow$ \> register allocation and spilling\\
98\> $\downarrow$ \> dead code elimination\\
99\textsf{LTL}\\
100\> $\downarrow$ \> function linearisation\\
101\> $\downarrow$ \> branch compression (an endo-transformation) \\
102\textsf{LIN}\\
103\> $\downarrow$ \> relabeling\\
104\end{tabbing}
105\end{small}
106\end{frame}
107
108\begin{frame}
109\frametitle{\texttt{Joint}: a new approach I}
110\begin{itemize}
111\item
112Looking at O'Caml code, languages after RTLabs are similar
113\item
114Similar instructions, similar semantics, and so on
115\item
116Differences are slight
117\item
118Pseudoregisters used instead of hardware registers
119\item
120A few new unique instructions for each language
121\item
122In semantics: some notion of `successor' of an instruction, etc.
123\end{itemize}
124\end{frame}
125
126\begin{frame}
127\frametitle{\texttt{Joint}: a new approach II}
128\begin{itemize}
129\item
130Idea: all of these languages are just instances of a single language
131\item
132This language \texttt{Joint} is parameterised by a type of registers to be used in instructions, and so forth
133\item
134Each language after RTLabs is now just defined as the \texttt{Joint} language instantiated with some concrete types
135\item
136Similarly for semantics: common definitions that take e.g. type representing program counters as parameters
137\end{itemize}
138\end{frame}
139
140\begin{frame}[fragile]
141\frametitle{\texttt{Joint}: a new approach III}
142\texttt{Joint} instructions allow us to embed language-specific instructions:
143\begin{lstlisting}
144inductive joint_instruction (p: params__) (globals: list ident): Type[0] :=
145 | COMMENT: String $\rightarrow$ joint_instruction p globals
146 | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals
147 ...
148 | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals
149 | extension: extend_statements p $\rightarrow$ joint_instruction p globals.
150\end{lstlisting}
151
152\begin{lstlisting}
153inductive ertl_statement_extension: Type[0] :=
154 | ertl_st_ext_new_frame: ertl_statement_extension
155 | ertl_st_ext_del_frame: ertl_statement_extension
156 | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension.
157\end{lstlisting}
158\end{frame}
159
160\begin{frame}[fragile]
161\frametitle{\texttt{Joint}: a new approach IV}
162For example, the definition of the \texttt{ERTL} language is now:
163\begin{lstlisting}
164inductive move_registers: Type[0] :=
165 | pseudo: register $\rightarrow$ move_registers
166 | hardware: Register $\rightarrow$ move_registers.
167
168definition ertl_params__: params__ :=
169 mk_params__ register register register register
170  (move_registers $\times$ move_registers)
171   register nat unit ertl_statement_extension.
172definition ertl_params_: params_ :=
173 graph_params_ ertl_params__.
174definition ertl_params0: params0 :=
175 mk_params0 ertl_params__ (list register) nat.
176definition ertl_params1: params1 :=
177 rtl_ertl_params1 ertl_params0.
178definition ertl_params: $\forall$globals. params globals ≝
179 rtl_ertl_params ertl_params0.
180\end{lstlisting}
181\end{frame}
182
183\begin{frame}
184\frametitle{\texttt{Joint}: advantages}
185\begin{itemize}
186\item
187Why use \texttt{Joint}, as opposed to defining all languages individually?
188\item
189Reduces repeated code (fewer bugs, or places to change)
190\item
191Unify some proofs, making correctness proof easier
192\item
193Easier to add new intermediate languages as needed
194\item
195Easier to see relationship between consecutive languages at a glance
196\end{itemize}
197\end{frame}
198
199\begin{frame}[fragile]
200\frametitle{Instruction embedding in \texttt{Joint}}
201\begin{lstlisting}
202inductive joint_instruction (p:params__) (globals: list ident): Type[0] :=
203 ...
204 | POP: acc_a_reg p $\rightarrow$ joint_instruction p globals
205 | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals
206 ...
207\end{lstlisting}
208\begin{itemize}
209\item
210RTLabs (not a \texttt{Joint} language) to RTL is where instruction selection takes place
211\item
212Instructions from the MCS-51 instruction set embedded in \texttt{Joint} syntax
213\end{itemize}
214\end{frame}
215
216\begin{frame}
217\frametitle{Semantics of \texttt{Joint} I}
218\begin{itemize}
219\item
220As mentioned, use of \texttt{Joint} also unifies semantics of these languages
221\item
222We use several sets of records, which represent the state that a program is in
223\item
224These records are parametric in representations for e.g. frames
225\end{itemize}
226\end{frame}
227
228\begin{frame}[fragile]
229\frametitle{Semantics of \texttt{Joint} II}
230\begin{lstlisting}
231record more_sem_params (p:params_): Type[1] :=
232{
233  framesT: Type[0];
234  empty_framesT: framesT;
235  regsT: Type[0];
236  ...
237  acca_store_: acc_a_reg p → beval → regsT → res regsT;
238  acca_retrieve_: regsT → acc_a_reg p → res beval;
239  ...
240  pair_reg_move_: regsT → pair_reg p → res regsT
241 }.
242\end{lstlisting}
243\end{frame}
244
245\begin{frame}[fragile]
246\frametitle{Semantics of \texttt{Joint} III}
247Generic functions:
248\begin{lstlisting}
249definition set_carry: $\forall$p. beval $\rightarrow$ state p $\rightarrow$ state p :=
250 $\lambda$p, carry, st.
251  mk_state $\ldots$ (st_frms $\ldots$ st) (pc $\ldots$ st)
252   (sp $\ldots$ st) (isp $\ldots$ st) carry (regs $\ldots$ st) (m $\ldots$ st).
253\end{lstlisting}
254\begin{lstlisting}
255definition goto: $\forall$globals. $\forall$p:sem_params1 globals. genv globals p $\rightarrow$
256  label $\rightarrow$ state p $\rightarrow$ res (state p) :=
257 $\lambda$globals, p, ge, l, st.
258  do oldpc $\leftarrow$ pointer_of_address (pc $\ldots$ st) ;
259  do newpc $\leftarrow$ address_of_label $\ldots$ ge oldpc l ;
260  OK $\ldots$ (set_pc $\ldots$ newpc st).
261\end{lstlisting}
262\end{frame}
263
264\begin{frame}[fragile]
265\frametitle{Semantics of \texttt{Joint} IV}
266Individual semantics obtained by instantiating records to concrete types (ERTL here):
267\begin{lstlisting}
268definition ertl_more_sem_params: more_sem_params ertl_params_ :=
269 mk_more_sem_params ertl_params_
270  (list (register_env beval)) [] ((register_env beval) $\times$ hw_register_env)
271   ($\lambda$sp. $\langle$empty_map $\ldots$,init_hw_register_env sp$\rangle$) 0 it
272   ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store
273    ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve
274     ($\lambda$locals,dest_src.
275       do v $\leftarrow$
276        match \snd dest_src with
277        [ pseudo reg $\Rightarrow$ ps_reg_retrieve locals reg
278        | hardware reg $\Rightarrow$ hw_reg_retrieve locals reg
279        ];
280       match \fst dest_src with
281       [ pseudo reg $\Rightarrow$ ps_reg_store reg v locals
282       | hardware reg $\Rightarrow$ hw_reg_store reg v locals
283       ]).
284\end{lstlisting}
285\end{frame}
286
287\begin{frame}[fragile]
288\frametitle{Semantics of \texttt{Joint} V}
289For languages with `extensions', we provide a semantics:
290\begin{lstlisting}
291definition ertl_exec_extended:
292 $\forall$globals. genv globals (ertl_params globals) $\rightarrow$
293  ertl_statement_extension $\rightarrow$ label $\rightarrow$ state ertl_sem_params $\rightarrow$
294   IO io_out io_in (trace $\times$ (state ertl_sem_params)) :=
295 $\lambda$globals, ge, stm, l, st.
296  match stm with
297   [ ertl_st_ext_new_frame $\Rightarrow$
298      ! v $\leftarrow$ framesize globals $\ldots$ ge st;
299      let sp := get_hwsp st in
300      ! newsp $\leftarrow$ addr_sub sp v;
301      let st := set_hwsp newsp st in
302      ! st $\leftarrow$ next $\ldots$ (ertl_sem_params1 globals) l st ;
303        ret ? $\langle$E0, st$\rangle$
304   | ...
305   ].
306\end{lstlisting}
307\end{frame}
308
309\begin{frame}
310\frametitle{\texttt{Joint} summary}
311\begin{itemize}
312\item
313Using \texttt{Joint} we get a modular semantics
314\item
315`Common' semantics are shared amongst all languages
316\item
317Specific languages are responsible for providing the semantics of the extensions that they provide
318\item
319Show differences (and similarities) between languages clearly
320\item
321Reduces proofs
322\item
323Easy to add new languages
324\end{itemize}
325\end{frame}
326
327\begin{frame}
328\frametitle{A new intermediate language}
329\begin{itemize}
330\item
331Matita backend includes a new intermediate language: RTLntc
332\item
333Sits between RTL and ERTL
334\item
335RTLntc is the RTL language where all tailcalls have been eliminated
336\item
337This language is `implicit' in the O'Caml compiler
338\item
339There, the RTL to ERTL transformation eliminates tailcalls as part of translation
340\item
341But including an extra, explicit intermediate language is `almost free' using the \texttt{Joint} language approach
342\end{itemize}
343\end{frame}
344
345\begin{frame}
346\frametitle{The LTL to LIN transform I}
347\begin{itemize}
348\item
349The order of transformations in O'Caml prototype is fixed
350\item
351Linearisation takes place at a fixed place, in the translation between LTL and LIN
352\item
353The Matita compiler is different: linearisation is a generic process
354\item
355Any graph-based language can now be linearised
356\end{itemize}
357\end{frame}
358
359\begin{frame}
360\frametitle{The LTL to LIN transform II}
361\begin{itemize}
362\item
363The CompCert backend linearises much sooner than CerCo's
364\item
365We can now experiment with linearising much earlier
366\item
367Many transformations and optimisations can work fine on a linearised form
368\end{itemize}
369\end{frame}
370
371\begin{frame}
372\frametitle{`Free time'}
373\begin{itemize}
374\item
375We had six months of `free time', time not allotted in the Contract to working on any explicit deliverable
376\item
377We invested this time working on:
378\begin{itemize}
379\item
380The proof of correctness for the assembler
381\item
382A notion of `structured traces', used throughout the compiler formalisation, as a means of eventually proving that the compiler correctly preserves costs
383\item
384Structured traces were defined in collaboration with the team at UEDIN
385\end{itemize}
386\item
387I now explain in more detail how this time was used
388\end{itemize}
389\end{frame}
390
391\begin{frame}
392\frametitle{Assembler}
393\begin{itemize}
394\item
395After LIN, compiler spits out assembly language for MCS-51
396\item
397Assembler has pseudoinstructions similar to many commercial assembly languages
398\item
399For 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
400\item
401Simplifies the compiler, at the expense of introducing more proof obligations
402\end{itemize}
403\end{frame}
404
405\begin{frame}
406\frametitle{A problem: jump expansion}
407\begin{itemize}
408\item
409`Jump expansion' is our name for the following (standard) problem
410\item
411Given 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?
412\item
413Problem also applies to conditional jumps
414\item
415Problem especially relevant for MCS-51 as it has a small code memory, therefore aggressive expansion of jumps into smallest possible concrete jump instruction needed
416\item
417But a known hard problem (NP-complete depending on architecture), and easy to imagine knotty configurations where size of jumps are interdependent
418\end{itemize}
419\end{frame}
420
421\begin{frame}
422\frametitle{Jump expansion I}
423\begin{itemize}
424\item
425We employed the following tactic: split the decision over how any particular pseudoinstruction is expanded from pseudoinstruction expansion
426\item
427Call the decision maker a `policy'
428\item
429We started the proof of correctness for the assembler based on the premise that a correct policy exists
430\item
431Further, 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)
432\item
433A 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
434\end{itemize}
435\end{frame}
436
437\begin{frame}
438\frametitle{Jump expansion II}
439\begin{itemize}
440\item
441Boender at UNIBO has been working on a verified implementation of a good jump expansion policy for the MCS-51
442\item
443The strategy initially translates all pseudojumps as \texttt{SJMP} and then increases their size if necessary
444\item
445Termination of the procedure is proved, as well as a safety property, stating that jumps are not expanded into jumps that are too long
446\item
447Optimality is not proved
448\item
449Boender's work is the first formal treatment of the `jump expansion problem'
450\end{itemize}
451\end{frame}
452
453\begin{frame}
454\frametitle{Assembler correctness proof}
455\begin{itemize}
456\item
457Assuming the existence of a good jump expansion property, we completed about 50\% of the correctness proof for the assembler
458\item
459Boender's work constitutes a large missing piece (modulo a few missing lemmas), but holes still remain in the main proof
460\item
461We abandoned this work to start on other tasks
462\item
463However, we intend to return to the proof, and publishing an account of the work (possibly) as a journal paper
464\end{itemize}
465\end{frame}
466
467\begin{frame}
468\frametitle{Structured traces I}
469\begin{itemize}
470\item
471We introduced a notion of `structured traces'
472\item
473These are intended to statically capture the execution trace of a program
474\item
475Come in two variants: inductive and coinductive
476\item
477Inductive is meant to capture program execution traces that eventually halt
478\item
479Coinductive is meant to capture program execution traces that diverge
480\end{itemize}
481\end{frame}
482
483\begin{frame}
484\frametitle{Structured traces II}
485\begin{itemize}
486\item
487Here, I focus on the inductive variety
488\item
489Used the most (for now) in the backend
490\item
491In particular, used in the proof that static and dynamic cost computations coincide
492\item
493This will be explained later
494\end{itemize}
495\end{frame}
496
497\begin{frame}
498\frametitle{Structured traces III}
499\begin{itemize}
500\item
501Central insight is that program execution is always in the body of some function (from \texttt{main} onwards)
502\item
503A well formed program must have labels appearing at certain spots
504\item
505Similarly, the final instruction executed when executing a function must be a \texttt{RET} instruction
506\item
507These invariants, and others, are crystalised in the specific syntactic form of a structured trace
508\item
509Some examples...
510\end{itemize}
511\end{frame}
512
513\begin{frame}[fragile]
514\frametitle{Structured trace examples I}
515Traces end with a return being executed, or not:
516\begin{lstlisting}
517inductive trace_ends_with_ret: Type[0] :=
518 | ends_with_ret: trace_ends_with_ret
519 | doesnt_end_with_ret: trace_ends_with_ret.
520\end{lstlisting}
521A trace starting with a label and ending with a return:
522\begin{lstlisting}
523inductive trace_label_return (S: abstract_status): S $\rightarrow$ S $\rightarrow$ Type[0] :=
524 | tlr_base:
525  $\forall$status_before: S.
526  $\forall$status_after: S.
527   trace_label_label S ends_with_ret status_before status_after $\rightarrow$
528    trace_label_return S status_before status_after
529  ...
530\end{lstlisting}
531\end{frame}
532
533\begin{frame}[fragile]
534\frametitle{Structured trace examples II}
535A trace starting and ending with a cost label:
536\begin{lstlisting}
537...
538with trace_label_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] :=
539 | tll_base:
540  $\forall$ends_flag: trace_ends_with_ret.
541  $\forall$start_status: S.
542  $\forall$end_status: S.
543   trace_any_label S ends_flag start_status end_status $\rightarrow$
544   as_costed S start_status $\rightarrow$
545    trace_label_label S ends_flag start_status end_status
546...
547\end{lstlisting}
548\end{frame}
549
550\begin{frame}[fragile]
551\frametitle{Structured trace examples III}
552A call followed by a label on return:
553\begin{lstlisting}
554...
555with trace_any_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] :=
556...
557 | tal_base_call:
558  $\forall$status_pre_fun_call: S.   
559  $\forall$status_start_fun_call: S.
560  $\forall$status_final: S.
561   as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$
562   $\forall$H:as_classifier S status_pre_fun_call cl_call.
563    as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final $\rightarrow$
564    trace_label_return S status_start_fun_call status_final $\rightarrow$
565    as_costed S status_final $\rightarrow$
566     trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
567...
568\end{lstlisting}
569\end{frame}
570
571\begin{frame}[fragile]
572\frametitle{Structured trace examples IV}
573A call followed by a non-empty trace:
574\begin{lstlisting}
575...
576| tal_step_call:
577 $\forall$end_flag: trace_ends_with_ret.
578 $\forall$status_pre_fun_call: S.
579 $\forall$status_start_fun_call: S.
580 $\forall$status_after_fun_call: S.
581 $\forall$status_final: S.
582  as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$
583  $\forall$H:as_classifier S status_pre_fun_call cl_call.
584   as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call $\rightarrow$
585   trace_label_return S status_start_fun_call status_after_fun_call $\rightarrow$
586   ¬ as_costed S status_after_fun_call $\rightarrow$
587   trace_any_label S end_flag status_after_fun_call status_final $\rightarrow$
588    trace_any_label S end_flag status_pre_fun_call status_final
589...
590\end{lstlisting}
591\end{frame}
592
593\begin{frame}
594\frametitle{Static and dynamic costs I}
595\begin{itemize}
596\item
597Given a structured trace, we can compute its associated cost
598\item
599This is the \emph{static} cost of a program execution
600\item
601Similarly, given a program counter and a code memory (corresponding to the trace), we can compute a \emph{dynamic cost} of a simple block
602\item
603Do this by repeatedly fetching, obtaining the next instruction, and a new program counter
604\item
605This requires some predicates defining what a `good program' and what a `good program counter' are
606\end{itemize}
607\end{frame}
608
609\begin{frame}
610\frametitle{Static and dynamic costs II}
611\begin{itemize}
612\item
613We aim to prove that the dynamic and static cost calculations coincide
614\item
615This would imply that the static cost computation is correct
616\item
617This proof is surprisingly tricky to complete (about 3 man months of work so far)
618\item
619Is now about 75\% complete
620\end{itemize}
621\end{frame}
622
623\begin{frame}
624\frametitle{Changes ported to O'Caml prototype}
625\begin{itemize}
626\item
627Bug fixes spotted in the formalisation so far have been merged back into the O'Caml compiler
628\item
629Larger changes like the \texttt{Joint} machinery have so far not
630\item
631It is unclear whether they will be
632\item
633Just a generalization of what is already there
634\item
635Supposed to make formalization easier
636\end{itemize}
637\end{frame}
638
639\begin{frame}
640\frametitle{Improvements in Matita}
641\begin{itemize}
642\item
643Part of the motivation for using Matita was for CerCo to act a `stress test'
644\item
645The proofs talked about in this talk have done this
646\item
647Many improvements to Matita have been made since the last project meeting
648\item
649These 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
650\end{itemize}
651\end{frame}
652
653\begin{frame}
654\frametitle{Summary}
655We have:
656\begin{itemize}
657\item
658Translated the O'Caml prototype's backend intermediate languages into Matita
659\item
660Implemented the translations between languages, and given the intermediate languages a semantics
661\item
662Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised
663\item
664Spotted opportunities for commuting backend translation passes
665\item
666Used six months of `free time' to define structured traces and start the proof of correctness for the assembler
667\end{itemize}
668\end{frame}
669
670\end{document}
Note: See TracBrowser for help on using the repository browser.