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

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

more changes to intro

File size: 27.5 KB
19        {\setlength{\fboxsep}{5pt}
20                \setlength{\mylength}{\linewidth}%
21                \addtolength{\mylength}{-2\fboxsep}%
22                \addtolength{\mylength}{-2\fboxrule}%
23                \Sbox
24                \minipage{\mylength}%
25                        \setlength{\abovedisplayskip}{0pt}%
26                        \setlength{\belowdisplayskip}{0pt}%
27                }%
28                {\endminipage\endSbox
29                        \[\fbox{\TheSbox}\]}
[510]32  {keywords={definition,coercion,lemma,theorem,remark,inductive,record,qed,let,in,rec,match,return,with,Type,try,on},
33   morekeywords={[2]whd,normalize,elim,cases,destruct},
34   morekeywords={[3]type,ofm},
[495]35   mathescape=true,
36  }
38        keywordstyle=\color{red}\bfseries,
39        keywordstyle=[2]\color{blue},
40        keywordstyle=[3]\color{blue}\bfseries,
41        commentstyle=\color{green},
42        stringstyle=\color{blue},
43        showspaces=false,showstringspaces=false}
[493]51\author{Claudio Sacerdoti Coen \and Dominic P. Mulligan}
[492]52\authorrunning{C. Sacerdoti Coen and D. P. Mulligan}
[501]53\title{An executable formalisation of the MCS-51 microprocessor in Matita}
54\titlerunning{An executable formalisation of the MCS-51}
[492]55\institute{Dipartimento di Scienze dell'Informazione, University of Bologna}
[495]62We summarise our formalisation of an emulator for the MCS-51 microprocessor in the Matita proof assistant.
63The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
65We proceeded in two stages, first implementing in O'Caml a prototype emulator, where bugs could be `ironed out' quickly.
66We then ported our O'Caml emulator to Matita's internal language.
67Though mostly straight-forward, this porting presented multiple problems.
68Of particular interest is how we handle the extreme non-orthoganality of the MSC-51's instruction set.
69In O'Caml, this was handled through heavy use of polymorphic variants.
[501]70In Matita, we achieve the same effect through a non-standard use of dependent types.
72Both the O'Caml and Matita emulators are `executable'.
73Assembly programs may be animated within Matita, producing a trace of instructions executed.
75Our formalisation is a major component of the ongoing EU-funded CerCo project.
79% SECTION                                                                      %
[512]84Formal methods are designed to increase our confidence in the design and implementation of software (and hardware).
85Ideally, we would like all software to come equipped with a formal specification, along with a proof of correctness for the implementation.
86Today practically all programs are written in high level languages and then compiled into low level ones.
87Specifications are therefore also given at a high level and correctness can be proved by reasoning automatically or interactively on the program's source code.
88The code that is actually run, however, is not the high level source code that we reason on, but the object code that is generated by the compiler.
[512]90A few simple questions now arise:
[509]93What properties are preserved during compilation?
[509]95What properties are affected by the compilation strategy?
[509]97To what extent can you trust your compiler in preserving those properties?
[512]100These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification}.
101So far, the field has been focused on the first and last questions only.
102In particular, much attention has been placed on verifying compiler correctness with respect to extensional properties of programs, which are easily preserved during compilation; it is sufficient to completely preserve the denotational semantics of the input program.
[513]104However, if we consider intensional properties of programs---such as space, time or energy spent into computation and transmission of data---the situation is more complex.
105To express even be able to express these properties, and to be able to reason about them, we are forced to adopt a cost model that assigns a cost to single, or blocks, of instructions.
106Ideally, we would like to have a compositional cost model that assigns the same cost to all occurrences of one instruction.
107However, compiler optimizations are inherently non-compositional: each occurrence of a high level instruction is usually compiled in a different way according to the context it finds itself in.
108Therefore both the cost model and intensional specifications are affected by the compilation process.
110In the EU Project CerCo (Certified Complexity) we will approach the problem
111by developing a compiler that induces the cost model on the source code by
112assigning to each block of high level instructions the cost associated to the
113obtained object code. The cost model will thus be inherently non compositional,
114but it can be extremely \emph{precise}, capturing the realistic cost. In
115particular, we already have a prototype where no approximation of the cost
116is provided at all. The natural applications of our approach are then in the
117domain of hard real time programs, where the user can certify the meeting of
118all dealines while fully exploiting the computational time, that would be
119wasted in case of over-estimation of the costs.
121Other applications of our approach are in the domain of compiler verification
122itself. For instance, an extensional specification of an optimization is useless
123since it grants preservation of the semantics without stating that the cost
124(in space or time) of the optimized code should be lower. Another example is
125completeness and correctness of the compilation process in presence of
126space constraints: the compiler could refuse a source
127program for an embedded system when the size of the compiled code exceeds the
128available ROM size. Moreover, preservation of the semantics must be required
129only for those programs that do not exhausts their stack/heap space. Hence the
130statement of completeness of the compiler must take in account the realistic
131cost model.
133In the methodology proposed in CerCo we assume to be able to compute on the
134object code exact and realistic costs for sequential blocks of instructions.
135With modern processors, it is possible~\cite{??,??,??}, but difficult,
136to compute exact costs or to reasonably approximate them, since the execution
137of the program itself has an influence on the speed of processing. This is due
138mainly to caching effects and memory effects in the processor, used, for
139instance, to perform branch prediction. For this reason, at the current stage
140of CerCo we decided to focus on 8-bits microprocessors that are still widely
141used in embedded systems and whose cost model is easily predictable.
143In particular, we have fully formalized an executable formal semantics of
144the Family of 8 bits Freescale Microprocessors~\cite{oliboni} and a similar
145one for the MCS-51 microprocessors. The latter is the one described in this
146paper. The main focus of the formalization has been on capturing the
147intensional behaviour of the processor. The main problems we have faced,
148however, are mainly due to the extreme unorthogonality of the memory model
149and instruction sets of the MCS-51 microprocessors. To cope with this
150unorthogonality and to have executability, we have exploited the dependent
151type system of the interactive theorem prover Matita.
153%Compiler verification, as of late, is a `hot topic' in computer science research.
154%This rapidly growing field is motivated by one simple question: `to what extent can you trust your compiler?'
155%Existing verification efforts have broadly focussed on \emph{semantic correctness}, that is, creating a compiler that is guaranteed to preserve the semantics of a program during the compilation process.
156%However, there is another important facet of correctness that has not garnered much attention, that is, correctness with respect to some intensional properties of the program to be compiled.
[493]158\subsection{The 8051/8052}
161The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
162Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
163Further, the processor and its immediate successor, the 8052, is still manufactured by a host of semiconductor suppliers---many of them European---including Atmel, Siemens Semiconductor, NXP (formerly Phillips Semiconductor), Texas Instruments, and Maxim (formerly Dallas Semiconductor).
165The 8051 is a well documented processor, and has the additional support of numerous open source and commercial tools, such as compilers for high-level languages and emulators.
166For instance, the open source Small Device C Compiler (SDCC) recognises a dialect of C, and other compilers targeting the 8051 for BASIC, Forth and Modula-2 are also extant.
167An open source emulator for the processor, MCU8051 IDE, is also available.
173\caption{High level overview of the 8051 memory layout}
177The 8051 has a relatively straightforward architecture, unencumbered by advanced features of modern processors, making it an ideal target for formalisation.
178A high-level overview of the processor's memory layout is provided in Figure~\ref{fig.memory.layout}.
180Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
181Internal memory, commonly provided on the die itself with fast access, is further divided into 128 bytes of internal RAM and numerous Special Function Registers (SFRs) which control the operation of the processor.
182Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7).
183These sit in the first eight bytes of IRAM, though can be programmatically `shifted up' as needed.
184Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks.
185What remains of the IRAM may be treated as general purpose memory.
186A schematic view of IRAM layout is provided in Figure~\ref{fig.iram.layout}.
188External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
189XRAM is accessed using a dedicated instruction.
190External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
191However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
193Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
194As 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.
195For instance, the 128 bytes of extra internal RAM that the 8052 features cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used.
197The 8051 series possesses an eight bit Arithmetic and Logic Unit (ALU), with a wide variety of instructions for performing arithmetic and logical operations on bits and integers.
198Further, the processor possesses two eight bit general purpose accumulators, A and B.
200Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
201Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
202(The 8052 provides an additional sixteen bit timer.)
203As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
205The programmer may take advantage of the interrupt mechanism that the processor provides.
206This is especially useful when dealing with input or output involving the serial device, as an interrupt can be set when a whole character is sent or received via the serial port.
208Interrupts 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.
209However, interrupts may be set to one of two priorities: low and high.
210The 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.
212The 8051 has interrupts disabled by default.
213The programmer is free to handle serial input and output manually, by poking serial flags in the SFRs.
214Similarly, `exceptional circumstances' that would otherwise trigger an interrupt on more modern processors, for example, division by zero, are also signalled by setting flags.
220\caption{Schematic view of 8051 IRAM layout}
225% SECTION                                                                      %
227\subsection{Overview of paper}
[494]230In Section~\ref{sect.development.strategy} we provide a brief overview of how we designed and implemented the formalised microprocessor emulator.
231In Section~\ref{} we describe how we made use of dependent types to handle some of the idiosyncracies of the microprocessor.
232In Section~\ref{} we describe the relation our work has to
235% SECTION                                                                      %
[495]237\section{From O'Caml prototype to Matita formalisation}
[506]240Our implementation progressed in two stages:
242\paragraph{O'Caml prototype}
[506]243We began with an emulator written in O'Caml.
244We used this to `iron out' any bugs in our design and implementation within O'Caml's more permissive type system.
245O'Caml's ability to perform file input-output also eased debugging and validation.
246Once we were happy with the performance and design of the O'Caml emulator, we moved to the Matita formalisation.
248\paragraph{Matita formalisation}
[506]249Matita's syntax is lexically similar to O'Caml's.
250This eased the translation, as large swathes of code were merely copy-pasted with minor modifications.
251However, several major issues had to be addresses when moving from O'Caml to Matita.
252These are now discussed.
255% SECTION                                                                      %
[494]257\section{Design issues in the formalisation}
261% SECTION                                                                      %
[494]263\subsection{Labels and pseudoinstructions}
[508]266As part of the CerCo project, a prototype compiler was being developed in parallel with the emulator.
267Easing the design of the compiler was a key objective in implementing the emulator.
268For this reason, we introduced notion of \emph{pseudoinstruction} and \emph{label}.
[508]270The MCS-51's instruction set has numerous instructions for unconditional and conditional jumps to memory locations, calling procedures and moving data between memory spaces.
271For instance, the instructions \texttt{AJMP}, \texttt{JMP} and \texttt{LJMP} all perform unconditional jumps.
272However, these instructions differ in how large the maximum size of the offset of the jump to be performed can be.
273Further, all jump instructions require a concrete memory address, to jump to, to be specified.
274Requiring the compiler to compute these offsets, and select appropriate jump instructions, was seen as needleslly burdensome.
[508]276Instead, we introduced generic \texttt{Jump}, \texttt{Call} and \texttt{Move} instructions.
277These are expanded into MCS-51 assembly instructions with an assembly phase, prior to program execution.
278Further, we introduced a notion of label (represented by strings), and introduced pseudoinstructions that allow conditional jumps to jump to labels.
279These are also removed during the assembly phase, and replaced by concrete memory addresses and offsets.
282% SECTION                                                                      %
[511]284\subsection{Representing memory}
288% SECTION                                                                      %
[494]290\subsection{Putting dependent types to work}
[510]293We typeset O'Caml source with blue, and Matita source with red.
[508]295A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
296For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes.
298Such non-orthogonality in the instruction set was handled with the use of polymorphic variants in the O'Caml emulator.
299For instance, we introduced types corresponding to each addressing mode:
302type direct = [ `DIRECT of byte ]
303type indirect = [ `INDIRECT of bit ]
307Which were then used in our inductive datatype for assembly instructions, as follows:
310type 'addr preinstruction =
311 [ `ADD of acc * [ reg | direct | indirect | data ]
313 | `MOV of
314    (acc * [ reg | direct | indirect | data ],
315     [ reg | indirect ] * [ acc | direct | data ],
316     direct * [ acc | reg | direct | indirect | data ],
317     dptr * data16,
318     carry * bit,
319     bit * carry
320     ) union6
324Here, \texttt{union6} is a disjoint union type, defined as follows:
327type ('a,'b,'c,'d,'e,'f) union6 = [ `U1 of 'a | ... | `U6 of 'f ]
[510]330For our purposes, the types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
[510]332This polymorphic variant machinery worked well: it introduced a certain level of type safety (for instance, the type of our \texttt{MOV} instruction 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.
333However, this polymorphic variant machinery is \emph{not} present in Matita.
334We needed some way to produce the same effect, which Matita supported.
335For this task, we used dependent types.
[510]337We first provided an inductive data type representing all possible addressing modes, a type that functions will pattern match against:
[510]340inductive addressing_mode: Type[0] ≝
[495]341  DIRECT: Byte $\rightarrow$ addressing_mode
342| INDIRECT: Bit $\rightarrow$ addressing_mode
[510]346We also wished to express in the type of functions the \emph{impossibility} of pattern matching against certain constructors.
347In order to do this, we introduced an inductive type of addressing mode `tags'.
348The constructors of \texttt{addressing\_mode\_tag} are in one-to-one correspondence with the constructors of \texttt{addressing\_mode}:
[510]351inductive addressing_mode_tag : Type[0] ≝
[495]352  direct: addressing_mode_tag
353| indirect: addressing_mode_tag
[510]357A function that checks whether an \texttt{addressing\_mode} is `morally' an \texttt{addressing\_mode\_tag} is provided, as follows:
[510]360let rec is_a (d: addressing_mode_tag) (A: addressing_mode) on d ≝
[495]361  match d with
362   [ direct $\Rightarrow$ match A with [ DIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
363   | indirect $\Rightarrow$ match A with [ INDIRECT _ $\Rightarrow$ true | _ $\Rightarrow$ false ]
367We also extend this check to vectors of \texttt{addressing\_mode\_tag}'s in the obvious manner:
[510]370let rec is_in (n) (l: Vector addressing_mode_tag n) (A: addressing_mode) on l ≝
371 match l return $\lambda$m.$\lambda$_: Vector addressing_mode_tag m. bool with
[495]372  [ VEmpty $\Rightarrow$ false
373  | VCons m he (tl: Vector addressing_mode_tag m) $\Rightarrow$
374     is_a he A $\vee$ is_in ? tl A ].
377Here \texttt{VEmpty} and \texttt{VCons} are the two constructors of the \texttt{Vector} data type, and $\mathtt{\vee}$ is inclusive disjunction on Booleans.
[510]380record subaddressing_mode (n: Nat) (l: Vector addressing_mode_tag (S n)) : Type[0] ≝
382  subaddressing_modeel :> addressing_mode;
383  subaddressing_modein: bool_to_Prop (is_in ? l subaddressing_modeel)
387We can now provide an inductive type of preinstructions with precise typings:
[510]390inductive preinstruction (A: Type[0]): Type[0] ≝
[495]391   ADD: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
392 | ADDC: $\llbracket$ acc_a $\rrbracket$ $\rightarrow$ $\llbracket$ register; direct; indirect; data $\rrbracket$ $\rightarrow$ preinstruction A
396Here $\llbracket - \rrbracket$ is syntax denoting a vector.
397We see that the constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), and the second being one of a register, direct, indirect or data addressing mode.
399The final, missing 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.
400The previous machinery allows us to state in the type of a function what addressing modes that function expects.
401For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
[510]404definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$ dptr $\rrbracket$ $\rightarrow$ Status ≝
[495]405  $\lambda$s, v, a.
406   match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$ dptr $\rrbracket$ x) $\rightarrow$ ? with
407     [ DPTR $\Rightarrow$ $\lambda$_: True.
408       let 〈 bu, bl 〉 := split $\ldots$ eight eight v in
409       let status := set_8051_sfr s SFR_DPH bu in
410       let status := set_8051_sfr status SFR_DPL bl in
411         status
412     | _ $\Rightarrow$ $\lambda$_: False.
413       match K in False with
414       [
415       ]
416     ] (subaddressing_modein $\ldots$ a).
419All other cases are discharged by the catch-all at the bottom of the match expression.
420Attempting to match against another addressing mode not indicated in the type (for example, \texttt{REGISTER}) will produce a type-error.
423% SECTION                                                                      %
[511]428We spent considerable effort attempting to ensure that our formalisation is correct, that is, what we have formalised really is an accurate model of the MCS-51 microprocessor.
430First, we made use of multiple data sheets, each from a different semiconductor manufacturer.
431This helped us spot errors in the specification of the processor's instruction set, and its behaviour.
433The O'Caml prototype was especially useful for validation purposes.
434This is because we wrote a module for parsing and loading the Intel HEX file format.
435HEX is a standard format that all compilers targetting the MCS-51, and similar processors, produce.
436It is essentially a snapshot of the processor's code memory in compressed form.
437Using this, we were able to compile C programs with SDCC, an open source compiler, and load the resulting program directly into our emulator's code memory, ready for execution.
438Further, we are able to produce a HEX file from our emulator's code memory, for loading into third party tools.
439After each step of execution, we can print out both the instruction that had been executed, along with its arguments, and a snapshot of the processor's state, including all flags and register contents.
440For example:
44508: mov 81 #07
447 Processor status:                               
449   ACC : 0 (00000000) B   : 0 (00000000)
450   PSW : 0 (00000000) with flags set as:
451     CY  : false   AC  : false
452     FO  : false   RS1 : false
453     RS0 : false   OV  : false
454     UD  : false   P   : false
455   SP  : 7 (00000111) IP  : 0 (00000000)
456   PC  : 8 (0000000000001000)
457   DPL : 0 (00000000) DPH : 0 (00000000)
458   SCON: 0 (00000000) SBUF: 0 (00000000)
459   TMOD: 0 (00000000) TCON: 0 (00000000)
460   Registers:                                   
461    R0 : 0 (00000000) R1 : 0 (00000000)
462    R2 : 0 (00000000) R3 : 0 (00000000)
463    R4 : 0 (00000000) R5 : 0 (00000000)
464    R6 : 0 (00000000) R7 : 0 (00000000)
469Here, the traces indicates that the instruction \texttt{mov 81 \#07} has just been executed by the processor, which is now in the state indicated.
470These traces were useful in spotting anything that was `obviously' wrong with the execution of the program.
472Further, we made use of an open source emulator for the MCS-51, \texttt{mcu8051ide}.
473Using our execution traces, we were able to step through a compiled program, one instruction at a time, in \texttt{mcu8051ide}, and compare the resulting execution trace with the trace produced by our emulator.
475Our Matita formalisation was largely copied from the O'Caml source code, apart from changes related to addressing modes already mentioned.
476However, 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.
479% SECTION                                                                      %
[493]481\section{Related work}
485% SECTION                                                                      %
Note: See TracBrowser for help on using the repository browser.