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

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

Fixed some slides: added description of WP4.1

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