Changeset 1200


Ignore:
Timestamp:
Sep 9, 2011, 11:03:20 AM (8 years ago)
Author:
mulligan
Message:

small changes and rewordings to decrease length

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r1199 r1200  
    7272
    7373\begin{abstract}
    74 We summarise the formalisation of two emulators for the MCS-51 microprocessor in O'Caml and the Matita proof assistant.
    75 The MCS-51 is a widely used 8-bit microprocessor, especially popular in embedded devices.
     74We summarise the formalisation of emulators for the MCS-51 microprocessor in O'Caml and the Matita proof assistant.
     75The MCS-51 is a widely used microprocessor, especially popular in embedded devices.
    7676
    7777The O'Caml emulator is intended to be `feature complete' with respect to the MCS-51 device.
     
    131131\emph{An optimisation specified only extensionally is only half specified}; the optimisation may preserve the denotational semantics of a program, but there is no guarantee that intentional properties of the program improve.
    132132
    133 Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints.
    134 A compiler could reject a source program targetting an embedded system when the size of the compiled code exceeds the available ROM size.
    135 Preservation of a program's semantics may only be required for those programs that do not exhaust the stack or heap.
     133Another potential application is the completeness and correctness of the compilation process in the presence of space constraints.
     134A compiler could reject a source program targetting an embedded system when the size of the compiled code exceeds available ROM size.
     135Preservation of semantics may only be required for those programs that do not exhaust the stack or heap.
    136136The statement of completeness of the compiler must take into account a realistic cost model.
    137137
     
    164164
    165165\paragraph*{The MCS-51}\quad
    166 The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s.
    167 Commonly called the 8051, in the decades since its introduction the processor has become a popular component of embedded systems.
    168 The processor and derivatives are still manufactured \emph{en masse} by a host of vendors.
    169 Surprisingly, however, there is not yet a formal model of the MCS-51.
     166The MCS-51 is an 8-bit microprocessor.
     167Commonly called the 8051, since its introduction by Intel the processor has become a popular component of embedded systems.
     168Despite being manufactured \emph{en masse}, there is not yet a formal model of the MCS-51.
    170169
    171170The 8051 is a well documented processor, with very few underspecified behaviours (almost all of these correspond to erroneous usage of the processor).
     
    178177\centering
    179178\setlength{\unitlength}{0.87pt}
     179\small{
    180180\begin{picture}(410,250)(-50,200)
    181181%\put(-50,200){\framebox(410,250){}}
     
    243243  \put(264,324){\makebox(80,0){Direct}}
    244244  \put(264,310){\makebox(80,0){PC relative}}
    245 \end{picture}
     245\end{picture}}
    246246\caption{The 8051 memory model}
    247247\label{fig.memory.layout}
     
    375375We may use Matita's type system to provide precise typings for functions that are polymorphic in the size without code duplication:
    376376\begin{lstlisting}[frame=single]
    377 let rec split (A: Type[0]) (m,n: nat) on m:
    378   Vector A (m+n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ...
     377let rec split (A: Type[0]) (m,n: nat) on m: Vector A (m+n) $\rightarrow$ (Vector A m)$\times$(Vector A n) := ...
    379378\end{lstlisting}
    380379
     
    390389Further, we assumed that large swathes of memory would often be uninitialized (an assumption on the behaviour of the programmer, not the processor!)
    391390
    392 We picked a modified form of trie of fixed height $h$.
    393 Paths are represented by bitvectors (already used in the implementation for addresses and registers) of length $h$:
     391We use a modified form of trie of fixed height $h$.
     392Paths are represented by bitvectors (used also for addresses and registers) of length $h$:
    394393\begin{lstlisting}[frame=single]
    395394inductive BitVectorTrie(A: Type[0]):nat $\rightarrow$ Type[0] :=
     
    405404All manufacturer data sheets that we consulted were silent on the subject of what should be returned if we attempt to access uninitialized memory.
    406405We defaulted to simply returning zero, though our \texttt{lookup} function is parametric in this choice.
    407 We believe that this is reasonable, as SDCC for instance generates code which first `zeroes' memory in a preamble before executing the program proper.
     406This is reasonable, as SDCC for instance generates code which first `zeroes' memory in a preamble before executing the program proper.
    408407This is in line with the C standard, which guarantees that all global variables will be zero initialized piecewise.
    409408
     
    535534The types \texttt{union2}, \texttt{union3} and \texttt{union6} sufficed.
    536535
    537 This 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.
     536This polymorphic variant machinery worked well: it introduced a certain level of type safety (the type of \texttt{MOV} above guarantees it cannot be invoked with arguments in the \texttt{carry} and \texttt{data16} addressing modes), and also allowed us to pattern match against instructions, when necessary.
    538537However, this polymorphic variant machinery is \emph{not} present in Matita.
    539538We needed some way to produce the same effect, which Matita supported.
     
    600599For instance, consider \texttt{set\_arg\_16}, which expects only a \texttt{DPTR}:
    601600\begin{lstlisting}[frame=single]
    602 definition set_arg_16:
    603   Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a.
    604 match a return
    605    $\lambda$x. bool_to_Prop (is_in ? $\llbracket$dptr$\rrbracket$ x) $\rightarrow$ ? with
     601definition set_arg_16: Status $\rightarrow$ Word $\rightarrow$ $\llbracket$dptr$\rrbracket$ $\rightarrow$ Status := $~\lambda$s, v, a.
     602match a return $\lambda$x. bool_to_Prop (is_in ? $\llbracket$dptr$\rrbracket$ x) $\rightarrow$ ? with
    606603  [ DPTR $\Rightarrow$ $\lambda$_: True.
    607604    let $\langle$bu, bl$\rangle$ := split $\ldots$ eight eight v in
Note: See TracChangeset for help on using the changeset viewer.