Ignore:
Timestamp:
Mar 15, 2012, 11:18:30 AM (8 years ago)
Author:
mulligan
Message:

Changes to my presentation based on feedback from practice session yesterday. More changes to come.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/Presentations/WP4-dominic.tex

    r1829 r1840  
    11\documentclass[serif]{beamer}
    22
     3\usepackage{amssymb}
    34\usepackage[english]{babel}
    45\usepackage{listings}
     
    3435
    3536\begin{frame}
    36 \frametitle{Summary I}
     37\frametitle{Summary}
    3738Relevant tasks: T4.2 and T4.3 (from the CerCo Contract):
    3839\begin{quotation}
     
    4849
    4950\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}
     51\frametitle{Contents}
     52\tableofcontents
     53\end{frame}
     54
     55\section{Rationalisation of backend languages}
    6856
    6957\begin{frame}
     
    7159\begin{itemize}
    7260\item
    73 O'Caml prototype has five backend intermediate languages: RTLabs, RTL, ERTL, LTL, LIN
     61OCaml prototype has five backend intermediate languages: RTLabs, RTL, ERTL, LTL, LIN
    7462\item
    7563RTLabs is the `frontier' between backend and frontend, last abstract language
     
    8775\begin{small}
    8876\begin{tabbing}
    89 \quad \=\,\quad \= \\
     77\quad \=\,\quad \=\ \\
    9078\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\\
     79\> $\downarrow$ \> copy propagation ($\times$) \\
     80\> $\downarrow$ \> instruction selection (\checkmark) \\
     81\> $\downarrow$ \> change of memory models in compiler (\checkmark) \\
    9482\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 \\
     83\> $\downarrow$ \> constant propagation ($\times$) \\
     84\> $\downarrow$ \> calling convention made explicit (\checkmark) \\
     85\> $\downarrow$ \> layout of activation records (\checkmark) \\
    9886\textsf{ERTL}\\
    99 \> $\downarrow$ \> register allocation and spilling\\
    100 \> $\downarrow$ \> dead code elimination\\
     87\> $\downarrow$ \> register allocation and spilling (\checkmark) \\
     88\> $\downarrow$ \> dead code elimination (\checkmark) \\
    10189\textsf{LTL}\\
    102 \> $\downarrow$ \> function linearisation\\
    103 \> $\downarrow$ \> branch compression (an endo-transformation) \\
     90\> $\downarrow$ \> function linearisation (\checkmark) \\
     91\> $\downarrow$ \> branch compression ($\times$) \\
    10492\textsf{LIN}\\
    105 \> $\downarrow$ \> relabeling\\
     93\> $\downarrow$ \> relabeling (\checkmark) \\
     94\textsf{ASM}
    10695\end{tabbing}
    10796\end{small}
     
    116105Transformations between languages translate away some small specific set of features
    117106\item
    118 But looking at O'Caml code, not clear precisely what differences between languages are, as code is repeated
     107But looking at OCaml code, not clear precisely what differences between languages are, as code is repeated
    119108\item
    120109Not clear if translation passes can commute, for instance
     
    160149\end{frame}
    161150
    162 \begin{frame}[fragile]
     151\begin{frame}
    163152\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?
     153\begin{itemize}
     154\item
     155Languages that provide extensions need to provide translations and semantics for those extensions
     156\item
     157Everything else can be handled at the \texttt{Joint}-level
     158\item
     159This modularises the handling of these languages
     160\end{itemize}
     161\end{frame}
     162
     163\begin{frame}
     164\frametitle{\texttt{Joint}: advantages I}
     165\begin{itemize}
     166\item
     167We can recover the concrete OCaml languages by instantiating parameterized types
     168\item
     169Why use \texttt{Joint}?
    207170\item
    208171Reduces repeated code (fewer bugs, or places to change)
    209172\item
    210173Unify some proofs, making correctness proof easier
     174\end{itemize}
     175\end{frame}
     176
     177\begin{frame}
     178\frametitle{\texttt{Joint}: advantages II}
     179\begin{itemize}
    211180\item
    212181Easier to add new intermediate languages as needed
     
    214183Easier to see relationship between consecutive languages at a glance
    215184\item
    216 Simplifies instruction selection (i.e. porting to a new platform, or expanding subset of instructions emitted)
     185MCS-51 instruction set embedded in \texttt{Joint} syntax
     186\item
     187Simplifies instruction selection
    217188\item
    218189We can investigate which translation passes commute much more easily
     
    232203\end{frame}
    233204
    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 
    333205\begin{frame}
    334206\frametitle{A new intermediate language}
     
    341213RTLntc is the RTL language where all tailcalls have been eliminated
    342214\item
    343 This language is `implicit' in the O'Caml compiler
     215This language is `implicit' in the OCaml compiler
    344216\item
    345217There, the RTL to ERTL transformation eliminates tailcalls as part of translation
     
    359231Linearisation is moving from fetching from a graph-based language to fetching from a list-based program representation
    360232\item
    361 The order of transformations in O'Caml prototype is fixed
     233The order of transformations in OCaml prototype is fixed
    362234\item
    363235Linearisation takes place at a fixed place, in the translation between LTL and LIN
     
    373245\begin{itemize}
    374246\item
    375 The CompCert backend linearises much sooner than CerCo's
    376 \item
    377 We can now experiment with linearising much earlier
     247CompCert backend linearises much sooner than CerCo's
     248\item
     249Can now experiment with linearising much earlier
    378250\item
    379251Many transformations and optimisations can work fine on a linearised form
    380252\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'}
     253Only place in the (current) backend that requires a graph-based language is in the ERTL pass, where we do a dataflow analysis
     254\end{itemize}
     255\end{frame}
     256
     257\section{Assembler correctness proof and structured traces}
     258
     259\begin{frame}
     260\frametitle{Time not reported}
    387261\begin{itemize}
    388262\item
     
    402276Structured traces were defined in collaboration with the team at UEDIN
    403277\end{itemize}
    404 \item
    405 I now explain in more detail how this time was used
    406278\end{itemize}
    407279\end{frame}
     
    418290\item
    419291Simplifies the compiler, at the expense of introducing more proof obligations
     292\item
     293Now need a formalized assembler (a step further than CompCert)
    420294\end{itemize}
    421295\end{frame}
     
    457331\begin{itemize}
    458332\item
    459 Boender at UNIBO has been working on a verified implementation of a good jump expansion policy for the MCS-51
     333Jaap Boender at UNIBO has been working on a verified implementation of a good jump expansion policy for the MCS-51
    460334\item
    461335The strategy initially translates all pseudojumps as \texttt{SJMP} and then increases their size if necessary
     
    465339His strategy is not optimal (though the computed solution is optimal for the strategy employed)
    466340\item
    467 Boender's work is the first formal treatment of the `jump expansion problem'
     341Jaap's work is the first formal treatment of the `jump expansion problem'
    468342\end{itemize}
    469343\end{frame}
     
    475349Assuming the existence of a good jump expansion property, we completed about 75\% of the correctness proof for the assembler
    476350\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
     351Jaap's work has just been completed (modulo a few missing lemmas)
     352\item
     353Postponed the remainder of main assembler proof to start work on other tasks (and for Jaap to finish)
     354\item
     355We intend to return to proof, and publish an account of the work (possibly) as a journal paper
    482356\end{itemize}
    483357\end{frame}
     
    485359\begin{frame}[fragile]
    486360\frametitle{Who pays? I}
     361\begin{columns}
     362\begin{column}[b]{0.5\linewidth}
     363\centering
    487364\begin{lstlisting}
    488365int main(int argc, char** argv) {
    489   label1:
     366  cost_label1:
    490367    ...
    491368    some_function();
    492   label2:
     369  cost_label2:
    493370    ...
    494371}
    495372\end{lstlisting}
     373\end{column}
     374\begin{column}[b]{0.5\linewidth}
     375\centering
     376\begin{lstlisting}
     377  main:
     378    ...
     379  cost_label1:
     380    ...
     381    LCALL some_function
     382  cost_label2:
     383    ...
     384\end{lstlisting}
     385\end{column}
     386\end{columns}
    496387\begin{itemize}
    497388\item
     
    502393Doesn't work well with \texttt{g(h() + 2 + f())}
    503394\item
    504 To prove accuracy we need to show \texttt{some\_function()} terminates!
     395Is \texttt{cost\_label2} ever reached? \texttt{some\_function()} must terminate!
    505396\item
    506397\texttt{some\_function()} may not return correctly
     
    512403\begin{itemize}
    513404\item
    514 Solution: omit \texttt{label2} and just keep \texttt{label1}
     405Solution: omit \texttt{cost\_label2} and just keep \texttt{cost\_label1}
    515406\item
    516407We pay for everything `up front' when entering a function
     
    527418
    528419\begin{frame}
     420\frametitle{Recursive structure of `good' execution}
     421\begin{center}
     422\includegraphics[scale=0.33]{recursive_structure.png}
     423\end{center}
     424\end{frame}
     425
     426\begin{frame}
    529427\frametitle{Structured traces I}
    530428\begin{itemize}
     
    534432These are intended to statically capture the (good) execution traces of a program
    535433\item
    536 That is, functions return to where they ought
     434To borrow a slogan: they are the `computational content of a well-formed program's execution'
    537435\item
    538436Come in two variants: inductive and coinductive
    539437\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
     438Inductive captures program execution traces that eventually halt, coinductive ones that diverge
    543439\end{itemize}
    544440\end{frame}
     
    548444\begin{itemize}
    549445\item
    550 Here, I focus on the inductive variety
    551 \item
    552 Used the most (for now) in the backend
     446I focus on the inductive variety, as used the most (for now) in the backend
    553447\item
    554448In particular, used in the proof that static and dynamic cost computations coincide
    555449\item
     450Traces preserved by backend compilation, initially created at RTL
     451\item
    556452This will be explained later
    557453\end{itemize}
     
    571467\item
    572468These 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}
     469\end{itemize}
    656470\end{frame}
    657471
     
    669483\item
    670484This requires some predicates defining what a `good program' and what a `good program counter' are
     485\item
     486Want program counters on instruction boundaries
    671487\end{itemize}
    672488\end{frame}
     
    686502\end{frame}
    687503
    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
     504\section{Changes to tools and prototypes, looking forward}
     505
     506\begin{frame}
     507\frametitle{Changes ported to OCaml prototype}
     508\begin{itemize}
     509\item
     510Bug fixes spotted in the formalisation so far have been merged back into the OCaml compiler
    693511\item
    694512Larger changes like the \texttt{Joint} machinery have so far not
     
    727545Person & Man months remaining \\
    728546\hline
    729 Boender & 14 months \\
     547Boender & 10 months \\
    730548Mulligan & 6 months \\
    731549Tranquilli & 10 months \\
     
    742560Sacerdoti Coen `floating'
    743561\item
    744 Believe we have enough manpower to complete backend
     562Believe we have enough manpower to complete backend (required 21 man months)
    745563\end{itemize}
    746564\end{frame}
     
    751569\begin{itemize}
    752570\item
    753 Translated the O'Caml prototype's backend intermediate languages into Matita
     571Translated the OCaml prototype's backend intermediate languages into Matita
    754572\item
    755573Implemented the translations between languages, and given the intermediate languages a semantics
Note: See TracChangeset for help on using the changeset viewer.