source: Deliverables/D1.1/Presentations/Paris presentation March 2012/WP4-dominic.tex @ 1814

\documentclass[serif]{beamer}

\usepackage[english]{babel}
\usepackage{listings}
\usepackage{microtype}

\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
\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}
XXX: todo
\end{frame}

\begin{frame}
\frametitle{Commuting passes}
XXX: todo
\end{frame}

\begin{frame}
\frametitle{Instruction selection in RTLabs}
XXX: todo
\end{frame}

\begin{frame}
\frametitle{Semantics of \texttt{Joint} I}
\end{frame}

\begin{frame}
\frametitle{Semantics of \texttt{Joint} II}
\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
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
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{`Free time'}
\begin{itemize}
\item
We had six months of `free time', time not allotted in the Contract to working on any explicit deliverable
\item
We invested this time working on:
\begin{itemize}
\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 following (standard) 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
\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
Optimality is not proved
\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 50\% of the correctness proof for the assembler
\item
Boender's work constitutes a large missing piece (modulo a few missing lemmas), but holes still remain in the main proof
\item
We abandoned this work to start on other tasks
\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}
\frametitle{Structured traces I}
\begin{itemize}
\item
We introduced a notion of `structured traces'
\item
These are intended to statically capture the execution trace of a program
\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} instruction
\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 75\% complete
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{Changes ported to O'Caml prototype}
XXX: todo
\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{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 commuting backend translation passes
\item
Used six months of `free time' to define structured traces and start the proof of correctness for the assembler
\end{itemize}
\end{frame}

\end{document}