Changeset 545
- Timestamp:
- Feb 16, 2011, 6:07:43 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r544 r545 553 553 554 554 % `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).555 The O'Caml emulator has code for handling timers, asynchronous I/O and interrupts (these are not yet ported to the Matita emulator). 556 556 All three of these features interact with each other in subtle ways. 557 557 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. 558 558 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} 559 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. 564 560 Before 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: 561 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 562 data 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 568 566 \begin{lstlisting} 569 567 type line = … … 574 572 [`Out of (time -> line -> time * continuation)] 575 573 \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 575 At each moment, the second projection of the continuation $k$ describes how 576 the environment will react to an output operation performed in the future by 577 the 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 579 environment will receive the output at time $\tau'$ and moreover 580 the 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 584 and the status will be updated with the continuation $k'$. The input will 585 become visible to the processor only at time $\tau' + \epsilon$. 586 587 The actual time required to perform an I/O operation is actually partially 588 specified in the data sheets of the UART chip, but its computation is so 589 complicated that we prefer to abstract over it, leaving to the environment 590 the computation of the delay time. 591 592 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, 593 depending on the value of some SFRs. In the asyncrhonous modes it transmits 594 eight bits at a time, using a ninth line for syncrhonization. In the 595 syncrhonous modes the ninth line is used to transmits an additional bit. 587 596 588 597 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset
for help on using the changeset viewer.