Changeset 556


Ignore:
Timestamp:
Feb 17, 2011, 2:31:07 PM (6 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r555 r556  
    306306\label{subsect.representing.memory}
    307307
    308 The MCS-51 has numerous different types of memory.
    309 In our prototype implementation, we simply used a map datastructure from the O'Caml standard library.
    310 Matita's standard library is relatively small, and does not contain a generic map datastructure.
    311 Therefore, we had the opportunity of crafting a special-purpose datastructure for the job.
    312 
    313 We worked under the assumption that large swathes of memory would often be uninitialized.
    314 Na\"ively, using a complete binary tree, for instance, would be extremely memory inefficient.
    315 Instead, we chose to use a modified form of trie, where paths are represented by bitvectors.
    316 As bitvectors were widely used in our implementation already for representing integers, this worked well:
     308The MCS-51 has numerous disjoint memory segments addressed by pointers of
     309different sizes.
     310In our prototype implementation, we simply used a map datastructure (from the O'Caml standard library) for each segment.
     311Matita'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 .
     312We also worked under the assumption that large swathes of memory would often be uninitialized, trying to represent them concisely using stubs.
     313
     314We picked a modified form of trie of fixed height $h$ where paths are
     315represented by bitvectors of length $h$, that are already used in our
     316implementation for addresses and registers:
    317317\begin{lstlisting}
    318318inductive BitVectorTrie (A: Type[0]): nat $\rightarrow$ Type[0] ≝
     
    325325Performing a lookup in memory is now straight-forward.
    326326We 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.}.
    327 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.
    328327
    329328%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.