source: Deliverables/D1.1/Presentations/WP3-brian.tex @ 649

\documentclass{beamer}

\usetheme{Frankfurt}
\logo{\includegraphics[height=1.0cm]{fetopen.png}}

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

\lstdefinelanguage{coq}
  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
   morekeywords={[2]if,then,else,forall,Prop},
  }

\lstdefinelanguage{matita}
  {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,and,on,return},
   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct,Prop,Type},
   mathescape=true,
  }

\lstset{language=matita,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
        keywordstyle=\color{red}\bfseries,
        keywordstyle=[2]\color{blue},
        commentstyle=\color{green},
        stringstyle=\color{blue},
        showspaces=false,showstringspaces=false}

\author{Brian Campbell, Randy Pollack and Ian Stark}
\title{CerCo Work Package 3}
\date{March 11, 2011}

\begin{document}

\begin{frame}
\maketitle
\end{frame}

\begin{frame}
\frametitle{Work Package 3}

\begin{quote}
This Work Package is devoted to the formal encoding and correctness verification of the compiler front end, from some
abstract syntax tree representation of (a large subset of) the C language to three-address like intermediate code.
\end{quote}

\begin{description}
\item[D3.1] Executable Formal Semantics of C
\item[T3.2] Functional encoding in the Calculus of Inductive Constructions
\item[T3.3] Formal semantics of intermediate languages
\end{description}


% introduction by quote about purpose of wp3
% main deliverable: D3.1
% start of T3.2, T3.3
\end{frame}

% place work to date in context of project

\definecolor{lightgreen}{rgb}{.7,1,.7}

\begin{frame}
\frametitle{D3.1: C semantics}

\[
\begin{array}{r@{\ }l}
\text{C} \Rightarrow \colorbox{yellow}{CIL parser} \Rightarrow \colorbox{yellow}{Clight}
  & \Rightarrow \colorbox{yellow}{inductive semantics} \\
  & \Rightarrow \colorbox{lightgreen}{executable semantics}
\end{array}
\]

\bigskip

\colorbox{yellow}{Sections ported from CompCert Coq development.} \\
\begin{itemize}
\item 8051 memory region extensions added.
\item Cost labels added.
\end{itemize}

\medskip
\colorbox{lightgreen}{New code.}
\begin{itemize}
\item Proved equivalent to the inductive semantics
\end{itemize}
\end{frame}

\begin{frame}
\frametitle{8051 memory region extensions}

