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
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
16\author{Dominic P. Mulligan and Claudio Sacerdoti Coen}
[629]17\title{CerCo Work Package 4.1}
[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}
[629]43\frametitle{Work Package 4.1}
[649]44Work Package 4.1 entitled `Executable Formal Semantics of Machine Code':
[629]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}
[650]48Manpower: Dominic Mulligan (609 hours) and Claudio Sacerdoti Coen (16 hours).
[613]49\end{frame}
50
51\begin{frame}
[615]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
[649]57Popular 8-bit microprocessor from the late 1970s.
[615]58\item
[649]59Widely used and manufactured.
[615]60\item
[649]61Relatively simple microprocessor (especially suited for CerCo).
[616]62\item
[649]63Can accurately predict timing information in cycles.
[615]64\end{itemize}
[613]65\end{frame}
66
67\begin{frame}
[615]68\frametitle{The MCS-51 microprocessor II}
69\begin{itemize}
70\item
[649]71No exhaustive introduction.
72Reveal enough to understand what problems we faced.
[615]73\item
[649]74Byzantine memory model.
[616]75\item
[649]76Overlap, have different sizes, may not be present depending on model, addressed in multiple ways, addressed with different sized pointers.
[616]77\item
[649]78Non-orthogonal instruction set.
79\texttt{MOV} takes 16 combinations of addressing mode (possible 300+)s.
[615]80\end{itemize}
81\end{frame}
82
83\begin{frame}
[616]84\frametitle{The MCS-51 microprocessor III}
85\begin{itemize}
86\item
[649]87Three unconditional jumps: \texttt{AJMP}, \texttt{SJMP} and \texttt{LJMP} (first one rarely used).
[616]88\item
[649]89Differ in the size of permissible offset and the size in bytes of instruction.
[616]90\item
[649]91Also has various timers, UART I/O and interrupts.
928052 adds additional timers.
[616]93\item
[649]94Interrupts are simple.
95Flags can be used to manually handle errors.
[616]96\end{itemize}
97\end{frame}
98
99\begin{frame}
[613]100\frametitle{Development strategy}
[649]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}
[613]113\end{frame}
114
115\begin{frame}
[618]116\frametitle{Dealing with the jumps}
117\begin{itemize}
118\item
[649]119Unconditional jumps: offset computed ahead of time.
[618]120\item
[649]121Problems: separate compilation, prototype C compiler.
[618]122\item
[649]123Add pseudoinstructions and `assemble away'.
[618]124\item
125Introduce labels and cost labels (for cost traces).
126\item
[649]127Introduce pseudoinstructions.
128\texttt{Jump}: unconditional jump to labels.
[618]129\item
[649]130Other pseudoinstructions introduced: \texttt{Mov} moves (16 bit) data stored at a label (global vars).
131Conditional jumps to labels.
[618]132\item
[649]133Assembly language similar to that of SDCC.
[618]134\end{itemize}
[613]135\end{frame}
136
[620]137\begin{frame}[fragile]
[613]138\frametitle{Polymorphic variants and phantom types}
[649]139Instruction set is highly non-orthogonal.
140Polymorphic variants and phantom types used to capture this non-orthogonality.
[620]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}
[613]158\end{frame}
159
[620]160\begin{frame}[fragile]
161\frametitle{Use of dependent types I}
[649]162Worked well in O'Caml, Matita does not have polymorphic variants.
[620]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}
[649]173Another type \texttt{addressing\_mode\_tag} of `tags'.
174Constructors are in correspondence with those of \texttt{addressing\_mode}.
[620]175\end{frame}
176
177\begin{frame}[fragile]
178\frametitle{Use of dependent types II}
[649]179Use vectors of \texttt{addressing\_mode\_tag}s in type signatures for instructions.
[620]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.
[649]191One coercion opens up a proof obligation when it is used.
192Requires some lemmas.
[620]193
[649]194Lemmas and automation close proof obligations generated (300+ in typechecking interpreter function).
[620]195\end{frame}
196
[613]197\begin{frame}
[620]198\frametitle{Overlapping memory spaces and addressing modes}
[649]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}
[613]211\end{frame}
212
[618]213\begin{frame}
[628]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
[649]220Output to Intel HEX.
221Loading into third party tools.
[628]222\item
[649]223O'Caml trace files with processor status after every execution step.
224Every opcode tested.
[628]225\item
[649]226Matita formalisation is also executable.
227\item
228Traces can be compared with O'Caml.
[628]229\end{itemize}
230\end{frame}
231
232\begin{frame}
[618]233\frametitle{What is implemented}
[649]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}
[618]242\end{frame}
243
244\begin{frame}
245\frametitle{Demo}
246\end{frame}
247
[611]248\end{document}
Note: See TracBrowser for help on using the repository browser.