Changeset 545


Ignore:
Timestamp:
Feb 16, 2011, 6:07:43 PM (6 years ago)
Author:
sacerdot
Message:

I/O revisited.

File:
1 edited

Legend:

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

    r544 r545  
    553553
    554554% `Real clock' for I/O and timers
    555 The O'Caml emulator has code for handling timers, I/O and interrupts (these are not yet ported to the Matita emulator).
     555The O'Caml emulator has code for handling timers, asynchronous I/O and interrupts (these are not yet ported to the Matita emulator).
    556556All three of these features interact with each other in subtle ways.
    557557For 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.
    558558
    559 To accurately model timers, we must modify the central \texttt{status} record of the emulator to keep track of the current time:
    560 \begin{lstlisting}
    561 type time = int
    562 type status = { ... clock: time; ... }
    563 \end{lstlisting}
     559To 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.
    564560Before every execution step, the \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute.
    565 The processor then executes the instruction, followed by the code implementing the timers.
    566 
    567 I/O is handled with a continuation:
     561The 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
     562data sheets if I/O is handled at the beginning or the end of each cycle.}
     563. In order to model I/O, we also store in the status a
     564\emph{continuation} that is a description of the behaviour of the environment:
     565
    568566\begin{lstlisting}
    569567type line =
     
    574572  [`Out of (time -> line -> time * continuation)]
    575573\end{lstlisting}
    576 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.
    577 We use only P1 and P3 despite the MCS-51 having four output lines, P0--P3.
    578 This is because P0 and P2 become inoperable if the processor is equipped with XRAM (which we assume it is).
    579 
    580 Input and output are handled with \texttt{continuation}.
    581 In words, this type captures the following idea:
    582 \begin{quote}
    583 Starting at \texttt{time} there may or may not be an input on \texttt{line} which takes \texttt{epsilon} to complete.
    584 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.
    585 \end{quote}
    586 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!}
     574
     575At each moment, the second projection of the continuation $k$ describes how
     576the environment will react to an output operation performed in the future by
     577the processor: if the processor at time $\tau$ starts an asynchronous output
     578$o$ either on the $P1$ or $P3$ serial lines or on the UART, then the
     579environment will receive the output at time $\tau'$ and moreover
     580the status is immediately updated with the continuation $k'$ where
     581$ \pi_2(k)(\tau,o) = \langle \tau',k' \rangle$. Moreover, if
     582$\pi_1(k) = \mathtt{Some}~\langle \tau',i,\epsilon,k'\rangle$, then at time
     583$\tau'$ the environment will send the asynchronous input $i$ to the processor
     584and the status will be updated with the continuation $k'$. The input will
     585become visible to the processor only at time $\tau' + \epsilon$.
     586
     587The actual time required to perform an I/O operation is actually partially
     588specified in the data sheets of the UART chip, but its computation is so
     589complicated that we prefer to abstract over it, leaving to the environment
     590the computation of the delay time.
     591
     592We 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,
     593depending on the value of some SFRs. In the asyncrhonous modes it transmits
     594eight bits at a time, using a ninth line for syncrhonization. In the
     595syncrhonous modes the ninth line is used to transmits an additional bit.
    587596
    588597%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.