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

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

Finished slides.

File size: 7.4 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 and Claudio Sacerdoti Coen}
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\end{frame}
45
46\begin{frame}
47\frametitle{The MCS-51 microprocessor I}
48\begin{itemize}
49\item
50MCS-51 is our target processor.
51Commonly called the 8051 (has an immediate successor in the 8052).
52\item
53A popular 8-bit microprocessor introduced by Intel in the late 1970s.
54\item
55Still widely used in embedded systems, and widely manufactured (including within the EU).
56\item
57Is a relatively simple microprocessor especially suited to CerCo's aims.
58\item
59We can accurately predict how long an instruction will take to execute in cycles (i.e. no pipelining, caching etc.)
60We use timings from a Siemen's datasheet.
61Vary between manufacturers and models.
62\end{itemize}
63\end{frame}
64
65\begin{frame}
66\frametitle{The MCS-51 microprocessor II}
67\begin{itemize}
68\item
69I will not give an exhaustive introduction to the processor.
70I am going to reveal enough for you to understand what problems we faced in formalising it.
71\item
72The MCS-51 has a byzantine memory model.
73\item
74Memory spaces overlap, have different sizes, may not be present depending on model, can be addressed in multiple ways, and addressed with different sized pointers.
75\item
76Instruction set is non-orthogonal.
77For instance, \texttt{MOV} can take 16 combinations of addressing mode out of a possible 300+.
78\end{itemize}
79\end{frame}
80
81\begin{frame}
82\frametitle{The MCS-51 microprocessor III}
83\begin{itemize}
84\item
85Instruction set contains three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used).
86\item
87These differ in the size of permissible offset and the size in bytes of instruction.
88\item
89MCS-51 also has various timers, UART I/O and interrupts.
90Succesor 8052 adds additional timers.
91\item
92Interrupts are simpler than a modern processor, as flags can be used to manually handle errors.
93\end{itemize}
94\end{frame}
95
96\begin{frame}
97\frametitle{Development strategy}
98We built two emulators for the processor.
99
100The first was written in O'Caml.
101This allowed us to `iron out' issues in the design and implementation, and make rapid changes in O'Caml's more permissive type system.
102We made use of O'Caml's ability to perform I/O for debugging purposes.
103
104When we were happy with the O'Caml emulator, we moved to Matita.
105Matita's language is lexically similar to O'Caml, so swathes of code could be copy-pasted with little additional effort.
106\end{frame}
107
108\begin{frame}
109\frametitle{Dealing with the jumps}
110\begin{itemize}
111\item
112Unconditional jumps a problem, as offset has to be computed ahead of time.
113\item
114This is problematic for separate compilation, and also for prototype C compiler.
115\item
116Much better to implement pseudoinstructions which are `assembled away'.
117\item
118Introduce labels and cost labels (for cost traces).
119\item
120Then introduce pseudoinstructions like \texttt{Jump} for unconditional jumping to labels: no offset calculation required beforehand.
121\item
122Other pseudoinstructions introduced: \texttt{Mov} for moving arbitrary (16 bit) data stored at a label (global vars) and conditional jumps to labels.
123\item
124Our assembly language similar to that of SDCC.
125\end{itemize}
126\end{frame}
127
128\begin{frame}[fragile]
129\frametitle{Polymorphic variants and phantom types}
130The instruction set is highly non-orthogonal.
131We used polymorphic variants and phantom types to capture this non-orthogonality in the type system.
132For instance:
133
134\begin{small}
135\begin{lstlisting}
136type direct = [ `DIRECT of byte ]
137type indirect = [ `INDIRECT of bit ]
138...
139type 'addr preinstruction =
140 [ `ADD of acc * [ reg | direct | indirect | data ]
141...
142 | `MOV of
143    (acc * [ reg | direct | indirect | data ],
144     [ reg | indirect ] * [ acc | direct | data ],
145     direct * [ acc | reg | direct | indirect | data ], ...)
146...
147\end{lstlisting}
148\end{small}
149\end{frame}
150
151\begin{frame}[fragile]
152\frametitle{Use of dependent types I}
153This approach worked well in O'Caml, but Matita does not have polymorphic variants, so we need a substitute.
154We use dependent types.
155
156Introduce a type for addressing modes:
157\begin{small}
158\begin{lstlisting}
159inductive addressing_mode: Type[0] :=
160  DIRECT: Byte $\rightarrow$ addressing_mode
161...
162\end{lstlisting}
163\end{small}
164And another type \texttt{addressing\_mode\_tag} of `tags' whose constructors are in correspondence with those of \texttt{addressing\_mode}.
165\end{frame}
166
167\begin{frame}[fragile]
168\frametitle{Use of dependent types II}
169We use vectors of \texttt{addressing\_mode\_tag}s in our type signatures for instructions.
170For instance:
171\begin{small}
172\begin{lstlisting}
173inductive preinstruction (A: Type[0]): Type[0] :=
174   ADD: $\llbracket$ acc_a $\rrbracket$
175        $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$
176        $\rightarrow$ preinstruction A
177...
178\end{lstlisting}
179\end{small}
180We need: an \emph{ad hoc} $\Sigma$ type and two coercions.
181One coercion automatically opens up a proof obligation when it is used, which requires some lemmas.
182
183These lemmas and automation close all proof obligations generated (over 300 in typechecking the main interpreter function).
184\end{frame}
185
186\begin{frame}
187\frametitle{Overlapping memory spaces and addressing modes}
188MCS-51 memory spaces overlap, and can be addressed using different modes and sized pointers.
189The `status' record models memory merely as disjoint spaces, using a `tries with holes' datastructure.
190
191All complications to do with overlapping are handled by \texttt{set\_arg\_XX} and \texttt{get\_arg\_XX} for \texttt{XX} = 1, 8, 16.
192These functions make use of the aforementioned dependent type trick.
193\end{frame}
194
195\begin{frame}
196\frametitle{Validation}
197We worked hard to make sure we implemented a MCS-51 emulator:
198\begin{itemize}
199\item
200Multiple data sheets from different manufacturers (errors found!)
201\item
202O'Caml output to Intel HEX for loading into third party tools, and input for use with SDCC.
203\item
204O'Caml produced trace files with processor status after every execution step, every opcode tested.
205\item
206Matita formalisation is also executable, and traces can be compared with O'Caml.
207\end{itemize}
208\end{frame}
209
210\begin{frame}
211\frametitle{What is implemented}
212In O'Caml we implemented the emulator proper, associated assembler, supprting debugging code (for loading and outputting Intel HEX), and also have (untested) code for timers, interrupts and I/O.
213
214In Matita, we have the emulator proper and associated assembler.
215We have yet to port the timers and I/O, preferring to focus on the core emulator.
216\end{frame}
217
218\begin{frame}
219\frametitle{Demo}
220\end{frame}
221
222\end{document}
Note: See TracBrowser for help on using the repository browser.