\documentclass[serif]{beamer} \usepackage[english]{babel} \usepackage{listings} \usepackage{microtype} \usetheme{Frankfurt} \logo{\includegraphics[height=1.0cm]{fetopen.png}} \author{Dominic Mulligan} \title{CerCo Work Package 4} \date{CerCo project review meeting\\March 2012} \lstdefinelanguage{matita-ocaml} {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try}, morekeywords={[2]whd,normalize,elim,cases,destruct}, morekeywords={[3]type,of}, mathescape=true, } \lstset{language=matita-ocaml,basicstyle=\scriptsize\tt,columns=flexible,breaklines=false, keywordstyle=\color{red}\bfseries, keywordstyle=[2]\color{blue}, keywordstyle=[3]\color{blue}\bfseries, commentstyle=\color{green}, stringstyle=\color{blue}, showspaces=false,showstringspaces=false} \begin{document} \begin{frame} \maketitle \end{frame} \begin{frame} \frametitle{Summary I} Relevant tasks: T4.2 and T4.3 (from the CerCo Contract): \begin{quotation} \textbf{Task 4.2} Functional encoding in the Calculus of Inductive Construction (indicative effort: UNIBO: 8; UDP: 2; UEDIN: 0) \end{quotation} \begin{quotation} \textbf{Task 4.3} Formal semantics of intermediate languages (indicative effort: UNIBO: 4; UDP: 0; UEDIN: 0) \end{quotation} \end{frame} \begin{frame} \frametitle{Summary II} Task 4.2 in detail (from the CerCo Contract): \begin{quotation} \textbf{CIC encoding: Back-end}: Functional Specification in the internal language of the Proof Assistant (the Calculus of Inductive Construction) of the back end of the compiler. This unit is meant to be composable with the front-end of deliverable D3.2, to obtain a full working compiler for Milestone M2. 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. \end{quotation} \end{frame} \begin{frame} \frametitle{Summary III} Task 4.3 in detail (from the CerCo contract): \begin{quotation} \textbf{Executable Formal Semantics of back-end intermediate languages}: This prototype is the formal counterpart of deliverable D2.1 for the back end side of the compiler and validates it. \end{quotation} \end{frame} \begin{frame} \frametitle{Backend intermediate languages I} \begin{itemize} \item O'Caml prototype has five backend intermediate languages: RTLabs, RTL, ERTL, LTL, LIN \item RTLabs is the frontier' between backend and frontend, last abstract language \item RTLabs, RTL, ERTL and LTL are graph based languages: functions represented as graphs of statements, with entry and exit points \item LIN is a linearised form of LTL, and is the exit point of the compiler's backend \item In contrast to frontend, backend is very different to CompCert's \end{itemize} \end{frame} \begin{frame} \frametitle{Backend intermediate languages II} \begin{small} \begin{tabbing} \quad \=\,\quad \= \\ \textsf{RTLabs}\\ \> $\downarrow$ \> copy propagation (an endo-transformation, yet to be ported) \\ \> $\downarrow$ \> instruction selection\\ \> $\downarrow$ \> change of memory models in compiler\\ \textsf{RTL}\\ \> $\downarrow$ \> constant propagation (an endo-transformation, yet to be ported) \\ \> $\downarrow$ \> calling convention made explicit \\ \> $\downarrow$ \> layout of activation records \\ \textsf{ERTL}\\ \> $\downarrow$ \> register allocation and spilling\\ \> $\downarrow$ \> dead code elimination\\ \textsf{LTL}\\ \> $\downarrow$ \> function linearisation\\ \> $\downarrow$ \> branch compression (an endo-transformation) \\ \textsf{LIN}\\ \> $\downarrow$ \> relabeling\\ \end{tabbing} \end{small} \end{frame} \begin{frame} \frametitle{\texttt{Joint}: a new approach I} \begin{itemize} \item Consecutive languages in backend must be similar \item Transformations between languages translate away some small specific set of features \item But looking at O'Caml code, not clear precisely what differences between languages are, as code is repeated \item Not clear if translation passes can commute, for instance \item CerCo passes are in a different order to CompCert (calling convention and register allocation done in different places) \item Instruction selection done early: changing subset of instructions used would require instructions to be duplicated everywhere in backend \end{itemize} \end{frame} \begin{frame} \frametitle{\texttt{Joint}: a new approach II} \begin{itemize} \item Idea: all of these languages are just instances of a single language \item This language \texttt{Joint} is parameterised by a type of registers to be used in instructions, and so forth \item Each language after RTLabs is now just defined as the \texttt{Joint} language instantiated with some concrete types \item Similarly for semantics: common definitions that take e.g. type representing program counters as parameters \end{itemize} \end{frame} \begin{frame}[fragile] \frametitle{\texttt{Joint}: a new approach III} \texttt{Joint} instructions allow us to embed language-specific instructions: \begin{lstlisting} inductive joint_instruction (p: params__) (globals: list ident): Type[0] := | COMMENT: String $\rightarrow$ joint_instruction p globals | COST_LABEL: costlabel $\rightarrow$ joint_instruction p globals ... | COND: acc_a_reg p $\rightarrow$ label $\rightarrow$ joint_instruction p globals | extension: extend_statements p $\rightarrow$ joint_instruction p globals. \end{lstlisting} \begin{lstlisting} inductive ertl_statement_extension: Type[0] := | ertl_st_ext_new_frame: ertl_statement_extension | ertl_st_ext_del_frame: ertl_statement_extension | ertl_st_ext_frame_size: register $\rightarrow$ ertl_statement_extension. \end{lstlisting} \end{frame} \begin{frame}[fragile] \frametitle{\texttt{Joint}: a new approach IV} For example, the definition of the \texttt{ERTL} language is now: \begin{lstlisting} inductive move_registers: Type[0] := | pseudo: register $\rightarrow$ move_registers | hardware: Register $\rightarrow$ move_registers. definition ertl_params__: params__ := mk_params__ register register register register (move_registers $\times$ move_registers) register nat unit ertl_statement_extension. definition ertl_params_: params_ := graph_params_ ertl_params__. definition ertl_params0: params0 := mk_params0 ertl_params__ (list register) nat. definition ertl_params1: params1 := rtl_ertl_params1 ertl_params0. definition ertl_params: $\forall$globals. params globals ≝ rtl_ertl_params ertl_params0. \end{lstlisting} \end{frame} \begin{frame}[fragile] \frametitle{Instruction embedding in \texttt{Joint}} \begin{lstlisting} inductive joint_instruction (p:params__) (globals: list ident): Type[0] := ... | POP: acc_a_reg p $\rightarrow$ joint_instruction p globals | PUSH: acc_a_reg p $\rightarrow$ joint_instruction p globals ... \end{lstlisting} \begin{itemize} \item RTLabs (not a \texttt{Joint} language) to RTL is where instruction selection takes place \item Instructions from the MCS-51 instruction set embedded in \texttt{Joint} syntax \end{itemize} \end{frame} \begin{frame} \frametitle{\texttt{Joint}: advantages} \begin{itemize} \item Why use \texttt{Joint}, as opposed to defining all languages individually? \item Reduces repeated code (fewer bugs, or places to change) \item Unify some proofs, making correctness proof easier \item Easier to add new intermediate languages as needed \item Easier to see relationship between consecutive languages at a glance \item Simplifies instruction selection (i.e. porting to a new platform, or expanding subset of instructions emitted) \item We can investigate which translation passes commute much more easily \end{itemize} \end{frame} \begin{frame} \frametitle{Semantics of \texttt{Joint} I} \begin{itemize} \item As mentioned, use of \texttt{Joint} also unifies semantics of these languages \item We use several sets of records, which represent the state that a program is in \item These records are parametric in representations for e.g. frames \end{itemize} \end{frame} \begin{frame}[fragile] \frametitle{Semantics of \texttt{Joint} II} \begin{lstlisting} record more_sem_params (p:params_): Type[1] := { framesT: Type[0]; empty_framesT: framesT; regsT: Type[0]; ... acca_store_: acc_a_reg p $\rightarrow$ beval $\rightarrow$ regsT $\rightarrow$ res regsT; acca_retrieve_: regsT $\rightarrow$ acc_a_reg p $\rightarrow$ res beval; ... pair_reg_move_: regsT $\rightarrow$ pair_reg p $\rightarrow$ res regsT }. \end{lstlisting} \end{frame} \begin{frame}[fragile] \frametitle{Semantics of \texttt{Joint} III} Generic functions: \begin{lstlisting} definition set_carry: $\forall$p. beval $\rightarrow$ state p $\rightarrow$ state p := $\lambda$p, carry, st. mk_state $\ldots$ (st_frms $\ldots$ st) (pc $\ldots$ st) (sp $\ldots$ st) (isp $\ldots$ st) carry (regs $\ldots$ st) (m $\ldots$ st). \end{lstlisting} \begin{lstlisting} definition goto: $\forall$globals. $\forall$p:sem_params1 globals. genv globals p $\rightarrow$ label $\rightarrow$ state p $\rightarrow$ res (state p) := $\lambda$globals, p, ge, l, st. do oldpc $\leftarrow$ pointer_of_address (pc $\ldots$ st) ; do newpc $\leftarrow$ address_of_label $\ldots$ ge oldpc l ; OK $\ldots$ (set_pc $\ldots$ newpc st). \end{lstlisting} \end{frame} \begin{frame}[fragile] \frametitle{Semantics of \texttt{Joint} IV} Individual semantics obtained by instantiating records to concrete types (ERTL here): \begin{lstlisting} definition ertl_more_sem_params: more_sem_params ertl_params_ := mk_more_sem_params ertl_params_ (list (register_env beval)) [] ((register_env beval) $\times$ hw_register_env) ($\lambda$sp. $\langle$empty_map $\ldots$,init_hw_register_env sp$\rangle$) 0 it ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ps_reg_store ps_reg_retrieve ($\lambda$locals,dest_src. do v $\leftarrow$ match \snd dest_src with [ pseudo reg $\Rightarrow$ ps_reg_retrieve locals reg | hardware reg $\Rightarrow$ hw_reg_retrieve locals reg ]; match \fst dest_src with [ pseudo reg $\Rightarrow$ ps_reg_store reg v locals | hardware reg $\Rightarrow$ hw_reg_store reg v locals ]). \end{lstlisting} \end{frame} \begin{frame}[fragile] \frametitle{Semantics of \texttt{Joint} V} For languages with extensions', we provide a semantics: \begin{lstlisting} definition ertl_exec_extended: $\forall$globals. genv globals (ertl_params globals) $\rightarrow$ ertl_statement_extension $\rightarrow$ label $\rightarrow$ state ertl_sem_params $\rightarrow$ IO io_out io_in (trace $\times$ (state ertl_sem_params)) := $\lambda$globals, ge, stm, l, st. match stm with [ ertl_st_ext_new_frame $\Rightarrow$ ! v $\leftarrow$ framesize globals $\ldots$ ge st; let sp := get_hwsp st in ! newsp $\leftarrow$ addr_sub sp v; let st := set_hwsp newsp st in ! st $\leftarrow$ next $\ldots$ (ertl_sem_params1 globals) l st ; ret ? $\langle$E0, st$\rangle$ | ... ]. \end{lstlisting} \end{frame} \begin{frame} \frametitle{\texttt{Joint} summary} \begin{itemize} \item Using \texttt{Joint} we get a modular semantics \item Common' semantics are shared amongst all languages \item Specific languages are responsible for providing the semantics of the extensions that they provide \item Show differences (and similarities) between languages clearly \item Reduces proofs \item Easy to add new languages \end{itemize} \end{frame} \begin{frame} \frametitle{A new intermediate language} \begin{itemize} \item Matita backend includes a new intermediate language: RTLntc \item Sits between RTL and ERTL \item RTLntc is the RTL language where all tailcalls have been eliminated \item This language is implicit' in the O'Caml compiler \item There, the RTL to ERTL transformation eliminates tailcalls as part of translation \item But including an extra, explicit intermediate language is almost free' using the \texttt{Joint} language approach \end{itemize} \end{frame} \begin{frame} \frametitle{The LTL to LIN transform I} \begin{itemize} \item \texttt{Joint} clearly separates fetching from program execution \item We can vary how one works whilst fixing the other \item Linearisation is moving from fetching from a graph-based language to fetching from a list-based program representation \item The order of transformations in O'Caml prototype is fixed \item Linearisation takes place at a fixed place, in the translation between LTL and LIN \item The Matita compiler is different: linearisation is a generic process \item Any graph-based language can now be linearised \end{itemize} \end{frame} \begin{frame} \frametitle{The LTL to LIN transform II} \begin{itemize} \item The CompCert backend linearises much sooner than CerCo's \item We can now experiment with linearising much earlier \item Many transformations and optimisations can work fine on a linearised form \item The only place in the backend that requires a graph-based language is in the ERTL pass, where we do a dataflow analysis \end{itemize} \end{frame} \begin{frame} \frametitle{Free time'} \begin{itemize} \item We had six months of time which is not reported on in any deliverable \item We invested this time working on: \begin{itemize} \item The global proof sketch \item The setup of proof infrastructure', common definitions, lemmas, invariants etc. required for main body of proof \item The proof of correctness for the assembler \item A notion of structured traces', used throughout the compiler formalisation, as a means of eventually proving that the compiler correctly preserves costs \item Structured traces were defined in collaboration with the team at UEDIN \end{itemize} \item I now explain in more detail how this time was used \end{itemize} \end{frame} \begin{frame} \frametitle{Assembler} \begin{itemize} \item After LIN, compiler spits out assembly language for MCS-51 \item Assembler has pseudoinstructions similar to many commercial assembly languages \item For instance, instead of computed jumps (e.g. \texttt{SJMP} to a specific address), compiler can simply spit out a generic jump instruction to a label \item Simplifies the compiler, at the expense of introducing more proof obligations \end{itemize} \end{frame} \begin{frame} \frametitle{A problem: jump expansion} \begin{itemize} \item Jump expansion' is our name for the standard branch displacement' problem \item Given a pseudojump to a label $l$, how best can this be expanded into an assembly instruction \texttt{SJMP}, \texttt{AJMP} or \texttt{LJMP} to a concrete address? \item Problem also applies to conditional jumps \item Problem especially relevant for MCS-51 as it has a small code memory, therefore aggressive expansion of jumps into smallest possible concrete jump instruction needed \item But a known hard problem (NP-complete depending on architecture), and easy to imagine knotty configurations where size of jumps are interdependent \end{itemize} \end{frame} \begin{frame} \frametitle{Jump expansion I} \begin{itemize} \item We employed the following tactic: split the decision over how any particular pseudoinstruction is expanded from pseudoinstruction expansion \item Call the decision maker a policy' \item We started the proof of correctness for the assembler based on the premise that a correct policy exists \item Further, we know that the assembler only fails to assemble a program if a good policy does not exist (a side-effect of using dependent types) \item A bad policy is a function that expands a given pseudojump into a concrete jump instruction that is too small' for the distance to be jumped, or makes the program consume too much memory \end{itemize} \end{frame} \begin{frame} \frametitle{Jump expansion II} \begin{itemize} \item Boender at UNIBO has been working on a verified implementation of a good jump expansion policy for the MCS-51 \item The strategy initially translates all pseudojumps as \texttt{SJMP} and then increases their size if necessary \item Termination of the procedure is proved, as well as a safety property, stating that jumps are not expanded into jumps that are too long \item His strategy is not optimal (though the computed solution is optimal for the strategy employed) \item Boender's work is the first formal treatment of the jump expansion problem' \end{itemize} \end{frame} \begin{frame} \frametitle{Assembler correctness proof} \begin{itemize} \item Assuming the existence of a good jump expansion property, we completed about 75\% of the correctness proof for the assembler \item Boender's work has just been completed (modulo a few missing lemmas) \item We abandoned the main assembler proof to start work on other tasks (and wait for Boender to finish) \item However, we intend to return to the proof, and publishing an account of the work (possibly) as a journal paper \end{itemize} \end{frame} \begin{frame}[fragile] \frametitle{Who pays? I} \begin{lstlisting} int main(int argc, char** argv) { label1: ... some_function(); label2: ... } \end{lstlisting} \begin{itemize} \item Question: where do we put cost labels to capture execution costs? \item Proof obligations complicated by panoply of labels \item Doesn't work well with \texttt{g(h() + 2 + f())} \item To prove accuracy we need to show \texttt{some\_function()} terminates! \item \texttt{some\_function()} may not return correctly \end{itemize} \end{frame} \begin{frame} \frametitle{Who pays? II} \begin{itemize} \item Solution: omit \texttt{label2} and just keep \texttt{label1} \item We pay for everything up front' when entering a function \item No need to prove \texttt{some\_function()} terminates \item But now execution of functions in CerCo takes a particular form \item Functions begin with a label, call other functions that begin with a label, eventually return, but \emph{return} to the correct place \item Recursive structure' \end{itemize} \end{frame} \begin{frame} \frametitle{Structured traces I} \begin{itemize} \item We introduced a notion of structured traces' \item These are intended to statically capture the (good) execution traces of a program \item That is, functions return to where they ought \item Come in two variants: inductive and coinductive \item Inductive is meant to capture program execution traces that eventually halt \item Coinductive is meant to capture program execution traces that diverge \end{itemize} \end{frame} \begin{frame} \frametitle{Structured traces II} \begin{itemize} \item Here, I focus on the inductive variety \item Used the most (for now) in the backend \item In particular, used in the proof that static and dynamic cost computations coincide \item This will be explained later \end{itemize} \end{frame} \begin{frame} \frametitle{Structured traces III} \begin{itemize} \item Central insight is that program execution is always in the body of some function (from \texttt{main} onwards) \item A well formed program must have labels appearing at certain spots \item Similarly, the final instruction executed when executing a function must be a \texttt{RET} \item Execution must then continue in body of calling function, at correct place \item These invariants, and others, are crystalised in the specific syntactic form of a structured trace \item Some examples... \end{itemize} \end{frame} \begin{frame}[fragile] \frametitle{Structured trace examples I} Traces end with a return being executed, or not: \begin{lstlisting} inductive trace_ends_with_ret: Type[0] := | ends_with_ret: trace_ends_with_ret | doesnt_end_with_ret: trace_ends_with_ret. \end{lstlisting} A trace starting with a label and ending with a return: \begin{lstlisting} inductive trace_label_return (S: abstract_status): S $\rightarrow$ S $\rightarrow$ Type[0] := | tlr_base: $\forall$status_before: S. $\forall$status_after: S. trace_label_label S ends_with_ret status_before status_after $\rightarrow$ trace_label_return S status_before status_after ... \end{lstlisting} \end{frame} \begin{frame}[fragile] \frametitle{Structured trace examples II} A trace starting and ending with a cost label: \begin{lstlisting} ... with trace_label_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] := | tll_base: $\forall$ends_flag: trace_ends_with_ret. $\forall$start_status: S. $\forall$end_status: S. trace_any_label S ends_flag start_status end_status $\rightarrow$ as_costed S start_status $\rightarrow$ trace_label_label S ends_flag start_status end_status ... \end{lstlisting} \end{frame} \begin{frame}[fragile] \frametitle{Structured trace examples III} A call followed by a label on return: \begin{lstlisting} ... with trace_any_label: trace_ends_with_ret $\rightarrow$ S $\rightarrow$ S $\rightarrow$ Type[0] := ... | tal_base_call: $\forall$status_pre_fun_call: S. $\forall$status_start_fun_call: S. $\forall$status_final: S. as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$ $\forall$H:as_classifier S status_pre_fun_call cl_call. as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final $\rightarrow$ trace_label_return S status_start_fun_call status_final $\rightarrow$ as_costed S status_final $\rightarrow$ trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final ... \end{lstlisting} \end{frame} \begin{frame}[fragile] \frametitle{Structured trace examples IV} A call followed by a non-empty trace: \begin{lstlisting} ... | tal_step_call: $\forall$end_flag: trace_ends_with_ret. $\forall$status_pre_fun_call: S. $\forall$status_start_fun_call: S. $\forall$status_after_fun_call: S. $\forall$status_final: S. as_execute S status_pre_fun_call status_start_fun_call $\rightarrow$ $\forall$H:as_classifier S status_pre_fun_call cl_call. as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call $\rightarrow$ trace_label_return S status_start_fun_call status_after_fun_call $\rightarrow$ ¬ as_costed S status_after_fun_call $\rightarrow$ trace_any_label S end_flag status_after_fun_call status_final $\rightarrow$ trace_any_label S end_flag status_pre_fun_call status_final ... \end{lstlisting} \end{frame} \begin{frame} \frametitle{Static and dynamic costs I} \begin{itemize} \item Given a structured trace, we can compute its associated cost \item This is the \emph{static} cost of a program execution \item Similarly, given a program counter and a code memory (corresponding to the trace), we can compute a \emph{dynamic cost} of a simple block \item Do this by repeatedly fetching, obtaining the next instruction, and a new program counter \item This requires some predicates defining what a good program' and what a good program counter' are \end{itemize} \end{frame} \begin{frame} \frametitle{Static and dynamic costs II} \begin{itemize} \item We aim to prove that the dynamic and static cost calculations coincide \item This would imply that the static cost computation is correct \item This proof is surprisingly tricky to complete (about 3 man months of work so far) \item Is now about 95\% complete \end{itemize} \end{frame} \begin{frame} \frametitle{Changes ported to O'Caml prototype} \begin{itemize} \item Bug fixes spotted in the formalisation so far have been merged back into the O'Caml compiler \item Larger changes like the \texttt{Joint} machinery have so far not \item It is unclear whether they will be \item Just a generalisation of what is already there \item Supposed to make formalisation easier \item Further, we want to ensure that the untrusted compiler is as correct as possible, for experiments in e.g. Frama-C \item Porting a large change to the untrusted compiler would jeopardise these experiments \end{itemize} \end{frame} \begin{frame} \frametitle{Improvements in Matita} \begin{itemize} \item Part of the motivation for using Matita was for CerCo to act a stress test' \item The proofs talked about in this talk have done this \item Many improvements to Matita have been made since the last project meeting \item These include major speed-ups of e.g. printing large goals, bug fixes, the porting of CerCo code to standard library, and more options for passing to tactics \end{itemize} \end{frame} \begin{frame} \frametitle{The next period} UNIBO has following pool of remaining manpower (postdocs): \begin{center} \begin{tabular}{ll} Person & Man months remaining \\ \hline Boender & 14 months \\ Mulligan & 6 months \\ Tranquilli & 10 months \\ \end{tabular} \end{center} \begin{itemize} \item Boender finishing assembler correctness proof \item Mulligan proofs of correctness for 1 intermediate language \item Tranquilli proofs of correctness for 2 intermediate languages \item Sacerdoti Coen floating' \item Believe we have enough manpower to complete backend \end{itemize} \end{frame} \begin{frame} \frametitle{Summary} We have: \begin{itemize} \item Translated the O'Caml prototype's backend intermediate languages into Matita \item Implemented the translations between languages, and given the intermediate languages a semantics \item Refactored many of the backend intermediate languages into a common, parametric `joint' language, that is later specialised \item Spotted opportunities for possibly commuting backend translation passes \item Used six months to define structured traces and start the proof of correctness for the assembler \item Distinguished our proof from CompCert's by heavy use of dependent types throughout whole compiler \end{itemize} \end{frame} \end{document}