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

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

Completed presentation slides by mentioning man hours used

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