Changeset 536

Timestamp:

Feb 16, 2011, 4:29:30 PM (9 years ago)

Author:

mulligan

Message:

more added

File:

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

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

@@ -248 +248 @@
 
 \begin{figure}[t]
-\begin{minipage}[t]{0.5\textwidth}
+\begin{minipage}[t]{0.45\textwidth}
 \vspace{0pt}
 \begin{lstlisting}
@@ -254 +254 @@
 type word = [`Sixteen] vect
 type byte = [`Eight] vect
-let from_nibble =
+$\color{blue}{\mathtt{let}}$ from_nibble =
  function
-    [b1; b2; b3; b4] -> b1,b2,b3,b4
+    [b1;b2;b3;b4] -> b1,b2,b3,b4
   | _ -> assert false
 \end{lstlisting}
 \end{minipage}
-\quad
-\begin{minipage}[t]{0.5\textwidth}
+%
+\begin{minipage}[t]{0.55\textwidth}
 \vspace{0pt}
 \begin{lstlisting}
@@ -298 +298 @@
 \label{subsect.representing.memory}
 
-% Different memory spaces are addressed with different sized pointers, and may use different addressing modes
-% Many-many map between addressing modes and memory spaces (e.g. DIRECT can be used to address low internal RAM and SFRs)
-% Maybe show snippet of get/set_arg_8?
-% Discuss overlapping memory: we implement as if disjoint memory spaces, but when we get/set we handle overlapping cases
-
 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
+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.
@@ -377 +372 @@
 This was due to a bug in Matita when we were constructing the emulator, since fixed, where the time needed to typecheck a record grew exponentially with the number of fields.
 
+Here, it appears that the MCS-51's memory spaces are completely disjoint.
+This is not so; many of them overlap with each other, and there's a many-many relationship between addressing modes and memory spaces.
+For instance, \texttt{DIRECT} addressing can be used to address low internal RAM and the SFRs, but not high internal RAM.
+
+For simplicity, we merely treat memory spaces as if they are completely disjoint in the \texttt{Status} record.
+Overlapping, and checking which addressing modes can be used to address particular memory spaces, is handled through numerous \texttt{get\_arg\_XX} and \texttt{set\_arg\_XX} (for 1, 8 and 16 bits) functions.
+
 Both the Matita and O'Caml emulators follows the classic `fetch-decode-execute' model of processor operation.
-The most important functions in the Matita emulator are highlighted below.
-
 The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
 An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
@@ -550 +550 @@
 The processor then executes the instruction, followed by the code implementing the timers.
 
-% Discuss I/O
+I/O is handled with a continuation:
+\begin{lstlisting}
+type line =
+  [ `P1 of byte | `P3 of byte
+  | `SerialBuff of [ `Eight of byte | `Nine of BitVectors.bit * byte ]]
+type continuation =
+  [`In of time * line * epsilon * continuation] option *
+  [`Out of (time -> line -> time * continuation)]
+\end{lstlisting}
+The \texttt{line} datatype signals which input/output channel is being used, either the P1 or P3 lines, or the UART port in eight or nine bit mode.
+Input and output are handled with \texttt{continuation}, 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%