Changeset 519

Timestamp:

Feb 15, 2011, 3:23:53 PM (10 years ago)

Author:

mulligan

Message:

Footnote fixed

File:

• Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) (2 diffs)

Deliverables/D4.1/ITP-Paper/itp-2011.tex

@@ -246 +246 @@
 % SECTION                                                                      %
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Representation of integers}
+\label{subsect.representation.integers}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% SECTION                                                                      %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\subsection{Representing memory}
+\label{subsect.representing.memory}
+
+The MCS-51 has numerous different types of memory.
+In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
+Matita's standard library is relatively small, and does not contain a generic map datastructure.
+Therefore, we had the opportunity of crafting a special-purpose datastructure for the job.s
+
+We worked under the assumption that large swathes of memory would often be uninitialized.
+Na\"ively, using a complete binary tree, for instance, would be extremely memory inefficient.
+Instead, we chose to use a modified form of trie, where paths are represented by bitvectors.
+As bitvectors were widely used in our implementation already for representing integers, this worked well:
+\begin{quote}
+\begin{lstlisting}
+inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
+  Leaf: A $\rightarrow$ BitVectorTrie A 0
+| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
+| Stub: ∀n. BitVectorTrie A n.
+\end{lstlisting}
+\end{quote}
+Here, \texttt{Stub} is a constructor that can appear at any point in our tries.
+It internalises the notion of `uninitialized data'.
+Performing a lookup in memory is now straight-forward.
+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.  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.}.
+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.
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% SECTION                                                                      %
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \subsection{Labels and pseudoinstructions}
 \label{subsect.labels.pseudoinstructions}
+
+% Compare to SDCC assembly
+% Need labels for separate compilation, should we implement it at a later date
+% Discuss Move instruction more, and labels for the GLOBALS
 
 As part of the CerCo project, a prototype compiler was being developed in parallel with the emulator.
@@ -263 +302 @@
 Further, we introduced a notion of label (represented by strings), and introduced pseudoinstructions that allow conditional jumps to jump to labels.
 These are also removed during the assembly phase, and replaced by concrete memory addresses and offsets.
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-% SECTION                                                                      %
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\subsection{Representing memory}
-\label{subsect.representing.memory}
-
-The MCS-51 has numerous different types of memory.
-In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
-However, when moving to Matita, we aimed to improve our treatment of memory.
-
-We worked under the assumption that large swathes of memory would often be uninitialized.
-Using a complete binary tree, for instance, would therefore be extremely memory inefficient.
-Instead, we chose to use a modified form of trie, where paths are represented by bitvectors.
-As bitvectors were widely used in our implementation already for representing integers, this worked well:
-\begin{quote}
-\begin{lstlisting}
-inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
-  Leaf: A $\rightarrow$ BitVectorTrie A 0
-| Node: ∀n. BitVectorTrie A n $\rightarrow$ BitVectorTrie A n $\rightarrow$ BitVectorTrie A (S n)
-| Stub: ∀n. BitVectorTrie A n.
-\end{lstlisting}
-\end{quote}
-Here, \texttt{Stub} is a constructor that can appear at any point in our tries.
-It internalises the notion of `uninitialized data'.
-Performing a lookup in memory is now straight-forward.
-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.}.
-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.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%