\begin{center}
\scalebox{.7}{
\setlength{\unitlength}{1pt}
\begin{picture}(410,250)(-50,200)
%\put(-50,200){\framebox(410,250){}}
\put(12,410){\makebox(80,0)[b]{Internal (256B)}}
\put(13,242){\line(0,1){165}}
\put(93,242){\line(0,1){165}}
\put(13,407){\line(1,0){80}}
\put(12,400){\makebox(0,0)[r]{0h}}  \put(14,400){\makebox(0,0)[l]{Register bank 0}}
\put(13,393){\line(1,0){80}}
\put(12,386){\makebox(0,0)[r]{8h}}  \put(14,386){\makebox(0,0)[l]{Register bank 1}}
\put(13,379){\line(1,0){80}}
\put(12,372){\makebox(0,0)[r]{10h}}  \put(14,372){\makebox(0,0)[l]{Register bank 2}}
\put(13,365){\line(1,0){80}}
\put(12,358){\makebox(0,0)[r]{18h}} \put(14,358){\makebox(0,0)[l]{Register bank 3}}
\put(13,351){\line(1,0){80}}
\put(12,344){\makebox(0,0)[r]{20h}} \put(14,344){\makebox(0,0)[l]{Bit addressable}}
\put(13,323){\line(1,0){80}}
\put(12,316){\makebox(0,0)[r]{30h}}
  \put(14,309){\makebox(0,0)[l]{\quad \vdots}}
\put(13,291){\line(1,0){80}}
\put(12,284){\makebox(0,0)[r]{80h}}
  \put(14,263){\makebox(0,0)[l]{\quad \vdots}}
\put(12,249){\makebox(0,0)[r]{ffh}}
\put(13,242){\line(1,0){80}}

\qbezier(-2,407)(-6,407)(-6,393)
\qbezier(-6,393)(-6,324)(-10,324)
\put(-12,324){\makebox(0,0)[r]{Indirect/Stack}}
\qbezier(-6,256)(-6,324)(-10,324)
\qbezier(-2,242)(-6,242)(-6,256)

\qbezier(94,407)(98,407)(98,393)
\qbezier(98,393)(98,349)(102,349)
\put(104,349){\makebox(0,0)[l]{Direct}}
\qbezier(98,305)(98,349)(102,349)
\qbezier(94,291)(98,291)(98,305)

\put(102,242){\framebox(20,49){SFR}}
% bit access to sfrs?

\qbezier(124,291)(128,291)(128,277)
\qbezier(128,277)(128,266)(132,266)
\put(134,266){\makebox(0,0)[l]{Direct}}
\qbezier(128,257)(128,266)(132,266)
\qbezier(124,242)(128,242)(128,256)

\put(164,410){\makebox(80,0)[b]{External (64kB)}}
\put(164,220){\line(0,1){187}}
\put(164,407){\line(1,0){80}}
\put(244,220){\line(0,1){187}}
\put(164,242){\line(1,0){80}}
\put(163,400){\makebox(0,0)[r]{0h}}
\put(164,324){\makebox(80,0){Paged access}}
  \put(164,310){\makebox(80,0){direct/indirect}}
\put(163,235){\makebox(0,0)[r]{80h}}
  \put(164,228){\makebox(80,0){\vdots}}
  \put(164,210){\makebox(80,0){Direct/indirect}}

\put(264,410){\makebox(80,0)[b]{Code (64kB)}}
\put(264,220){\line(0,1){187}}
\put(264,407){\line(1,0){80}}
\put(344,220){\line(0,1){187}}
\put(263,400){\makebox(0,0)[r]{0h}}
  \put(264,228){\makebox(80,0){\vdots}}
  \put(264,324){\makebox(80,0){Direct}}
  \put(264,310){\makebox(80,0){PC relative}}
\end{picture}
}\\
\textbf{Memory model}
\end{center}

\end{frame}

\begin{frame}
\frametitle{8051 memory region extensions}

\begin{tabular}{rcl}
Attribute & Pointer size & Memory space \\
          &  (bytes)             & \\\hline
\lstinline'__data' & 1 & Internal, first half (0h -- 7fh) \\
\lstinline'__idata' & 1 & Internal, indirect only (80h -- ffh) \\
\lstinline'__pdata' & 1 & External, page access (usually 0h -- 7fh) \\
\lstinline'__xdata' & 2 & External, any (0h -- ffffh) \\
\lstinline'__code' & 2 & Code, any (0h -- ffffh) \\
\emph{none}& 3 & Any / Generic pointer
\end{tabular}

\bigskip
\begin{itemize}
\item Reuse syntax from \texttt{sdcc} compiler for compatibility.
\item No support for direct access to registers, bits, etc.
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Port of CompCert semantics: CIL parser}
\[ \text{C} \Rightarrow \text{CIL parser} \Rightarrow \text{Clight} \]

\bigskip
\begin{overprint}
\onslide<1>
\begin{itemize}
\item Clight is a C-like language
\item starting point of formal development
\item[$\triangleright$] deterministic
\item[$\triangleright$] side-effect free expressions
\item[$\triangleright$] explicit casting
\end{itemize}

CIL parser provides semi-formal C semantics by translation to Clight

\onslide<2>
CIL parser essentially the same as CompCert, plus
\begin{itemize}
\item parsing of memory region extensions
\item memory regions tracked during elaboration to provide extra type
      information
\end{itemize}
\end{overprint}

% maybe example
%  - of clight?
%  - of elab (for type of &e need to know region of e)

\end{frame}

