Changeset 519


Ignore:
Timestamp:
Feb 15, 2011, 3:23:53 PM (6 years ago)
Author:
mulligan
Message:

Footnote fixed

File:
1 edited

Legend:

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

    r518 r519  
    246246% SECTION                                                                      %
    247247%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     248\subsection{Representation of integers}
     249\label{subsect.representation.integers}
     250
     251%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     252% SECTION                                                                      %
     253%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     254\subsection{Representing memory}
     255\label{subsect.representing.memory}
     256
     257The MCS-51 has numerous different types of memory.
     258In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
     259Matita's standard library is relatively small, and does not contain a generic map datastructure.
     260Therefore, we had the opportunity of crafting a special-purpose datastructure for the job.s
     261
     262We worked under the assumption that large swathes of memory would often be uninitialized.
     263Na\"ively, using a complete binary tree, for instance, would be extremely memory inefficient.
     264Instead, we chose to use a modified form of trie, where paths are represented by bitvectors.
     265As bitvectors were widely used in our implementation already for representing integers, this worked well:
     266\begin{quote}
     267\begin{lstlisting}
     268inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
     269  Leaf: A $\rightarrow$ BitVectorTrie A 0
     270| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
     271| Stub: ∀n. BitVectorTrie A n.
     272\end{lstlisting}
     273\end{quote}
     274Here, \texttt{Stub} is a constructor that can appear at any point in our tries.
     275It internalises the notion of `uninitialized data'.
     276Performing a lookup in memory is now straight-forward.
     277We 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.  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.}.
     278As 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.
     279
     280%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     281% SECTION                                                                      %
     282%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    248283\subsection{Labels and pseudoinstructions}
    249284\label{subsect.labels.pseudoinstructions}
     285
     286% Compare to SDCC assembly
     287% Need labels for separate compilation, should we implement it at a later date
     288% Discuss Move instruction more, and labels for the GLOBALS
    250289
    251290As part of the CerCo project, a prototype compiler was being developed in parallel with the emulator.
     
    263302Further, we introduced a notion of label (represented by strings), and introduced pseudoinstructions that allow conditional jumps to jump to labels.
    264303These are also removed during the assembly phase, and replaced by concrete memory addresses and offsets.
    265 
    266 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    267 % SECTION                                                                      %
    268 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
    269 \subsection{Representing memory}
    270 \label{subsect.representing.memory}
    271 
    272 The MCS-51 has numerous different types of memory.
    273 In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
    274 However, when moving to Matita, we aimed to improve our treatment of memory.
    275 
    276 We worked under the assumption that large swathes of memory would often be uninitialized.
    277 Using a complete binary tree, for instance, would therefore be extremely memory inefficient.
    278 Instead, we chose to use a modified form of trie, where paths are represented by bitvectors.
    279 As bitvectors were widely used in our implementation already for representing integers, this worked well:
    280 \begin{quote}
    281 \begin{lstlisting}
    282 inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
    283   Leaf: A $\rightarrow$ BitVectorTrie A 0
    284 | Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
    285 | Stub: ∀n. BitVectorTrie A n.
    286 \end{lstlisting}
    287 \end{quote}
    288 Here, \texttt{Stub} is a constructor that can appear at any point in our tries.
    289 It internalises the notion of `uninitialized data'.
    290 Performing a lookup in memory is now straight-forward.
    291 We 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.}.
    292 As 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.
    293304
    294305%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.