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

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

Use better titles for T3.2/3.3.

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] CIC encoding: Front-end
49\item[T3.3] Executable Formal Semantics of front end 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 and cost labels,
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] CIC encoding: Front-end
377\item[T3.3] Executable Formal Semantics of front end 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.