\begin{frame}[fragile]
\frametitle{Port of CompCert semantics: Clight inductive semantics}
\alt<1>{CompCert provides a small-step semantics for Clight (in Coq)}
{We provide a small-step semantics for Clight (in Matita)}
\begin{overprint}
\onslide<1-2>
\begin{itemize}
\item executable memory model, maps, etc
\item operations defined by functions
\item relations for casts, expressions (`lvalues' and `rvalues')
      and statements
\end{itemize}

\onslide<3>
\bigskip
\textbf{Not so easy} --- no sections, different library, bugs\dots
\end{overprint}

\begin{overprint}
\onslide<1>
\begin{lstlisting}[language=Coq]
Inductive eval_expr: expr -> val -> Prop :=

...
  | eval_Elvalue: forall a ty loc ofs v,
      eval_lvalue (Expr a ty) loc ofs ->
      load_value_of_type ty m loc ofs = Some v ->
      eval_expr (Expr a ty) v
\end{lstlisting}

\onslide<2-3>
\begin{lstlisting}
ninductive eval_expr (ge:genv) (e:env) (m:mem) :
   expr $\rightarrow$ val $\rightarrow$ trace $\rightarrow$ Prop :=
...
  | eval_Elvalue: $\forall$a,ty,psp,loc,ofs,v,tr.
      eval_lvalue ge e m (Expr a ty) psp loc ofs tr $\rightarrow$
      load_value_of_type ty m psp loc ofs = Some ? v $\rightarrow$
      eval_expr ge e m (Expr a ty) v tr
\end{lstlisting}
\end{overprint}

\end{frame}

\begin{frame}[fragile]
\frametitle{Clight executable semantics}

Input in the inductive semantics is treated non-deterministically:
\begin{itemize}
\item execution derivation includes arbitrary input value
\item program behaviour may not be defined on all inputs
\end{itemize}

For the executable semantics, we use resumptions
\begin{itemize}
\item return suspended semantics as a function of the input value
\item combined resumption + error monad
\item lift properties over arbitrary values where appropriate:
\end{itemize}
\begin{lstlisting}
nlet rec P_io O I (A:Type) (P:A $\rightarrow$ Prop) (v:IO O I A) on v : Prop :=
match v return $\lambda$_.Prop with
[ Wrong $\Rightarrow$ True
| Value z $\Rightarrow$ P z
| Interact out k $\Rightarrow$ $\forall$v'.P_io O I A P (k v')
].
\end{lstlisting}
\end{frame}

\begin{frame}[fragile]
\frametitle{Clight executable semantics}

Follows the (largely syntax-directed) inductive semantics closely.
\begin{itemize}
\item rearranged around pattern matching
\end{itemize}
\begin{lstlisting}
nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val$\times$trace) ≝
match e with
[ Expr e' ty $\Rightarrow$
  match e' with
  [ ...
  | Evar _ $\Rightarrow$
      do $\langle$l,tr$\rangle$ $\leftarrow$ exec_lvalue' ge en m e' ty;
      do v $\leftarrow$ opt_to_res ? (load_value_of_type' ty m l);
      OK ? $\langle$v,tr$\rangle$
...
\end{lstlisting}

A cofixpoint gives a stream of $\langle$trace, state$\rangle$ pairs for whole
executions.

% executable semantics

\end{frame}

\begin{frame}
\frametitle{Validation: proof}

Have shown inductive and executable semantics equivalent:
\begin{itemize}
\item single-step soundness and completeness straightforward
\item experimented with requiring soundness in result type
  \begin{itemize}
  \item[$\triangleright$] proof terms get in the way later on
  \item[$\triangleright$] providing separate theorems easier
  \end{itemize}
\item Full executions trickier --- final result requires ability to
      commit to (non-)termination
  \begin{itemize}
  \item[$\triangleright$] reusing commitment technique from CompCert made
    proof tractable
  \end{itemize}
\end{itemize}

\end{frame}

\begin{frame}
\frametitle{Validation: testing}

Executing C programs using the semantics is feasible
\begin{itemize}
\item use CIL parser to produce Matita Clight AST
\item feed AST to executable semantics
\item extract state at $n$th step and normalise term
\end{itemize}

Labour intensive --- so only light, targeted testing until we have program
extraction.

\end{frame}
% demo would come here, if at all

\begin{frame}
\frametitle{T3.2 / T3.3}
Started after D3.1 delivery.
\begin{description}
\item[T3.2] Functional encoding in the Calculus of Inductive Constructions
\item[T3.3] Formal semantics of intermediate languages
\end{description}

\bigskip
Begun work with
\begin{itemize}
\item Harmonisation of common code
  \begin{itemize}
  \item with D4.1, e.g. representation of the integers
  \item with prototype, e.g. bugs found with pointer regions
  \end{itemize}
\item Started construction of RTLabs semantics
  \begin{itemize}
  \item Need to start RTL languages early as they cross between the front and
        back end
  \end{itemize}
\end{itemize}

\end{frame}

% maybe something about post 3.1

\end{document}