source: Deliverables/D4.1/ITP-Paper/itp-2011.tex @ 808

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

Changes to paper to get it ready for FMCAD

File size: 52.2 KB
Line 
1\documentclass[10pt, final, conference]{IEEEtran}
2
3\usepackage{amsfonts}
4\usepackage{amsmath}
5\usepackage{amssymb} 
6\usepackage[english]{babel}
7\usepackage{color}
8\usepackage{fancybox}
9\usepackage{graphicx}
10\usepackage[colorlinks]{hyperref}
11\usepackage[utf8x]{inputenc}
12\usepackage{listings}
13\usepackage{mdwlist}
14\usepackage{microtype}
15\usepackage{stmaryrd}
16\usepackage{url}
17
18\newlength{\mylength} 
19\newenvironment{frametxt}%
20        {\setlength{\fboxsep}{5pt}
21                \setlength{\mylength}{\linewidth}%
22                \addtolength{\mylength}{-2\fboxsep}%
23                \addtolength{\mylength}{-2\fboxrule}%
24                \Sbox
25                \minipage{\mylength}%
26                        \setlength{\abovedisplayskip}{0pt}%
27                        \setlength{\belowdisplayskip}{0pt}%
28                }%
29                {\endminipage\endSbox
30                        \[\fbox{\TheSbox}\]}
31
32\lstdefinelanguage{matita-ocaml}
33  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on,to},
34   morekeywords={[2]whd,normalize,elim,cases,destruct},
35   morekeywords={[3]type,of,val,assert,let,function},
36   mathescape=true,
37  }
38\lstset{language=matita-ocaml,basicstyle=\small\tt,columns=flexible,breaklines=false,
39        keywordstyle=\bfseries, %\color{red}\bfseries,
40        keywordstyle=[2]\bfseries, %\color{blue},
41        keywordstyle=[3]\bfseries, %\color{blue}\bfseries,
42%        commentstyle=\color{green},
43%        stringstyle=\color{blue},
44        showspaces=false,showstringspaces=false}
45\DeclareUnicodeCharacter{8797}{:=}
46\DeclareUnicodeCharacter{10746}{++}
47\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
48\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
49
50\lstset{
51  extendedchars=false,
52  inputencoding=utf8x,
53  tabsize=1
54}
55
56\author{
57  \IEEEauthorblockN{Dominic P. Mulligan}
58  \IEEEauthorblockA{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
59\and
60  \IEEEauthorblockN{Claudio Sacerdoti Coen}
61  \IEEEauthorblockA{Dipartimento di Scienze dell'Informazione,\\ Universit\`a di Bologna}
62}
63
64\title{An executable formalisation of the MCS-51 microprocessor in Matita}
65
66\thanks{The project CerCo acknowledges the financial support of the Future and
67Emerging Technologies (FET) programme within the Seventh Framework
68Programme for Research of the European Commission, under FET-Open grant
69number: 243881}
70
71\bibliographystyle{plain}
72
73\begin{document}
74
75\maketitle
76
77\begin{abstract}
78We summarise the formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.
79The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
80
81The formalisation proceeded in two stages, first implementing an O'Caml prototype, for quickly `ironing out' bugs, and then porting the O'Caml emulator to Matita.
82Though mostly straight-forward, this porting presented multiple problems.
83Of particular interest is how the unorthoganality of the MSC-51's instruction set is handled.
84In O'Caml, this was handled with polymorphic variants.
85In Matita, we achieved the same effect with a non-standard use of dependent types.
86
87Both the O'Caml and Matita emulators are `executable'.
88Assembly programs may be animated within Matita, producing a trace of instructions executed.
89The formalisation is a major component of the ongoing EU-funded CerCo project.
90\end{abstract}
91
92\begin{IEEEkeywords}
93Hardware formalisation, Matita, dependent types, CerCo
94\end{IEEEkeywords}
95
96%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
97% SECTION                                                                      %
98%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
99\section{Introduction}
100\label{sect.introduction}
101
102Formal methods aim to increase our confidence in the design and implementation of software.
103Ideally, all software should come equipped with a formal specification and a proof of correctness for the corresponding implementation.
104The majority of programs are written in high level languages and then compiled into low level ones.
105Specifications are therefore also given at a high level and correctness can be proved by reasoning on the program's source code.
106The code that is actually run, however, is not the high level source code that we reason on, but low level code generated by the compiler.
107A few questions now arise:
108\begin{itemize*}
109\item
110What properties are preserved during compilation?
111\item
112What properties are affected by the compilation strategy?
113\item
114To what extent can you trust your compiler in preserving those properties?
115\end{itemize*}
116These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification} (for instance~\cite{chlipala:verified:2010,leroy:formal:2009}, and many others).
117So far, the field has only been focused on the first and last questions.
118Much attention has been placed on verifying compiler correctness with respect to extensional properties of programs.
119These are `easily' preserved during compilation.
120
121If we consider intensional properties of programs---space, time, and so forth---the situation is more complex.
122To express these properties, and reason about them, we must adopt a cost model that assigns a cost to single, or blocks, of instructions.
123A compositional cost model, assigning the same cost to all occurrences of one instruction, would be ideal.
124However, compiler optimisations are inherently non-compositional: each occurrence of a high level instruction may be compiled in a different way depending on its context.
125Therefore both the cost model and intensional specifications are affected by the compilation process.
126
127In the CerCo project (`Certified Complexity')~\cite{cerco:2011} we approach the problem of reasoning about intensional properties of programs as follows.
128We are currently developing a compiler that induces a cost model on high level source code.
129Costs are assigned to each block of high level instructions by considering the costs of the corresponding blocks of compiled code.
130The cost model is therefore inherently non-compositional, but has the potential to be extremely \emph{precise}, capturing a program's \emph{realistic} cost.
131That is, the compilation process is taken into account, not ignored.
132A prototype compiler, where no approximation of the cost is provided, has been developed.
133(The technical details of the cost model is explained in~\cite{amadio:certifying:2010}.)
134
135We believe that our approach is applicable to certifying real time programs.
136A user can certify that `deadlines' are met whilst wringing as many clock cycles from the processor---using a cost model that does not over-estimate---as possible.
137
138We also see our approach as being relevant to compiler verification (and construction).
139\emph{An optimisation specified only extensionally is only half specified}.
140Though the optimisation may preserve the denotational semantics of a program, there is no guarantee that intensional properties of the program improve.
141
142Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints.
143A compiler could reject a source program targetting an embedded system when the size of the compiled code exceeds the available ROM size.
144Preservation of a program's semantics may only be required for those programs that do not exhaust the stack or heap.
145The statement of completeness of the compiler must therefore take in to account a realistic cost model.
146
147With the CerCo methodology, we assume we can assign to object code exact and realistic costs for sequential blocks of instructions.
148This is possible with modern processors (see~\cite{bate:wcet:2011,yan:wcet:2008} for instance) but difficult, as the structure and execution of a program itself has an influence on the speed of processing.
149Caching, memory effects, and advanced features such as branch prediction all have an effect on execution speed.
150For this reason CerCo decided to focus on 8-bit microprocessors.
151These are still used in embedded systems, with the advantage of a predictable cost model due to their relative paucity of features.
152
153We have fully formalised an executable formal semantics of a family of 8-bit Freescale microprocessors~\cite{oliboni:matita:2008}, and provided a similar executable formal semantics for the MCS-51 microprocessor.
154The latter is what we describe in this paper.
155The focus of the formalisation has been on capturing the intensional behaviour of the processor.
156However, the design of the MCS-51 itself has caused problems in the formalisation.
157For example, the MCS-51 has a highly unorthogonal instruction set.
158To cope with this unorthogonality, and to produce an executable specification, we rely on the dependent types of Matita, an interactive proof assistant~\cite{asperti:user:2007}.
159
160\paragraph{The MCS-51}\quad
161The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s.
162Commonly called the 8051, in the decades since its introduction the processor has become a popular component of embedded systems.
163The processor and derivatives are still manufactured \emph{en masse} by a host of vendors.
164
165The 8051 is a well documented processor, and has the support of numerous open source and commercial tools, such as compilers and emulators.
166For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C~\cite{sdcc:2010}, and other compilers for BASIC, Forth and Modula-2 are also extant.
167An open source emulator for the processor, MCU 8051 IDE, is also available~\cite{mcu8051ide:2010}.
168Both MCU 8051 IDE and SDCC were used in for validating the formalisation.
169
170\begin{figure*}
171\centering
172\setlength{\unitlength}{0.87pt}
173\begin{picture}(410,250)(-50,200)
174%\put(-50,200){\framebox(410,250){}}
175\put(12,410){\makebox(80,0)[b]{Internal (256B)}}
176\put(13,242){\line(0,1){165}}
177\put(93,242){\line(0,1){165}}
178\put(13,407){\line(1,0){80}}
179\put(12,400){\makebox(0,0)[r]{0h}}  \put(14,400){\makebox(0,0)[l]{Register bank 0}}
180\put(13,393){\line(1,0){80}}
181\put(12,386){\makebox(0,0)[r]{8h}}  \put(14,386){\makebox(0,0)[l]{Register bank 1}}
182\put(13,379){\line(1,0){80}}
183\put(12,372){\makebox(0,0)[r]{10h}}  \put(14,372){\makebox(0,0)[l]{Register bank 2}}
184\put(13,365){\line(1,0){80}}
185\put(12,358){\makebox(0,0)[r]{18h}} \put(14,358){\makebox(0,0)[l]{Register bank 3}}
186\put(13,351){\line(1,0){80}}
187\put(12,344){\makebox(0,0)[r]{20h}} \put(14,344){\makebox(0,0)[l]{Bit addressable}}
188\put(13,323){\line(1,0){80}}
189\put(12,316){\makebox(0,0)[r]{30h}}
190  \put(14,309){\makebox(0,0)[l]{\quad \vdots}}
191\put(13,291){\line(1,0){80}}
192\put(12,284){\makebox(0,0)[r]{80h}}
193  \put(14,263){\makebox(0,0)[l]{\quad \vdots}}
194\put(12,249){\makebox(0,0)[r]{ffh}}
195\put(13,242){\line(1,0){80}}
196
197\qbezier(-2,407)(-6,407)(-6,393)
198\qbezier(-6,393)(-6,324)(-10,324)
199\put(-12,324){\makebox(0,0)[r]{Indirect/stack}}
200\qbezier(-6,256)(-6,324)(-10,324)
201\qbezier(-2,242)(-6,242)(-6,256)
202
203\qbezier(94,407)(98,407)(98,393)
204\qbezier(98,393)(98,349)(102,349)
205\put(104,349){\makebox(0,0)[l]{Direct}}
206\qbezier(98,305)(98,349)(102,349)
207\qbezier(94,291)(98,291)(98,305)
208
209\put(102,242){\framebox(20,49){SFR}}
210% bit access to sfrs?
211
212\qbezier(124,291)(128,291)(128,277)
213\qbezier(128,277)(128,266)(132,266)
214\put(134,266){\makebox(0,0)[l]{Direct}}
215\qbezier(128,257)(128,266)(132,266)
216\qbezier(124,242)(128,242)(128,256)
217
218\put(164,410){\makebox(80,0)[b]{External (64kB)}}
219\put(164,220){\line(0,1){187}}
220\put(164,407){\line(1,0){80}}
221\put(244,220){\line(0,1){187}}
222\put(164,242){\line(1,0){80}}
223\put(163,400){\makebox(0,0)[r]{0h}}
224\put(164,324){\makebox(80,0){Paged access}}
225  \put(164,310){\makebox(80,0){Direct/indirect}}
226\put(163,235){\makebox(0,0)[r]{80h}}
227  \put(164,228){\makebox(80,0){\vdots}}
228  \put(164,210){\makebox(80,0){Direct/indirect}}
229
230\put(264,410){\makebox(80,0)[b]{Code (64kB)}}
231\put(264,220){\line(0,1){187}}
232\put(264,407){\line(1,0){80}}
233\put(344,220){\line(0,1){187}}
234\put(263,400){\makebox(0,0)[r]{0h}}
235  \put(264,228){\makebox(80,0){\vdots}}
236  \put(264,324){\makebox(80,0){Direct}}
237  \put(264,310){\makebox(80,0){PC relative}}
238\end{picture}
239\caption{The 8051 memory model}
240\label{fig.memory.layout}
241\end{figure*}
242
243The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
244A high-level overview of the processor's memory layout, along with the ways in which different memory spaces may be addressed, is provided in Figure~\ref{fig.memory.layout}.
245
246Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
247Internal memory, commonly provided on the die itself with fast access, is composed of 256 bytes, but, in direct addressing mode, half of them are overloaded with 128 bytes of memory-mapped Special Function Registers (SFRs).
248SFRs control the operation of the processor.
249Internal RAM (IRAM) is divided again into 8 general purpose bit-addressable registers (R0--R7).
250These sit in the first 8 bytes of IRAM, though can be programmatically `shifted up' as needed.
251Bit memory, followed by a small amount of stack space, resides in the memory space immediately following the register banks.
252What remains of IRAM may be treated as general purpose memory.
253A schematic view of IRAM layout is also provided in Figure~\ref{fig.memory.layout}.
254
255External RAM (XRAM), limited to a maximum size of 64 kilobytes, is optional, and may be provided on or off chip, depending on the vendor.
256XRAM is accessed using a dedicated instruction, and requires 16 bits to address fully.
257External code memory (XCODE) is often stored as an EPROM, and limited to 64 kilobytes in size.
258However, depending on the particular processor model, a dedicated on-die read-only memory area for program code (ICODE) may be supplied.
259
260Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
261As the latter two addressing modes hint, there are some restrictions enforced by the 8051, and its derivatives, on which addressing modes may be used with specific types of memory.
262For instance, the extra 128 bytes of IRAM of the 8052 cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used. Moreover, some memory segments are addressed using 8-bit pointers while others require 16-bits.
263
264The 8051 possesses an 8-bit Arithmetic and Logic Unit (ALU), with a variety of instructions for performing arithmetic and logical operations on bits and integers.
265Two 8-bit general purpose accumulators, A and B, are provided.
266
267Communication with the device is handled by an inbuilt UART serial port and controller.
268This can operate in numerous modes.
269Serial baud rate is determined by one of two 16-bit timers included with the 8051, which can be set to multiple modes of operation.
270(The 8052 provides an additional 16-bit timer.)
271The 8051 also provides a 4 byte bit-addressable I/O port.
272
273The programmer may take advantage of an interrupt mechanism.
274This is especially useful when dealing with I/O involving the serial device, as an interrupt can be set when a whole character is sent or received via the UART.
275
276Interrupts immediately halt the flow of execution of the processor, and cause the program counter to jump to a fixed address, where the requisite interrupt handler is stored.
277However, interrupts may be set to one of two priorities: low and high.
278The interrupt handler of an interrupt with high priority is executed ahead of the interrupt handler of an interrupt of lower priority, interrupting a currently executing handler of lower priority, if necessary.
279
280The 8051 has interrupts disabled by default.
281The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
282`Exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, (e.g. division by zero) are also signalled by setting flags.
283
284%\begin{figure}[t]
285%\begin{center}
286%\includegraphics[scale=0.5]{iramlayout.png}
287%\end{center}
288%\caption{Schematic view of 8051 IRAM layout}
289%\label{fig.iram.layout}
290%\end{figure}
291
292\paragraph{Overview of paper}\quad
293In Section~\ref{sect.design.issues.formalisation} we discuss design issues in the development of the formalisation.
294In Section~\ref{sect.validation} we discuss how we validated the design and implementation of the emulator to ensure that what we formalised was an accurate model of an MCS-51 series microprocessor.
295In Section~\ref{sect.related.work} we describe previous work, with an eye toward describing its relation with the work described herein.
296In Section~\ref{sect.conclusions} we conclude.
297
298%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
299% SECTION                                                                      %
300%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
301\section{Design issues in the formalisation}
302\label{sect.design.issues.formalisation}
303
304We typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}}.
305Matita's syntax is straightforward if familiar with Coq or O'Caml.
306One subtlety is the use of `\texttt{?}' or `\texttt{$\ldots$}' denoting an argument or arguments to be inferred, respectively.
307
308A full account of the formalisation can be found in~\cite{cerco-report:2011}.
309All source code is available from the CerCo project website~\cite{cerco-code:2011}.
310
311\subsection{Development strategy}
312\label{subsect.development.strategy}
313
314The implementation progressed in two stages.
315We began with an emulator written in O'Caml to `iron out' any bugs in the design and implementation.
316O'Caml's ability to perform file I/O also eased debugging and validation.
317Once we were happy with the design of the O'Caml emulator, we moved to Matita.
318
319Matita's syntax is lexically similar to O'Caml's.
320This eased the translation, as swathes of code were copied with minor modifications.
321However, several major issues had to be addressed when moving to Matita.
322These are now discussed.
323
324%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
325% SECTION                                                                      %
326%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
327\subsection{Representation of bytes, words, etc.}
328\label{subsect.representation.integers}
329
330\begin{figure}[t]
331\begin{minipage}[t]{0.45\textwidth}
332\vspace{0pt}
333\small{
334\begin{lstlisting}
335type 'a vect = bit list
336type nibble = [`Sixteen] vect
337type byte = [`Eight] vect
338$\color{blue}{\mathtt{let}}$ split_word w = split_nth 4 w
339$\color{blue}{\mathtt{let}}$ split_byte b = split_nth 2 b
340\end{lstlisting}}
341\end{minipage}
342%
343\begin{minipage}[t]{0.55\textwidth}
344\vspace{0pt}
345\begin{lstlisting}
346type 'a vect
347type word = [`Sixteen] vect
348type byte = [`Eight] vect
349val split_word: word -> byte * word
350val split_byte: byte -> nibble * nibble
351\end{lstlisting}
352\end{minipage}
353\caption{Sample of O'Caml implementation and interface for bitvectors module}
354\label{fig.ocaml.implementation.bitvectors}
355\end{figure}
356
357The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits), and also more exoteric quantities (7, 3 and 9-bits).
358To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans.
359In the O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
360From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
361However, the module's interface (right column) enforces size invariants in the rest of the code.
362
363In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
364\begin{lstlisting}
365inductive Vector (A: Type[0]): nat $\rightarrow$ Type[0] ≝
366  VEmpty: Vector A O
367| VCons: $\forall$n: nat. A $\rightarrow$ Vector A n $\rightarrow$ Vector A (S n).
368\end{lstlisting}
369We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}.
370We may use Matita's type system to provide precise typings for functions that are polymorphic in the size without code duplication:
371\begin{lstlisting}
372let rec split (A: Type[0]) (m,n: nat) on m:
373   Vector A (plus m n) $\rightarrow$ (Vector A m) $\times$ (Vector A n) := ...
374\end{lstlisting}
375
376%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
377% SECTION                                                                      %
378%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
379\subsection{Representing memory}
380\label{subsect.representing.memory}
381
382The MCS-51 has numerous disjoint memory spaces addressed by differently sized pointers.
383In the O'Caml implementation, we use a map data structure (from the standard library) for each space.
384Matita's standard library is small, and does not contain a generic map data structure.
385We had the opportunity of crafting a dependently typed special-purpose data structure for the job to enforce the correspondence between the size of pointer and the size of the memory space.
386Further, we assumed that large swathes of memory would often be uninitialized.
387
388We picked a modified form of trie of fixed height $h$.
389Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$:
390\begin{lstlisting}
391inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
392  Leaf: A $\rightarrow$ BitVectorTrie A 0
393| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
394| Stub: ∀n. BitVectorTrie A n.
395\end{lstlisting}
396\texttt{Stub} is a constructor that can appear at any point in a trie.
397It represents `uninitialized data'.
398Performing a lookup in memory is now straight-forward.
399The only subtlety over normal trie lookup is how we handle \texttt{Stub}.
400We traverse a path, and upon encountering \texttt{Stub}, we return a default value\footnote{All manufacturer data sheets that we consulted were silent on the subject of what should be returned if we attempt to access uninitialized memory.  We defaulted to simply returning zero, though our \texttt{lookup} function is parametric in this choice.  We do not believe that this is an outrageous decision, as SDCC for instance generates code which first `zeroes out' all memory in a preamble before executing the program proper.  This is in line with the C standard, which guarantees that all global variables will be zero initialized piecewise.}.
401
402%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
403% SECTION                                                                      %
404%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
405\subsection{Labels and pseudoinstructions}
406\label{subsect.labels.pseudoinstructions}
407
408Aside from implementing the core MCS-51 instruction set, we also provided \emph{pseudoinstructions}, \emph{labels} and \emph{cost labels}.
409The purpose of \emph{cost labels} will be explained in Subsection~\ref{subsect.computation.cost.traces}.
410
411Introducing pseudoinstructions had the effect of simplifying a C compiler---another component of the CerCo project---that was being implemented in parallel with our implementation.
412To see why, consider the fact that the MCS-51's instruction set has numerous instructions for unconditional and conditional jumps to memory locations.
413For instance, the instructions \texttt{AJMP}, \texttt{JMP} and \texttt{LJMP} all perform unconditional jumps.
414However, these instructions differ in how large the maximum size of the offset of the jump to be performed can be.
415Further, all jump instructions require a concrete memory address---to jump to---to be specified.
416Compilers that support separate compilation cannot directly compute these offsets and select the appropriate jump instructions.
417These operations are also burdensome for compilers that do not do separate compilation and are handled by assemblers.
418We followed suit.
419
420While introducing pseudoinstructions, we also introduced labels for locations to jump to, and for global data.
421To specify global data via labels, we introduced a preamble before the program where labels and the size of reserved space for data is stored.
422A pseudoinstruction \texttt{Mov} moves (16-bit) data stored at a label into the MCS-51's one 16-bit register, \texttt{DPTR}.
423(This register is used for indirect addressing of data stored in external memory.)
424
425The pseudoinstructions and labels induce an assembly language similar to that of SDCC's.
426All pseudoinstructions and labels are `assembled away' prior to program execution.
427Jumps are computed in two stages.
428A map associating memory addresses to labels is built, before replacing pseudojumps with concrete jumps to the correct address.
429The algorithm currently implemented does not try to minimize object code size by picking the shortest possible jump instruction.
430A better algorithm is left for future work.
431
432%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
433% SECTION                                                                      %
434%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
435\subsection{Anatomy of the (Matita) emulator}
436\label{subsect.anatomy.matita.emulator}
437
438The internal state of the Matita emulator is represented as a record:
439\begin{lstlisting}
440record Status: Type[0] ≝ {
441  code_memory: BitVectorTrie Byte 16;
442  low_internal_ram: BitVectorTrie Byte 7;
443  high_internal_ram: BitVectorTrie Byte 7;
444  external_ram: BitVectorTrie Byte 16;
445  program_counter: Word;
446  special_function_registers_8051: Vector Byte 19;
447  special_function_registers_8052: Vector Byte 5;
448  ...  }.
449\end{lstlisting}
450This record encapsulates the current memory contents, the program counter, the state of the current SFRs, and so on.
451
452Here the MCS-51's memory model is implemented using four disjoint memory spaces, plus SFRs.
453From the programmer's point of view, what \emph{really} matters are the addressing modes that are in a many-to-many relationship with the spaces.
454\texttt{DIRECT} addressing can be used to address either lower IRAM (if the first bit is 0) or the SFRs (if the first bit is 1), for instance.
455That's why DIRECT uses 8-bit addresses but pointers to lower IRAM only use 7 bits.
456The complexity of the memory model is captured in a pair of functions, \texttt{get\_arg\_XX} and \texttt{set\_arg\_XX}, that `get' and `set' data of size \texttt{XX} from memory.
457
458%Overlapping, and checking which addressing modes can be used to address particular memory spaces, is handled through numerous \texttt{get\_arg\_XX} and \texttt{set\_arg\_XX} (for 1, 8 and 16 bits) functions.
459
460Both the Matita and O'Caml emulators follow the classic `fetch-decode-execute' model of processor operation.
461The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
462An updated program counter, along with its concrete cost in processor cycles, is also returned.
463These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary between particular implementations.
464\begin{lstlisting}
465definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat
466\end{lstlisting}
467Instruction are assembled to bit encodings by \texttt{assembly1}:
468\begin{lstlisting}
469definition assembly1: instruction $\rightarrow$ list Byte
470\end{lstlisting}
471An assembly program---comprising a preamble containing global data and a list of pseudoinstructions---is assembled using \texttt{assembly}.
472Pseudoinstructions and labels are eliminated in favour of instructions from the MCS-51 instruction set.
473A map associating memory locations and cost labels (see Subsection~\ref{subsect.computation.cost.traces}) is produced.
474\begin{lstlisting}
475definition assembly:
476  assembly_program $\rightarrow$ option (list Byte $\times$ (BitVectorTrie String 16))
477\end{lstlisting}
478A single fetch-decode-execute cycle is performed by \texttt{execute\_1}:
479\begin{lstlisting}
480definition execute_1: Status $\rightarrow$ Status
481\end{lstlisting}
482The \texttt{execute} functions performs a fixed number of cycles by iterating
483\texttt{execute\_1}:
484\begin{lstlisting}
485let rec execute (n: nat) (s: Status) on n: Status := ...
486\end{lstlisting}
487This differs from the O'Caml emulator, which executed a program indefinitely.
488A callback function was also accepted as an argument, which `witnessed' the execution as it happened.
489Due to Matita's termination requirement, \texttt{execute} cannot execute a program indefinitely.
490An alternative approach would be to produce an infinite stream of statuses representing an execution trace.
491Matita supports infinite streams through co-inductive types.
492
493%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
494% SECTION                                                                      %
495%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
496\subsection{Instruction set unorthogonality}
497\label{subsect.instruction.set.unorthogonality}
498
499A peculiarity of the MCS-51 is its unorthogonal instruction set.
500For instance, the \texttt{MOV} instruction can be invoked using one of 16 combinations of addressing modes out of a possible 361.
501
502% Show example of pattern matching with polymorphic variants
503
504Such unorthogonality in the instruction set was handled with the use of polymorphic variants in O'Caml.
505For instance, we introduced types corresponding to each addressing mode:
506\begin{lstlisting}
507type direct = [ `DIRECT of byte ]
508type indirect = [ `INDIRECT of bit ]
509...
510\end{lstlisting}
511Which were then combined in the inductive datatype for assembly preinstructions using the union operator `$|$':
512\begin{lstlisting}
513type 'addr preinstruction =
514 [ `ADD of acc * [ reg | direct | indirect | data ]
515...
516 | `MOV of
517    (acc * [ reg | direct | indirect | data ],
518     [ reg | indirect ] * [ acc | direct | data ],
519     direct * [ acc | reg | direct | indirect | data ],
520     dptr * data16,
521     carry * bit,
522     bit * carry
523     ) union6
524...
525\end{lstlisting}
526Here, \texttt{union6} is a disjoint union type, defined as follows:
527\begin{lstlisting}
528type ('a,'b,'c,'d,'e,'f) union6 =
529  [ `U1 of 'a | ... | `U6 of 'f ]
530\end{lstlisting}
531For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
532
533This polymorphic variant machinery worked well: it introduced a certain level of type safety (for instance, the type of \texttt{MOV} above guarantees it cannot be invoked with arguments in the \texttt{carry} and \texttt{data16} addressing modes, respectively), and also allowed us to pattern match against instructions, when necessary.
534However, this polymorphic variant machinery is \emph{not} present in Matita.
535We needed some way to produce the same effect, which Matita supported.
536For this task, we used dependent types.
537
538We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against:
539\begin{lstlisting}
540inductive addressing_mode: Type[0] ≝
541  DIRECT: Byte $\rightarrow$ addressing_mode
542| INDIRECT: Bit $\rightarrow$ addressing_mode
543...
544\end{lstlisting}
545We also wished to express in the type of functions the \emph{impossibility} of pattern matching against certain constructors.
546In order to do this, we introduced an inductive type of addressing mode `tags'.
547The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}:
548\begin{lstlisting}
549inductive addressing_mode_tag : Type[0] ≝
550  direct: addressing_mode_tag
551| indirect: addressing_mode_tag
552...
553\end{lstlisting}
554The \texttt{is\_a} function checks if an \texttt{addressing\_mode} matches an \texttt{addressing\_mode\_tag}:
555\begin{lstlisting}
556let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d :=
557  match d with
558   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
559   | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
560...
561\end{lstlisting}
562The \texttt{is\_in} function checks if an \texttt{addressing\_mode} matches a set of tags represented as a vector. It simply extends the \texttt{is\_a} function in the obvious manner.
563
564A \texttt{subaddressing\_mode} is an \emph{ad hoc} non-empty $\Sigma$-type of \texttt{addressing\_mode}s constrained to be in a set of tags:
565\begin{lstlisting}
566record subaddressing_mode n (l: Vector addressing_mode_tag (S n)): Type[0] :=
567 { subaddressing_modeel :> addressing_mode;
568   subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel) }.
569\end{lstlisting}
570An implicit coercion is provided to promote vectors of tags (denoted with $\llbracket - \rrbracket$) to the corresponding \texttt{subaddressing\_mode} so that we can use a syntax close to that of O'Caml to specify \texttt{preinstruction}s:
571\begin{lstlisting}
572inductive preinstruction (A: Type[0]): Type[0] ≝
573   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
574 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
575...
576\end{lstlisting}
577The constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), the second being a register, direct, indirect or data addressing mode.
578
579% One of these coercions opens up a proof obligation which needs discussing
580% Have lemmas proving that if an element is a member of a sub, then it is a member of a superlist, and so on
581The final component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively.
582The first is a forgetful coercion, while the second opens a proof obligation wherein we must prove that the provided value is in the admissible set.
583These coercions were first introduced by PVS to implement subset types~\cite{shankar:principles:1999}, and later in Coq as part of Russell~\cite{sozeau:subset:2006}.
584In Matita all coercions can open proof obligations.
585
586Proof obligations require us to state and prove a few auxilliary lemmas related to the transitivity of subtyping.
587For instance, an \texttt{addressing\_mode} that belongs to an allowed set also belongs to any one of its supersets.
588At the moment, Matita's automation exploits these lemmas to completely solve all the proof obligations opened in the formalisation.
589The \texttt{execute\_1} function, for instance, opens over 200 proof obligations during type checking.
590
591The machinery just described allows us to restrict the set of \texttt{addressing\_mode}s expected by a function and use this information during pattern matching.
592This allows us to skip impossible cases.
593For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
594\begin{lstlisting}
595definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝ $~\lambda$s, v, a.
596   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
597     [ DPTR $\Rightarrow$ $\lambda$_: True.
598       let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
599       let status := set_8051_sfr s SFR_DPH bu in
600       let status := set_8051_sfr status SFR_DPL bl in
601         status
602     | _ $\Rightarrow$ $\lambda$_: False. $\bot$ ]
603       $~$(subaddressing_modein $\ldots$ a).
604\end{lstlisting}
605We give a proof (the expression \texttt{(subaddressing\_modein} $\ldots$ \texttt{a)}) that the argument $a$ is in the set $\llbracket$ \texttt{dptr} $\rrbracket$ to the \texttt{match} expression.
606In every case but \texttt{DPTR}, the proof is a proof of \texttt{False}, and the system opens a proof obligation $\bot$ that can be discarded using \emph{ex falso}.
607Attempting to match against a disallowed addressing mode (replacing \texttt{False} with \texttt{True} in the branch) produces a type error.
608
609We tried other dependently and non-dependently typed solutions before settling on this approach.
610As we need a large number of different combinations of addressing modes to describe the whole instruction set, it is infeasible to declare a datatype for each one of these combinations.
611The current solution is closest to the corresponding O'Caml code, to the point that the translation from O'Caml to Matita is almost syntactical.
612We would like to investigate the possibility of changing the code extraction procedure of Matita so that it recognises this programming pattern and outputs O'Caml code using polymorphic variants.
613
614% Talk about extraction to O'Caml code, which hopefully will allow us to extract back to using polymorphic variants, or when extracting vectors we could extract using phantom types
615% Discuss alternative approaches, i.e. Sigma types to piece together smaller types into larger ones, as opposed to using a predicate to `cut out' pieces of a larger type, which is what we did
616
617%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
618% SECTION                                                                      %
619%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
620\subsection{I/O and timers}
621\label{subsect.i/o.timers}
622
623% `Real clock' for I/O and timers
624The O'Caml emulator has code for handling timers, asynchronous I/O and interrupts (these are not yet ported to the Matita emulator).
625All three of these features interact with each other in subtle ways.
626Interrupts can `fire' when an input is detected on the processor's UART port, and, in certain modes, timers reset when a high signal is detected on one of the MCS-51's communication pins.
627
628To accurately model timers and I/O, we add an unbounded integral field \texttt{clock} to the central \texttt{status} record.
629This field is only logical, since it does not represent any quantity stored in the physical processor, and is used to keep track of the current `processor time'.
630Before every execution step, \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute.
631The emulator then executes the instruction, followed by the code implementing the timers and I/O\footnote{Though it isn't fully specified by the manufacturer's data sheets if I/O is handled at the beginning or the end of each cycle.}.
632In order to model I/O, we also store in \texttt{status} a \emph{continuation} which is a description of the behaviour of the environment:
633\begin{lstlisting}
634type line =
635  [ `P1 of byte | `P3 of byte
636  | `SerialBuff of
637     [ `Eight of byte
638     | `Nine of BitVectors.bit * byte ]
639  ]
640type continuation =
641  [`In of time * line *
642          epsilon * continuation] option *
643  [`Out of (time -> line -> time * continuation)]
644\end{lstlisting}
645At each moment, the second projection of the continuation $k$ describes how the environment will react to an output event performed in the future by the processor.
646Suppose $\pi_2(k)(\tau,o) = \langle \tau',k' \rangle$.
647If the emulator at time $\tau$ starts an asynchronous output $o$ either on the P1 or P3 output lines, or on the UART, then the environment will receive the output at time $\tau'$.
648Moreover \texttt{status} is immediately updated with the continuation $k'$.
649
650Further, if $\pi_1(k) = \mathtt{Some}~\langle \tau',i,\epsilon,k'\rangle$, then at time $\tau'$ the environment will send the asynchronous input $i$ to the emulator and \texttt{status} is updated with the continuation $k'$.
651This input is visible to the emulator only at time $\tau' + \epsilon$.
652
653The time required to perform an I/O operation is partially specified in the data sheets of the UART module.
654This computation is complex so we prefer to abstract over it.
655We leave the computation of the delay time to the environment.
656
657We use only the P1 and P3 lines despite the MCS-51 having 4 output lines, P0--P3.
658This is because P0 and P2 become inoperable if the processor is equipped with XRAM (we assume it is).
659
660The UART port can work in several modes, depending on the how the SFRs are set.
661In an asyncrhonous mode, the UART transmits 8 bits at a time, using a ninth line for synchronisation.
662In a synchronous mode the ninth line is used to transmit an additional bit.
663
664%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
665% SECTION                                                                      %
666%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
667\subsection{Computation of cost traces}
668\label{subsect.computation.cost.traces}
669
670As mentioned in Subsection~\ref{subsect.labels.pseudoinstructions} we introduced a notion of \emph{cost label}.
671Cost labels are inserted by the prototype C compiler at specific locations in the object code.
672Roughly, for those familiar with control flow graphs, they are inserted at the start of every basic block.
673
674Cost labels are used to calculate a precise costing for a program by marking the location of basic blocks.
675During the assembly phase, where labels and pseudoinstructions are eliminated, a map is generated associating cost labels with memory locations.
676This map is later used in a separate analysis which computes the cost of a program by traversing through a program, fetching one instruction at a time, and computing the cost of blocks.
677These block costings are stored in another map, and will later be passed back to the prototype compiler.
678
679%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
680% SECTION                                                                      %
681%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
682\section{Validation}
683\label{sect.validation}
684
685\begin{figure}[t]
686\begin{scriptsize}
687\begin{verbatim}
68808: mov 81 #07
689
690 Processor status:                               
691
692   ACC: 0   B: 0   PSW: 0
693    with flags set as:
694     CY: false    AC: false   FO: false   RS1: false
695     RS0: false   OV: false   UD: false   P: false
696   SP: 7   IP: 0   PC: 8   DPL: 0   DPH: 0   SCON: 0
697   SBUF: 0   TMOD: 0   TCON: 0
698   Registers:                                   
699    R0: 0   R1: 0   R2: 0   R3: 0
700    R4: 0   R5: 0   R6: 0   R7: 0
701\end{verbatim}
702\end{scriptsize}
703\caption{An example snippet from an emulator execution trace}
704\label{fig.execution.trace}
705\end{figure}
706
707We spent considerable effort attempting to ensure that what we have formalised is an accurate model of the MCS-51 microprocessor.
708
709We made use of multiple data sheets, each from a different manufacturer.
710This helped us triangulate errors in the specification of the processor's instruction set, and its behaviour, for instance, in a data sheet from Philips Semiconductor.
711
712The O'Caml prototype was especially useful for validation purposes.
713We wrote a module for parsing and loading Intel HEX format files.
714Intel HEX is a standard format that all compilers targetting the MCS-51, and similar processors, produce.
715It is essentially a snapshot of the processor's code memory in compressed form.
716Using this we were able to compile C programs with SDCC and load the resulting program directly into the emulator's code memory, ready for execution.
717Further, we can produce a HEX file from the emulator's code memory for loading into third party tools.
718After each step of execution, we can print out both the instruction that had been executed and a snapshot of the processor's state, including all flags and register contents.
719
720A snippet from an execution trace is found in Figure~\ref{fig.execution.trace}.
721Here, the trace indicates that the instruction \texttt{mov 81 \#07} has just been executed by the processor, which is now in the state indicated.
722These traces were useful in spotting anything that was `obviously' wrong with the execution of the program.
723
724We further used MCU 8051 IDE as a reference, which allows a user to step through an assembly program one instruction at a time.
725Using these execution traces, we were able to step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator.
726
727We partially validated the assembler by checking that on defined opcodes the \texttt{assembly\_1} and \texttt{fetch} functions are inverse.
728
729The Matita formalisation was largely copied from the O'Caml source code, apart from the changes already mentioned.
730However, as the Matita emulator is executable, we could perform further validation by comparing the trace of a program's execution in the Matita emulator with the trace of the same program in the O'Caml emulator.
731
732%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
733% SECTION                                                                      %
734%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
735\section{Related work}
736\label{sect.related.work}
737A large body of literature on the formalisation of microprocessors exists.
738The majority of it deals with proving correctness of implementations of microprocessors at the microcode or gate level.
739We are interested in providing a precise specification of the behaviour of the microprocessor in order to prove the correctness of a compiler which will target the processor.
740In particular, we are interested in intensional properties of the processor; precise timings of instruction execution in clock cycles.
741Moreover, in addition to formalising the interface of an MCS-51 processor, we have also built a complete MCS-51 ecosystem: UART, I/O lines, and hardware timers, complete with an assembler.
742
743Work closely related to our own can be found in~\cite{fox:trustworthy:2010}.
744Here, the authors describe the formalisation, in HOL4, of the ARMv7 instruction set architecture.
745They further point to an excellent list of references to related work in the literature for the interested reader.
746This formalisation also considers the machine code level, opposed to their formalisation, which only considering an abstract assembly language.
747In particular, instruction decoding is explicitly modeled inside HOL4's logic.
748We go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction into machine code.
749
750Further, in~\cite{fox:trustworthy:2010} the authors validated their formalisation by using development boards and random testing.
751We currently rely on non-exhaustive testing against a third party emulator.
752We recognise the importance of this exhaustive testing, but currently leave it for future work.
753
754Executability is another key difference between our work and that of~\cite{fox:trustworthy:2010}.
755Our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state.
756This is because Matita is based on a logic, CIC, which internalizes conversion.
757In~\cite{fox:trustworthy:2010} the authors provide an automation layer to derive single step theorems: if the processor is in a state that satisfies some preconditions, then after execution of an instruction it will reside in a state satisfying some postconditions.
758We do not need single step theorems of this form.
759
760Our main difficulties resided in the non-uniformity of an old 8-bit architecture, in terms of the instruction set, addressing modes and memory models.
761In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably.
762
763Perhaps the closest project to CerCo is CompCert~\cite{leroy:formally:2009}.
764CompCert concerns the certification of a C compiler and includes a formalisation in Coq of a subset of PowerPC.
765(Coq and Matita essentially share the same logic.)
766
767Despite this similarity, the two formalisations do not have much in common.
768First, CompCert provides a formalisation at the assembly level (no instruction decoding).
769This impels them to trust an unformalised assembler and linker, whereas we provide our own.
770Our formalisation is \emph{directly} executable, while the one in CompCert only provides a relation that describes execution.
771I/O is also not considered at all in CompCert.
772Moreover an idealized abstract and uniform memory model is assumed, while we take into account the complicated overlapping memory model of the MCS-51 architecture.
773Finally, 82 instructions of the more than 200 offered by the processor are formalised in CompCert, and the assembly language is augmented with macro instructions that are turned into `real' instructions only during communication with the external assembler.
774Even from a technical level the two formalisations differ: we tried to exploit dependent types whilst CompCert largely sticks to a non-dependent fragment of Coq.
775
776In~\cite{atkey:coqjvm:2007} an executable specification of the Java Virtual Machine, using dependent types, is presented.
777As we do, dependent types there are used to remove spurious partiality from the model.
778They also lower the need for over-specifying the behaviour of the processor in impossible cases.
779Our use of dependent types will also help to maintain invariants when we prove the correctness of the CerCo prototype C compiler.
780
781Finally~\cite{sarkar:semantics:2009} provides an executable semantics for x86-CC multiprocessor machine code.
782This machine code exhibits a high degree of non-uniformity similar to the MCS-51.
783However, only a small subset of the instruction set is considered, and they over-approximate the possibilities of unorthogonality of the instruction set, largely dodging the problems we had to face.
784
785Further, it seems that the definition of the decode function is potentially error prone.
786A small domain specific language of patterns is formalised in HOL4.
787This is similar to the specification language of the x86 instruction set found in manufacturer's data sheets.
788A decode function is implemented by copying lines from data sheets into the proof script, which are then interpreted.
789
790We are currently considering implementing a similar domain specific language in Matita.
791However, we would prefer to certify in Matita the compiler for this language.
792Data sheets could then be compiled down to the efficient code that we currently provide, instead of inefficiently interpreting the data sheets every time an instruction is executed.
793
794%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
795% SECTION                                                                      %
796%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
797\section{Conclusions}
798\label{sect.conclusions}
799
800In CerCo, we are interested in the certification of a compiler for C that induces a precise cost model on the source code.
801Our cost model assigns costs to blocks of instructions by tracing the way that blocks are compiled, and by computing exact costs on generated machine language.
802To perform this accurately, we have provided an executable semantics for the MCS-51 family of processors.
803The formalisation was done twice, first in O'Caml and then in Matita, and captures the exact timings of the processor (according to a Siemen's data sheet).
804Moreover, the O'Caml formalisation also considers timers and I/O.
805Adding support for I/O and timers in Matita is on-going work that will not present any major problem, and was delayed only because the addition is not immediately useful for the formalisation of the CerCo compiler.
806
807The formalisation is done at machine level and not at assembly level; we also formalise fetching and decoding.
808We separately provide an assembly language, enhanched with labels and pseudoinstructions, and an assembler from this language to machine code.
809This assembly language is similar to those found in `industrial strength' compilers, such as SDCC.
810We introduce cost labels in the machine language to relate the data flow of the assembly program to that of the C source language, in order to associate costs to the C program.
811For the O'Caml version, we provide a parser and pretty printer from code memory to Intel HEX.
812Hence we can perform testing on programs compiled using any free or commercial compiler.
813
814Our main difficulty in formalising the MCS-51 was the unorthogonality of its memory model and instruction set.
815These problems are easily handled in O'Caml by using advanced language features like polymorphic variants and phantom types, simulating Generalized Abstract Data Types.
816In Matita, we use dependent types to recover the same flexibility, to reduce spurious partiality, and to grant invariants that will be later useful in other formalisations in the CerCo project.
817
818The formalisation has been partially verified by computing execution traces on selected programs and comparing them with an existing emulator.
819All instructions have been tested at least once, but we have not yet pushed testing further, for example with random testing or by using development boards.
820I/O in particular has not been tested yet, and it is currently unclear how to provide exhaustive testing in the presence of I/O.
821Finally, we are aware of having over-specified the processor in several places, by fixing a behaviour hopefully consistent with the real machine, where manufacturer data sheets are ambiguous or under-specified.
822
823\bibliography{itp-2011.bib}
824
825\end{document}
Note: See TracBrowser for help on using the repository browser.