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

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

Fixed man months

File size: 7.0 KB
RevLine 
[611]1\documentclass{beamer}
2
3\usetheme{Frankfurt}
[614]4\logo{\includegraphics[height=1.0cm]{fetopen.png}}
[611]5
[620]6\usepackage{amsfonts}
7\usepackage{amsmath}
8\usepackage{amssymb}
[611]9\usepackage[english]{babel}
[620]10\usepackage{color}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{stmaryrd}
14% \usepackage{microtype}
[611]15
[667]16\author{Dominic P. Mulligan}
17\title{CerCo Work Package 4}
[611]18\date{March 11, 2011}
19
[617]20\setlength{\parskip}{1em}
21
[620]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
[611]36\begin{document}
37
38\begin{frame}
39\maketitle
40\end{frame}
41
[613]42\begin{frame}
[668]43\frametitle{Work Package 4}
[667]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.
[613]55\end{frame}
56
57\begin{frame}
[667]58\frametitle{People involved}
59\begin{tabular}{lll}
[669]60Name & Position & Man months \\
[667]61\hline
[669]62Dominic Mulligan & Postdoc & 5 man months \\
63Claudio Sacerdoti Coen & Assistant Professor & 1 man month
[667]64\end{tabular}
65\end{frame}
66
67\begin{frame}
[615]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
[649]73Popular 8-bit microprocessor from the late 1970s.
[615]74\item
[649]75Widely used and manufactured.
[615]76\item
[649]77Relatively simple microprocessor (especially suited for CerCo).
[616]78\item
[649]79Can accurately predict timing information in cycles.
[615]80\end{itemize}
[613]81\end{frame}
82
83\begin{frame}
[615]84\frametitle{The MCS-51 microprocessor II}
85\begin{itemize}
86\item
[649]87No exhaustive introduction.
88Reveal enough to understand what problems we faced.
[615]89\item
[649]90Byzantine memory model.
[616]91\item
[649]92Overlap, have different sizes, may not be present depending on model, addressed in multiple ways, addressed with different sized pointers.
[616]93\item
[649]94Non-orthogonal instruction set.
95\texttt{MOV} takes 16 combinations of addressing mode (possible 300+)s.
[615]96\end{itemize}
97\end{frame}
98
99\begin{frame}
[616]100\frametitle{The MCS-51 microprocessor III}
101\begin{itemize}
102\item
[649]103Three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used).
[616]104\item
[649]105Differ in the size of permissible offset and the size in bytes of instruction.
[616]106\item
[649]107Also has various timers, UART I/O and interrupts.
1088052 adds additional timers.
[616]109\item
[649]110Interrupts are simple.
111Flags can be used to manually handle errors.
[616]112\end{itemize}
113\end{frame}
114
115\begin{frame}
[613]116\frametitle{Development strategy}
[649]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}
[613]129\end{frame}
130
131\begin{frame}
[618]132\frametitle{Dealing with the jumps}
133\begin{itemize}
134\item
[649]135Unconditional jumps: offset computed ahead of time.
[618]136\item
[649]137Problems: separate compilation, prototype C compiler.
[618]138\item
[649]139Add pseudoinstructions and `assemble away'.
[618]140\item
141Introduce labels and cost labels (for cost traces).
142\item
[649]143Introduce pseudoinstructions.
144\texttt{Jump}: unconditional jump to labels.
[618]145\item
[649]146Other pseudoinstructions introduced: \texttt{Mov} moves (16 bit) data stored at a label (global vars).
147Conditional jumps to labels.
[618]148\item
[649]149Assembly language similar to that of SDCC.
[618]150\end{itemize}
[613]151\end{frame}
152
[620]153\begin{frame}[fragile]
[613]154\frametitle{Polymorphic variants and phantom types}
[649]155Instruction set is highly non-orthogonal.
156Polymorphic variants and phantom types used to capture this non-orthogonality.
[620]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}
[613]174\end{frame}
175
[620]176\begin{frame}[fragile]
177\frametitle{Use of dependent types I}
[649]178Worked well in O'Caml, Matita does not have polymorphic variants.
[620]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}
[649]189Another type \texttt{addressing\_mode\_tag} of `tags'.
190Constructors are in correspondence with those of \texttt{addressing\_mode}.
[620]191\end{frame}
192
193\begin{frame}[fragile]
194\frametitle{Use of dependent types II}
[649]195Use vectors of \texttt{addressing\_mode\_tag}s in type signatures for instructions.
[620]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.
[649]207One coercion opens up a proof obligation when it is used.
208Requires some lemmas.
[620]209
[649]210Lemmas and automation close proof obligations generated (300+ in typechecking interpreter function).
[620]211\end{frame}
212
[613]213\begin{frame}
[620]214\frametitle{Overlapping memory spaces and addressing modes}
[649]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}
[613]227\end{frame}
228
[618]229\begin{frame}
[628]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
[649]236Output to Intel HEX.
237Loading into third party tools.
[628]238\item
[649]239O'Caml trace files with processor status after every execution step.
240Every opcode tested.
[628]241\item
[649]242Matita formalisation is also executable.
243\item
244Traces can be compared with O'Caml.
[628]245\end{itemize}
246\end{frame}
247
248\begin{frame}
[618]249\frametitle{What is implemented}
[649]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}
[618]258\end{frame}
259
260\begin{frame}
261\frametitle{Demo}
262\end{frame}
263
[611]264\end{document}
Note: See TracBrowser for help on using the repository browser.