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

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

Changes to presentation that claudio wanted

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