Changeset 570


Ignore:
Timestamp:
Feb 18, 2011, 10:57:24 AM (6 years ago)
Author:
mulligan
Message:

Tightened English up to Subsection 2.5

File:
1 edited

Legend:

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

    r569 r570  
    288288\label{sect.design.issues.formalisation}
    289289
    290 From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}} to distinguish the two syntaxes.
    291 Matita's syntax is largely straightforward to those familiar with Coq or O'Caml.
    292 The only subtlety is the use of `\texttt{?}' in an argument position denoting an argument that should be inferred automatically.
     290From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}}.
     291Matita's syntax is straightforward if familiar with Coq or O'Caml.
     292One subtlety is the use of `\texttt{?}' in an argument position denoting an argument to be inferred.
    293293
    294294A full account of the formalisation can be found in~\cite{cerco-report:2011}.
     
    298298
    299299Our implementation progressed in two stages.
    300 We began with an emulator written in O'Caml to `iron out' any bugs in our design and implementation.
     300We began with an emulator written in O'Caml to `iron out' any bugs in the design and implementation.
    301301O'Caml's ability to perform file I/O also eased debugging and validation.
    302 Once we were happy with the design of the O'Caml emulator, we moved Matita.
     302Once we were happy with the design of the O'Caml emulator, we moved to Matita.
    303303
    304304Matita's syntax is lexically similar to O'Caml's.
    305 This eased the translation, as code was merely copied with minor modifications.
     305This eased the translation, as swathes of code were copied with minor modifications.
    306306However, several major issues had to be addresses when moving from to Matita.
    307307These are now discussed.
     
    339339\end{figure}
    340340
    341 The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits) but also with more exoteric quantities (7-bits, 3-bits, 9-bits).
    342 To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
     341The formalization of MCS-51 must deal with bytes (8-bits), words (16-bits), and also more exoteric quantities (7, 3 and 9-bits).
     342To avoid difficult-to-trace size mismatch bugs, we represented all quantities using bitvectors, i.e. fixed length vectors of booleans.
    343343In our 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}.
    344344From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
    345 However, the module's interface (right column) enforces the size invariants in the rest of the code.
     345However, the module's interface (right column) enforces size invariants in the rest of the code.
    346346
    347347In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
     
    352352\end{lstlisting}
    353353We define \texttt{BitVector} as a specialization of \texttt{Vector} to \texttt{bool}.
    354 We may use Matita's type system to provide precise typing for functions that are
    355 polymorphic in the size without having to duplicate the code as we did in O'Caml:
     354We may use Matita's type system to provide precise typings for functions that are polymorphic in the size without code duplication:
    356355\begin{lstlisting}
    357356let rec split (A: Type[0]) (m,n: nat) on m:
     
    365364\label{subsect.representing.memory}
    366365
    367 The MCS-51 has numerous disjoint memory spaces addressed by pointers of different sizes.
    368 In our prototype implementation, we use a map data structure (from O'Caml's standard library) for each space.
     366The MCS-51 has numerous disjoint memory spaces addressed by differently sized pointers.
     367In our O'Caml implementation, we use a map data structure (from the standard library) for each space.
    369368Matita's standard library is small, and does not contain a generic map data structure.
    370369We 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.
    371 We assumed that large swathes of memory would often be uninitialized.
     370Further, we assumed that large swathes of memory would often be uninitialized.
    372371
    373372We picked a modified form of trie of fixed height $h$.
     
    382381It represents `uninitialized data'.
    383382Performing a lookup in memory is now straight-forward.
    384 We traverse a path, and if we encounter \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.}.
     383The only subtlety over normal trie lookup is how we handle \texttt{Stub}.
     384We 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.}.
    385385
    386386%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    399399Further, all jump instructions require a concrete memory address---to jump to---to be specified.
    400400Compilers that support separate compilation cannot directly compute these offsets and select the appropriate jump instructions.
    401 These operations are also burdensome for compilers that do not do separate compilation and are handled by the assemblers, as we decided to do.
     401These operations are also burdensome for compilers that do not do separate compilation and are handled by assemblers.
     402We followed suit.
    402403
    403404While introducing pseudoinstructions, we also introduced labels for locations to jump to, and for global data.
    404 To specify global data via labels, we introduced a preamble before the program where labels and the size of reserved space for data is associated.
    405 A pseudoinstruction \texttt{Mov} moves (16-bit) data stored at a label into the (16-bit) register \texttt{DPTR}.
    406 
    407 Our pseudoinstructions and labels induce an assembly language similar to that of SDCC.
     405To specify global data via labels, we introduced a preamble before the program where labels and the size of reserved space for data is stored.
     406A pseudoinstruction \texttt{Mov} moves (16-bit) data stored at a label into the MCS-51's one 16-bit register, \texttt{DPTR}.
     407
     408Our pseudoinstructions and labels induce an assembly language similar to that of SDCC's.
    408409All pseudoinstructions and labels are `assembled away' prior to program execution.
    409410Jumps are computed in two stages.
    410 A map associating memory addresses to labels is built, before removing pseudojumps with concrete jumps to the correct address.
    411 The algorithm currently implemented does not try to minimize the object code size by always picking the shortest possible jump instruction.
    412 A better algorithm is currently left for future work.
     411A map associating memory addresses to labels is built, before replacing pseudojumps with concrete jumps to the correct address.
     412The algorithm currently implemented does not try to minimize object code size by picking the shortest possible jump instruction.
     413A better algorithm is left for future work.
    413414
    414415%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.