Changeset 519 for Deliverables/D4.1/ITPPaper
 Timestamp:
 Feb 15, 2011, 3:23:53 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/ITPPaper/itp2011.tex
r518 r519 246 246 % SECTION % 247 247 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 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 257 The MCS51 has numerous different types of memory. 258 In our prototype implementation, we simply used a map datastructure from the O'Caml standard library. 259 Matita's standard library is relatively small, and does not contain a generic map datastructure. 260 Therefore, we had the opportunity of crafting a specialpurpose datastructure for the job.s 261 262 We worked under the assumption that large swathes of memory would often be uninitialized. 263 Na\"ively, using a complete binary tree, for instance, would be extremely memory inefficient. 264 Instead, we chose to use a modified form of trie, where paths are represented by bitvectors. 265 As bitvectors were widely used in our implementation already for representing integers, this worked well: 266 \begin{quote} 267 \begin{lstlisting} 268 inductive 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} 274 Here, \texttt{Stub} is a constructor that can appear at any point in our tries. 275 It internalises the notion of `uninitialized data'. 276 Performing a lookup in memory is now straightforward. 277 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.}. 278 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. 279 280 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 281 % SECTION % 282 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 248 283 \subsection{Labels and pseudoinstructions} 249 284 \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 250 289 251 290 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. 264 303 These 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 MCS51 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 0284  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 straightforward.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.293 304 294 305 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset
for help on using the changeset viewer.