Changeset 516


Ignore:
Timestamp:
Feb 15, 2011, 2:12:45 PM (6 years ago)
Author:
mulligan
Message:

Added section on Tries

File:
1 edited

Legend:

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

    r515 r516  
    163163Processor RAM is divided into numerous segments, with the most prominent division being between internal and (optional) external memory.
    164164Internal 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.
    165 Internal RAM (IRAM) is further divided into a eight general purpose bit-addressable registers (R0--R7).
     165Internal RAM (IRAM) is further divided into eight general purpose bit-addressable registers (R0--R7).
    166166These sit in the first eight bytes of IRAM, though can be programmatically `shifted up' as needed.
    167 Bit memory, followed by a small amount of stack space resides in the memory space immediately after the register banks.
     167Bit memory, followed by a small amount of stack space, resides in the memory space immediately after the register banks.
    168168What remains of the IRAM may be treated as general purpose memory.
    169169A schematic view of IRAM layout is provided in Figure~\ref{fig.iram.layout}.
    170170
    171 External RAM (XRAM), limited to 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
    172 XRAM is accessed using a dedicated instruction.
     171External RAM (XRAM), limited to a maximum size of 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
     172XRAM is accessed using a dedicated instruction, and requires sixteen bits to address fully.
    173173External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
    174174However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
     
    218218% SECTION                                                                      %
    219219%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     220\subsection{Emulator architecture}
     221\label{subsect.emulator.architecture}
     222
     223%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     224% SECTION                                                                      %
     225%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    220226\section{From O'Caml prototype to Matita formalisation}
    221227\label{sect.from.o'caml.prototype.matita.formalisation}
     
    267273\subsection{Representing memory}
    268274\label{subsect.representing.memory}
     275
     276The MCS-51 has numerous different types of memory.
     277In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
     278However, when moving to Matita, we aimed to improve our treatment of memory.
     279
     280We worked under the assumption that large swathes of memory would often be uninitialized.
     281Using a complete binary tree, for instance, would therefore be extremely memory inefficient.
     282Instead, we chose to use a modified form of trie, where paths are represented by bitvectors.
     283As bitvectors were widely used in our implementation already for representing integers, this worked well:
     284\begin{quote}
     285\begin{lstlisting}
     286inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
     287  Leaf: A $\rightarrow$ BitVectorTrie A 0
     288| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
     289| Stub: ∀n. BitVectorTrie A n.
     290\end{lstlisting}
     291\end{quote}
     292Here, \texttt{Stub} is a constructor that can appear at any point in our tries.
     293It internalises the notion of `uninitialized data'.
     294Performing a lookup in memory is now straight-forward.
     295We merely traverse a path, and if at any point we encounter a \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.}.
     296As we are using bitvectors, we may make full use of dependent types and ensure that our bitvector paths are of the same length as the height of the tree.
    269297
    270298%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.