Changeset 545

Timestamp:

Feb 16, 2011, 6:07:43 PM (6 years ago)

Author:

sacerdot

Message:

I/O revisited.

File:

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

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

@@ -553 +553 @@
 
 % `Real clock' for I/O and timers
-The O'Caml emulator has code for handling timers, I/O and interrupts (these are not yet ported to the Matita emulator).
+The O'Caml emulator has code for handling timers, asynchronous I/O and interrupts (these are not yet ported to the Matita emulator).
 All three of these features interact with each other in subtle ways.
 For instance, interrupts can `fire' when an input is detected on the processor's UART port, and, in certain modes, timers reset when a high signal is detected on one of the MCS-51's communication pins.
 
-To accurately model timers, we must modify the central \texttt{status} record of the emulator to keep track of the current time:
-\begin{lstlisting}
-type time = int
-type status = { ... clock: time; ... }
-\end{lstlisting}
+To accurately model timers and I/O, we add to the central \texttt{status} record of the emulator an unbounded integral field \texttt{clock} to keep track of the current time. This field is only logical, since it does not represent any quantity stored in the actual processor.
 Before every execution step, the \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute.
-The processor then executes the instruction, followed by the code implementing the timers.
-
-I/O is handled with a continuation:
+The processor then executes the instruction, followed by the code implementing the timers and I/O\footnote{Though is isn't fully specified by the manufacturer
+data sheets if I/O is handled at the beginning or the end of each cycle.}
+. In order to model I/O, we also store in the status a
+\emph{continuation} that is a description of the behaviour of the environment:
+
 \begin{lstlisting}
 type line =
@@ -574 +572 @@
   [`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.
-We use only P1 and P3 despite the MCS-51 having four output lines, P0--P3.
-This is because P0 and P2 become inoperable if the processor is equipped with XRAM (which we assume it is).
-
-Input and output are handled with \texttt{continuation}.
-In words, this type captures the following idea:
-\begin{quote}
-Starting at \texttt{time} there may or may not be an input on \texttt{line} which takes \texttt{epsilon} to complete.
-At the same time, we may wish to perform an output on \texttt{line}, in which case we will get a \texttt{time} when this transmission finishes, along with another continuation to work with.
-\end{quote}
-Handling input and output takes place at the end of every processor cycle.\footnote{Though this isn't fully specified by the manufacturer's data sheets!}
+
+At each moment, the second projection of the continuation $k$ describes how
+the environment will react to an output operation performed in the future by
+the processor: if the processor at time $\tau$ starts an asynchronous output
+$o$ either on the $P1$ or $P3$ serial lines or on the UART, then the
+environment will receive the output at time $\tau'$ and moreover
+the status is immediately updated with the continuation $k'$ where
+$ \pi_2(k)(\tau,o) = \langle \tau',k' \rangle$. Moreover, if
+$\pi_1(k) = \mathtt{Some}~\langle \tau',i,\epsilon,k'\rangle$, then at time
+$\tau'$ the environment will send the asynchronous input $i$ to the processor
+and the status will be updated with the continuation $k'$. The input will
+become visible to the processor only at time $\tau' + \epsilon$.
+
+The actual time required to perform an I/O operation is actually partially
+specified in the data sheets of the UART chip, but its computation is so
+complicated that we prefer to abstract over it, leaving to the environment
+the computation of the delay time.
+
+We use only the P1 and P3 lines despite the MCS-51 having four output lines, P0--P3. This is because P0 and P2 become inoperable if the processor is equipped with XRAM (which we assume it is). The UART port can work in several modes,
+depending on the value of some SFRs. In the asyncrhonous modes it transmits
+eight bits at a time, using a ninth line for syncrhonization. In the
+syncrhonous modes the ninth line is used to transmits an additional bit.
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%