Changeset 556 for Deliverables

Timestamp:

Feb 17, 2011, 2:31:07 PM (10 years ago)

Author:

sacerdot

Message:

...

File:

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

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

@@ -306 +306 @@
 \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.
-
-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:
+The MCS-51 has numerous disjoint memory segments addressed by pointers of
+different sizes.
+In our prototype implementation, we simply used a map datastructure (from the O'Caml standard library) for each segment.
+Matita's standard library is relatively small, and does not contain a generic map datastructure. Therefore, we had the opportunity of crafting a dependently typed special-purpose datastructure for the job to enforce the correspondence between the size of pointers and the size of the segment .
+We also worked under the assumption that large swathes of memory would often be uninitialized, trying to represent them concisely using stubs.
+
+We picked a modified form of trie of fixed height $h$ where paths are
+represented by bitvectors of length $h$, that are already used in our
+implementation for addresses and registers:
 \begin{lstlisting}
 inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
@@ -325 +325 @@
 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.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%