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

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

Small additions to WP3 slides.

File size: 11.1 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,forall,Prop},
13  }
14
15\lstdefinelanguage{matita}
16  {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,and,on,return},
17   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct,Prop,Type},
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 Proved 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
237\begin{itemize}
238\item[$\triangleright$] Also additional trace for cost labels
239\end{itemize}
240\end{overprint}
241
242\begin{overprint}
243\onslide<1>
244\begin{lstlisting}[language=Coq]
245Inductive eval_expr: expr -> val -> Prop :=
246
247...
248  | eval_Elvalue: forall a ty loc ofs v,
249      eval_lvalue (Expr a ty) loc ofs ->
250      load_value_of_type ty m loc ofs = Some v ->
251      eval_expr (Expr a ty) v
252\end{lstlisting}
253
254\onslide<2-3>
255\begin{lstlisting}
256ninductive eval_expr (ge:genv) (e:env) (m:mem) :
257   expr $\rightarrow$ val $\rightarrow$ trace $\rightarrow$ Prop :=
258...
259  | eval_Elvalue: $\forall$a,ty,psp,loc,ofs,v,tr.
260      eval_lvalue ge e m (Expr a ty) psp loc ofs tr $\rightarrow$
261      load_value_of_type ty m psp loc ofs = Some ? v $\rightarrow$
262      eval_expr ge e m (Expr a ty) v tr
263\end{lstlisting}
264\end{overprint}
265
266\end{frame}
267
268\begin{frame}[fragile]
269\frametitle{Clight executable semantics}
270
271Input in the inductive semantics is treated non-deterministically:
272\begin{itemize}
273\item execution derivation includes arbitrary input value
274\item program behaviour may not be defined on all inputs
275\end{itemize}
276
277For the executable semantics, we use resumptions
278\begin{itemize}
279\item return suspended semantics as a function of the input value
280\item combined resumption + error monad
281\item lift properties over arbitrary values where appropriate:
282\end{itemize}
283\begin{lstlisting}
284nlet rec P_io O I (A:Type) (P:A $\rightarrow$ Prop) (v:IO O I A) on v : Prop :=
285match v return $\lambda$_.Prop with
286[ Wrong $\Rightarrow$ True
287| Value z $\Rightarrow$ P z
288| Interact out k $\Rightarrow$ $\forall$v'.P_io O I A P (k v')
289].
290\end{lstlisting}
291\end{frame}
292
293\begin{frame}[fragile]
294\frametitle{Clight executable semantics}
295
296Follows the (largely syntax-directed) inductive semantics closely.
297\begin{itemize}
298\item rearranged around pattern matching
299\end{itemize}
300\begin{lstlisting}
301nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val$\times$trace) ≝
302match e with
303[ Expr e' ty $\Rightarrow$
304  match e' with
305  [ ...
306  | Evar _ $\Rightarrow$
307      do $\langle$l,tr$\rangle$ $\leftarrow$ exec_lvalue' ge en m e' ty;
308      do v $\leftarrow$ opt_to_res ? (load_value_of_type' ty m l);
309      OK ? $\langle$v,tr$\rangle$
310...
311\end{lstlisting}
312
313A cofixpoint gives a stream of $\langle$trace, state$\rangle$ pairs for whole
314executions.
315
316% executable semantics
317
318\end{frame}
319
320\begin{frame}
321\frametitle{Validation: proof}
322
323Have shown inductive and executable semantics equivalent:
324\begin{itemize}
325\item single-step soundness and completeness straightforward
326\item experimented with requiring soundness in result type
327  \begin{itemize}
328  \item[$\triangleright$] proof terms get in the way later on
329  \item[$\triangleright$] providing separate theorems easier
330  \end{itemize}
331\item Full executions trickier --- final result requires ability to
332      commit to (non-)termination
333  \begin{itemize}
334  \item[$\triangleright$] reusing commitment technique from CompCert made
335    proof tractable
336  \end{itemize}
337\end{itemize}
338
339\end{frame}
340
341\begin{frame}
342\frametitle{Validation: testing}
343
344Executing C programs using the semantics is feasible
345\begin{itemize}
346\item use CIL parser to produce Matita Clight AST
347\item feed AST to executable semantics
348\item extract state at $n$th step and normalise term
349\end{itemize}
350
351Labour intensive --- so only light, targeted testing until we have program
352extraction.
353
354\bigskip
355\textbf{Demo}
356
357\end{frame}
358
359\begin{frame}
360\frametitle{D3.1 summary}
361
362C semantics produced by
363\begin{itemize}
364\item using CIL and ported inductive semantics from CompCert,
365\item adding 8051 memory extensions,
366\item writing executable semantics,
367\item proving inductive and executable semantics equivalent,
368\item executable testing.
369\end{itemize}
370\end{frame}
371
372\begin{frame}
373\frametitle{T3.2 / T3.3}
374Started after D3.1 delivery.
375\begin{description}
376\item[T3.2] Functional encoding in the Calculus of Inductive Constructions
377\item[T3.3] Formal semantics of intermediate languages
378\end{description}
379
380\bigskip
381Begun work with
382\begin{itemize}
383\item Harmonisation of common code
384  \begin{itemize}
385  \item with D4.1, e.g. representation of the integers
386  \item with prototype, e.g. bugs found with pointer regions
387  \end{itemize}
388\item Started construction of RTLabs semantics
389  \begin{itemize}
390  \item Need to start RTL languages early as they cross between the front and
391        back end
392  \end{itemize}
393\end{itemize}
394
395\end{frame}
396
397% maybe something about post 3.1
398
399\end{document}
Note: See TracBrowser for help on using the repository browser.