source: Deliverables/D1.1/Presentations/WP4-dominic.tex @ 672

Last change on this file since 672 was 669, checked in by mulligan, 9 years ago

Fixed man months

File size: 7.0 KB
Line 
1\documentclass{beamer}
2
3\usetheme{Frankfurt}
4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
5
6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{amssymb}
9\usepackage[english]{babel}
10\usepackage{color}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{stmaryrd}
14% \usepackage{microtype}
15
16\author{Dominic P. Mulligan}
17\title{CerCo Work Package 4}
18\date{March 11, 2011}
19
20\setlength{\parskip}{1em}
21
22\lstdefinelanguage{matita-ocaml}
23  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
24   morekeywords={[2]whd,normalize,elim,cases,destruct},
25   morekeywords={[3]type,of,val,assert,let,function},
26   mathescape=true,
27  }
28\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
29        keywordstyle=\color{red}\bfseries,
30        keywordstyle=[2]\color{blue},
31        keywordstyle=[3]\color{blue}\bfseries,
32        commentstyle=\color{green},
33        stringstyle=\color{blue},
34        showspaces=false,showstringspaces=false}
35
36\begin{document}
37
38\begin{frame}
39\maketitle
40\end{frame}
41
42\begin{frame}
43\frametitle{Work Package 4}
44\begin{itemize}
45\item
46Task 4.1: Executable semantics of machine code (D4.1, month 10).
47\item
48Task 4.2: Functional encoding in Calculus of Inductive Constructions (D4.2, month 18).
49\item
50Task 4.3: Formal semantics of intermediate languages (D4.3, month 18).
51\item
52Task 4.4: Correctness proofs (D4.4, month 36).
53\end{itemize}
54Only Task 4.1 was active.  Delivered O'Caml and Matita formalisations of MCS-51 processor.
55\end{frame}
56
57\begin{frame}
58\frametitle{People involved}
59\begin{tabular}{lll}
60Name & Position & Man months \\
61\hline
62Dominic Mulligan & Postdoc & 5 man months \\
63Claudio Sacerdoti Coen & Assistant Professor & 1 man month
64\end{tabular}
65\end{frame}
66
67\begin{frame}
68\frametitle{The MCS-51 microprocessor I}
69\begin{itemize}
70\item
71Commonly called the 8051 (has an immediate successor in the 8052).
72\item
73Popular 8-bit microprocessor from the late 1970s.
74\item
75Widely used and manufactured.
76\item
77Relatively simple microprocessor (especially suited for CerCo).
78\item
79Can accurately predict timing information in cycles.
80\end{itemize}
81\end{frame}
82
83\begin{frame}
84\frametitle{The MCS-51 microprocessor II}
85\begin{itemize}
86\item
87No exhaustive introduction.
88Reveal enough to understand what problems we faced.
89\item
90Byzantine memory model.
91\item
92Overlap, have different sizes, may not be present depending on model, addressed in multiple ways, addressed with different sized pointers.
93\item
94Non-orthogonal instruction set.
95\texttt{MOV} takes 16 combinations of addressing mode (possible 300+)s.
96\end{itemize}
97\end{frame}
98
99\begin{frame}
100\frametitle{The MCS-51 microprocessor III}
101\begin{itemize}
102\item
103Three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used).
104\item
105Differ in the size of permissible offset and the size in bytes of instruction.
106\item
107Also has various timers, UART I/O and interrupts.
1088052 adds additional timers.
109\item
110Interrupts are simple.
111Flags can be used to manually handle errors.
112\end{itemize}
113\end{frame}
114
115\begin{frame}
116\frametitle{Development strategy}
117\begin{itemize}
118\item
119Have two emulators.
120\item
121First in O'Caml.
122`Iron out' issues.
123\item
124I/O for debugging purposes.
125\item
126Then we moved to Matita.
127Lexically similar to O'Caml: code copy-pasted.
128\end{itemize}
129\end{frame}
130
131\begin{frame}
132\frametitle{Dealing with the jumps}
133\begin{itemize}
134\item
135Unconditional jumps: offset computed ahead of time.
136\item
137Problems: separate compilation, prototype C compiler.
138\item
139Add pseudoinstructions and `assemble away'.
140\item
141Introduce labels and cost labels (for cost traces).
142\item
143Introduce pseudoinstructions.
144\texttt{Jump}: unconditional jump to labels.
145\item
146Other pseudoinstructions introduced: \texttt{Mov} moves (16 bit) data stored at a label (global vars).
147Conditional jumps to labels.
148\item
149Assembly language similar to that of SDCC.
150\end{itemize}
151\end{frame}
152
153\begin{frame}[fragile]
154\frametitle{Polymorphic variants and phantom types}
155Instruction set is highly non-orthogonal.
156Polymorphic variants and phantom types used to capture this non-orthogonality.
157For instance:
158
159\begin{small}
160\begin{lstlisting}
161type direct = [ `DIRECT of byte ]
162type indirect = [ `INDIRECT of bit ]
163...
164type 'addr preinstruction =
165 [ `ADD of acc * [ reg | direct | indirect | data ]
166...
167 | `MOV of
168    (acc * [ reg | direct | indirect | data ],
169     [ reg | indirect ] * [ acc | direct | data ],
170     direct * [ acc | reg | direct | indirect | data ], ...)
171...
172\end{lstlisting}
173\end{small}
174\end{frame}
175
176\begin{frame}[fragile]
177\frametitle{Use of dependent types I}
178Worked well in O'Caml, Matita does not have polymorphic variants.
179We use dependent types.
180
181Introduce a type for addressing modes:
182\begin{small}
183\begin{lstlisting}
184inductive addressing_mode: Type[0] :=
185  DIRECT: Byte $\rightarrow$ addressing_mode
186...
187\end{lstlisting}
188\end{small}
189Another type \texttt{addressing\_mode\_tag} of `tags'.
190Constructors are in correspondence with those of \texttt{addressing\_mode}.
191\end{frame}
192
193\begin{frame}[fragile]
194\frametitle{Use of dependent types II}
195Use vectors of \texttt{addressing\_mode\_tag}s in type signatures for instructions.
196For instance:
197\begin{small}
198\begin{lstlisting}
199inductive preinstruction (A: Type[0]): Type[0] :=
200   ADD: $\llbracket$ acc_a $\rrbracket$
201        $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$
202        $\rightarrow$ preinstruction A
203...
204\end{lstlisting}
205\end{small}
206We need: an \emph{ad hoc} $\Sigma$ type and two coercions.
207One coercion opens up a proof obligation when it is used.
208Requires some lemmas.
209
210Lemmas and automation close proof obligations generated (300+ in typechecking interpreter function).
211\end{frame}
212
213\begin{frame}
214\frametitle{Overlapping memory spaces and addressing modes}
215\begin{itemize}
216\item
217Memory spaces overlap, can be addressed with different modes and pointers.
218\item
219`Status' record models memory as disjoint spaces.
220\item
221`Tries with holes' datastructure (dependent types).
222\item
223Complications with overlapping handled by \texttt{set\_arg\_XX} and \texttt{get\_arg\_XX} for \texttt{XX} = 1, 8, 16.
224\item
225Make use of dependent type trick.
226\end{itemize}
227\end{frame}
228
229\begin{frame}
230\frametitle{Validation}
231We worked hard to make sure we implemented a MCS-51 emulator:
232\begin{itemize}
233\item
234Multiple data sheets from different manufacturers (errors found!)
235\item
236Output to Intel HEX.
237Loading into third party tools.
238\item
239O'Caml trace files with processor status after every execution step.
240Every opcode tested.
241\item
242Matita formalisation is also executable.
243\item
244Traces can be compared with O'Caml.
245\end{itemize}
246\end{frame}
247
248\begin{frame}
249\frametitle{What is implemented}
250\begin{itemize}
251\item
252In O'Caml: emulator proper, associated assembler, supprting debugging code (Intel HEX), (untested) code for timers, interrupts and I/O.
253\item
254In Matita: emulator proper and associated assembler.
255\item
256Yet to port the timers and I/O, preferring to focus on the core emulator.
257\end{itemize}
258\end{frame}
259
260\begin{frame}
261\frametitle{Demo}
262\end{frame}
263
264\end{document}
Note: See TracBrowser for help on using the repository browser.