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

Last change on this file since 637 was 637, checked in by campbell, 9 years ago

First draft of WP3 slides.

File size: 10.6 KB
Line 
1\documentclass{beamer}
2
3\usetheme{Frankfurt}
4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
5
6\usepackage[english]{babel}
7\usepackage{inputenc}
8\usepackage{listings}
9
10\lstdefinelanguage{coq}
11  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
12   morekeywords={[2]if,then,else},
13  }
14
15\lstdefinelanguage{matita}
16  {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,Type,and,on},
17   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
18   mathescape=true,
19  }
20
21\lstset{language=matita,basicstyle=\footnotesize\tt,columns=flexible,breaklines=false,
22        keywordstyle=\color{red}\bfseries,
23        keywordstyle=[2]\color{blue},
24        commentstyle=\color{green},
25        stringstyle=\color{blue},
26        showspaces=false,showstringspaces=false}
27
28\author{Brian Campbell, Randy Pollack and Ian Stark}
29\title{CerCo Work Package 3}
30\date{March 11, 2011}
31
32\begin{document}
33
34\begin{frame}
35\maketitle
36\end{frame}
37
38\begin{frame}
39\frametitle{Work Package 3}
40
41\begin{quote}
42This Work Package is devoted to the formal encoding and correctness verification of the compiler front end, from some
43abstract syntax tree representation of (a large subset of) the C language to three-address like intermediate code.
44\end{quote}
45
46\begin{description}
47\item[D3.1] Executable Formal Semantics of C
48\item[T3.2] Functional encoding in the Calculus of Inductive Constructions
49\item[T3.3] Formal semantics of intermediate languages
50\end{description}
51
52
53% introduction by quote about purpose of wp3
54% main deliverable: D3.1
55% start of T3.2, T3.3
56\end{frame}
57
58% place work to date in context of project
59
60\definecolor{lightgreen}{rgb}{.7,1,.7}
61
62\begin{frame}
63\frametitle{D3.1: C semantics}
64
65\[
66\begin{array}{r@{\ }l}
67\text{C} \Rightarrow \colorbox{yellow}{CIL parser} \Rightarrow \colorbox{yellow}{Clight}
68  & \Rightarrow \colorbox{yellow}{inductive semantics} \\
69  & \Rightarrow \colorbox{lightgreen}{executable semantics}
70\end{array}
71\]
72
73\bigskip
74
75\colorbox{yellow}{Sections ported from CompCert Coq development.} \\
76\begin{itemize}
77\item 8051 memory region extensions added.
78\item Cost labels added.
79\end{itemize}
80
81\medskip
82\colorbox{lightgreen}{New code.}
83\begin{itemize}
84\item Proven equivalent to the inductive semantics
85\end{itemize}
86\end{frame}
87
88\begin{frame}
89\frametitle{8051 memory region extensions}
90
91\begin{center}
92\scalebox{.7}{
93\setlength{\unitlength}{1pt}
94\begin{picture}(410,250)(-50,200)
95%\put(-50,200){\framebox(410,250){}}
96\put(12,410){\makebox(80,0)[b]{Internal (256B)}}
97\put(13,242){\line(0,1){165}}
98\put(93,242){\line(0,1){165}}
99\put(13,407){\line(1,0){80}}
100\put(12,400){\makebox(0,0)[r]{0h}}  \put(14,400){\makebox(0,0)[l]{Register bank 0}}
101\put(13,393){\line(1,0){80}}
102\put(12,386){\makebox(0,0)[r]{8h}}  \put(14,386){\makebox(0,0)[l]{Register bank 1}}
103\put(13,379){\line(1,0){80}}
104\put(12,372){\makebox(0,0)[r]{10h}}  \put(14,372){\makebox(0,0)[l]{Register bank 2}}
105\put(13,365){\line(1,0){80}}
106\put(12,358){\makebox(0,0)[r]{18h}} \put(14,358){\makebox(0,0)[l]{Register bank 3}}
107\put(13,351){\line(1,0){80}}
108\put(12,344){\makebox(0,0)[r]{20h}} \put(14,344){\makebox(0,0)[l]{Bit addressable}}
109\put(13,323){\line(1,0){80}}
110\put(12,316){\makebox(0,0)[r]{30h}}
111  \put(14,309){\makebox(0,0)[l]{\quad \vdots}}
112\put(13,291){\line(1,0){80}}
113\put(12,284){\makebox(0,0)[r]{80h}}
114  \put(14,263){\makebox(0,0)[l]{\quad \vdots}}
115\put(12,249){\makebox(0,0)[r]{ffh}}
116\put(13,242){\line(1,0){80}}
117
118\qbezier(-2,407)(-6,407)(-6,393)
119\qbezier(-6,393)(-6,324)(-10,324)
120\put(-12,324){\makebox(0,0)[r]{Indirect/Stack}}
121\qbezier(-6,256)(-6,324)(-10,324)
122\qbezier(-2,242)(-6,242)(-6,256)
123
124\qbezier(94,407)(98,407)(98,393)
125\qbezier(98,393)(98,349)(102,349)
126\put(104,349){\makebox(0,0)[l]{Direct}}
127\qbezier(98,305)(98,349)(102,349)
128\qbezier(94,291)(98,291)(98,305)
129
130\put(102,242){\framebox(20,49){SFR}}
131% bit access to sfrs?
132
133\qbezier(124,291)(128,291)(128,277)
134\qbezier(128,277)(128,266)(132,266)
135\put(134,266){\makebox(0,0)[l]{Direct}}
136\qbezier(128,257)(128,266)(132,266)
137\qbezier(124,242)(128,242)(128,256)
138
139\put(164,410){\makebox(80,0)[b]{External (64kB)}}
140\put(164,220){\line(0,1){187}}
141\put(164,407){\line(1,0){80}}
142\put(244,220){\line(0,1){187}}
143\put(164,242){\line(1,0){80}}
144\put(163,400){\makebox(0,0)[r]{0h}}
145\put(164,324){\makebox(80,0){Paged access}}
146  \put(164,310){\makebox(80,0){direct/indirect}}
147\put(163,235){\makebox(0,0)[r]{80h}}
148  \put(164,228){\makebox(80,0){\vdots}}
149  \put(164,210){\makebox(80,0){Direct/indirect}}
150
151\put(264,410){\makebox(80,0)[b]{Code (64kB)}}
152\put(264,220){\line(0,1){187}}
153\put(264,407){\line(1,0){80}}
154\put(344,220){\line(0,1){187}}
155\put(263,400){\makebox(0,0)[r]{0h}}
156  \put(264,228){\makebox(80,0){\vdots}}
157  \put(264,324){\makebox(80,0){Direct}}
158  \put(264,310){\makebox(80,0){PC relative}}
159\end{picture}
160}\\
161\textbf{Memory model}
162\end{center}
163
164\end{frame}
165
166\begin{frame}
167\frametitle{8051 memory region extensions}
168
169\begin{tabular}{rcl}
170Attribute & Pointer size & Memory space \\
171          &  (bytes)             & \\\hline
172\lstinline'__data' & 1 & Internal, first half (0h -- 7fh) \\
173\lstinline'__idata' & 1 & Internal, indirect only (80h -- ffh) \\
174\lstinline'__pdata' & 1 & External, page access (usually 0h -- 7fh) \\
175\lstinline'__xdata' & 2 & External, any (0h -- ffffh) \\
176\lstinline'__code' & 2 & Code, any (0h -- ffffh) \\
177\emph{none}& 3 & Any / Generic pointer
178\end{tabular}
179
180\bigskip
181\begin{itemize}
182\item Reuse syntax from \texttt{sdcc} compiler for compatibility.
183\item No support for direct access to registers, bits, etc.
184\end{itemize}
185
186\end{frame}
187
188\begin{frame}
189\frametitle{Port of CompCert semantics: CIL parser}
190\[ \text{C} \Rightarrow \text{CIL parser} \Rightarrow \text{Clight} \]
191
192\bigskip
193\begin{overprint}
194\onslide<1>
195\begin{itemize}
196\item Clight is a C-like language
197\item starting point of formal development
198\item[$\triangleright$] deterministic
199\item[$\triangleright$] side-effect free expressions
200\item[$\triangleright$] explicit casting
201\end{itemize}
202
203CIL parser provides semi-formal C semantics by translation to Clight
204
205\onslide<2>
206CIL parser essentially the same as CompCert, plus
207\begin{itemize}
208\item parsing of memory region extensions
209\item memory regions tracked during elaboration to provide extra type
210      information
211\end{itemize}
212\end{overprint}
213
214% maybe example
215%  - of clight?
216%  - of elab (for type of &e need to know region of e)
217
218\end{frame}
219
220\begin{frame}[fragile]
221\frametitle{Port of CompCert semantics: Clight inductive semantics}
222\alt<1>{CompCert provides a small-step semantics for Clight (in Coq)}
223{We provide a small-step semantics for Clight (in Matita)}
224\begin{overprint}
225\onslide<1-2>
226\begin{itemize}
227\item executable memory model, maps, etc
228\item operations defined by functions
229\item relations for casts, expressions (`lvalues' and `rvalues')
230      and statements
231\end{itemize}
232
233\onslide<3>
234\bigskip
235\textbf{Not so easy} --- no sections, different library, bugs\dots
236\end{overprint}
237
238\begin{overprint}
239\onslide<1>
240\begin{lstlisting}[language=Coq]
241Inductive eval_expr: expr -> val -> Prop :=
242
243...
244  | eval_Elvalue: forall a ty loc ofs v,
245      eval_lvalue (Expr a ty) loc ofs ->
246      load_value_of_type ty m loc ofs = Some v ->
247      eval_expr (Expr a ty) v
248\end{lstlisting}
249
250\onslide<2-3>
251\begin{lstlisting}
252ninductive eval_expr (ge:genv) (e:env) (m:mem) :
253   expr $\rightarrow$ val $\rightarrow$ trace $\rightarrow$ Prop :=
254...
255  | eval_Elvalue: $\forall$a,ty,psp,loc,ofs,v,tr.
256      eval_lvalue ge e m (Expr a ty) psp loc ofs tr $\rightarrow$
257      load_value_of_type ty m psp loc ofs = Some ? v $\rightarrow$
258      eval_expr ge e m (Expr a ty) v tr
259\end{lstlisting}
260\end{overprint}
261
262\end{frame}
263
264\begin{frame}[fragile]
265\frametitle{Clight executable semantics}
266
267Input in the inductive semantics is treated non-deterministically:
268\begin{itemize}
269\item execution derivation includes arbitrary input value
270\item program behaviour may not be defined on all inputs
271\end{itemize}
272
273For the executable semantics, we use resumptions
274\begin{itemize}
275\item return suspended semantics as a function of the input value
276\item combined resumption + error monad
277\item lift properties over arbitrary values where appropriate:
278\end{itemize}
279\begin{lstlisting}
280nlet rec P_io O I (A:Type) (P:A $\rightarrow$ Prop) (v:IO O I A) on v : Prop :=
281match v return $\lambda$_.Prop with
282[ Wrong $\Rightarrow$ True
283| Value z $\Rightarrow$ P z
284| Interact out k $\Rightarrow$ $\forall$v'.P_io O I A P (k v')
285].
286\end{lstlisting}
287\end{frame}
288
289\begin{frame}[fragile]
290\frametitle{Clight executable semantics}
291
292Follows the (largely syntax-directed) inductive semantics closely.
293\begin{itemize}
294\item rearranged around pattern matching
295\end{itemize}
296\begin{lstlisting}
297nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val$\times$trace) ≝
298match e with
299[ Expr e' ty $\Rightarrow$
300  match e' with
301  [ ...
302  | Evar _ $\Rightarrow$
303      do $\langle$l,tr$\rangle$ $\leftarrow$ exec_lvalue' ge en m e' ty;
304      do v $\leftarrow$ opt_to_res ? (load_value_of_type' ty m l);
305      OK ? $\langle$v,tr$\rangle$
306...
307\end{lstlisting}
308
309A cofixpoint gives a stream of $\langle$trace, state$\rangle$ pairs for whole
310executions.
311
312% executable semantics
313
314\end{frame}
315
316\begin{frame}
317\frametitle{Validation: proof}
318
319Have shown inductive and executable semantics equivalent:
320\begin{itemize}
321\item single-step soundness and completeness straightforward
322\item experimented with requiring soundness in result type
323  \begin{itemize}
324  \item[$\triangleright$] proof terms get in the way later on
325  \end{itemize}
326\item Full executions tricker --- final result requires ability to
327      commit to (non-)termination
328  \begin{itemize}
329  \item[$\triangleright$] reusing commitment technique from CompCert made
330    proof tractable
331  \end{itemize}
332\end{itemize}
333
334\end{frame}
335
336\begin{frame}
337\frametitle{Validation: testing}
338
339Executing C programs using the semantics is feasible
340\begin{itemize}
341\item use CIL parser to produce Matita Clight AST
342\item feed AST to executable semantics
343\item extract state at $n$th step and normalise term
344\end{itemize}
345
346Labour intensive --- so only light, targeted testing until we have program
347extraction.
348
349\end{frame}
350% demo would come here, if at all
351
352\begin{frame}
353\frametitle{T3.2 / T3.3}
354Started after D3.1 delivery.
355\begin{description}
356\item[T3.2] Functional encoding in the Calculus of Inductive Constructions
357\item[T3.3] Formal semantics of intermediate languages
358\end{description}
359
360\bigskip
361Begun work with
362\begin{itemize}
363\item Harmonisation of common code
364  \begin{itemize}
365  \item with D4.1, e.g. representation of the integers
366  \item with prototype, e.g. bugs found with pointer regions
367  \end{itemize}
368\item Started construction of RTLabs semantics
369  \begin{itemize}
370  \item Need to start RTL languages early as they cross between the front and
371        back end
372  \end{itemize}
373\end{itemize}
374
375\end{frame}
376
377% maybe something about post 3.1
378
379\end{document}
Note: See TracBrowser for help on using the repository browser.