Changeset 548


Ignore:
Timestamp:
Feb 17, 2011, 10:50:02 AM (6 years ago)
Author:
mulligan
Message:

Fixed English in conclusion and discussion of I/O.

File:
1 edited

Legend:

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

    r546 r548  
    558558For 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.
    559559
    560 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.
    561 Before every execution step, the \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute.
    562 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
    563 data sheets if I/O is handled at the beginning or the end of each cycle.}
    564 . In order to model I/O, we also store in the status a
    565 \emph{continuation} that is a description of the behaviour of the environment:
    566 
     560To accurately model timers and I/O, we add an unbounded integral field \texttt{clock} to the central \texttt{status} record.
     561This field is only logical, since it does not represent any quantity stored in the actual processor, and is used to keep track of the current processor time.
     562Before every execution step, \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute.
     563The processor then executes the instruction, followed by the code implementing the timers and I/O\footnote{Though it isn't fully specified by the manufacturer's 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
     564We use \emph{continuation} as a description of the behaviour of the environment:
    567565\begin{lstlisting}
    568566type line =
     
    573571  [`Out of (time -> line -> time * continuation)]
    574572\end{lstlisting}
    575 
    576 At each moment, the second projection of the continuation $k$ describes how
    577 the environment will react to an output operation performed in the future by
    578 the processor: if the processor at time $\tau$ starts an asynchronous output
    579 $o$ either on the $P1$ or $P3$ serial lines or on the UART, then the
    580 environment will receive the output at time $\tau'$ and moreover
    581 the status is immediately updated with the continuation $k'$ where
    582 $ \pi_2(k)(\tau,o) = \langle \tau',k' \rangle$. Moreover, if
    583 $\pi_1(k) = \mathtt{Some}~\langle \tau',i,\epsilon,k'\rangle$, then at time
    584 $\tau'$ the environment will send the asynchronous input $i$ to the processor
    585 and the status will be updated with the continuation $k'$. The input will
    586 become visible to the processor only at time $\tau' + \epsilon$.
    587 
    588 The actual time required to perform an I/O operation is actually partially
    589 specified in the data sheets of the UART chip, but its computation is so
    590 complicated that we prefer to abstract over it, leaving to the environment
    591 the computation of the delay time.
    592 
    593 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,
    594 depending on the value of some SFRs. In the asyncrhonous modes it transmits
    595 eight bits at a time, using a ninth line for syncrhonization. In the
    596 syncrhonous modes the ninth line is used to transmits an additional bit.
     573At each moment, the second projection of the continuation $k$ describes how the environment will react to an output event performed in the future by the processor.
     574If the processor at time $\tau$ starts an asynchronous output $o$ either on the P1 or P3 output lines, or on the UART, then the environment will receive the output at time $\tau'$.
     575Moreover the status is immediately updated with the continuation $k'$ where $\pi_2(k)(\tau,o) = \langle \tau',k' \rangle$.
     576
     577Further, 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'$.
     578This input will become visible to the processor only at time $\tau' + \epsilon$.
     579
     580The time required to perform an I/O operation is partially specified in the data sheets of the UART module.
     581However, this computation is complex so we prefer to abstract over it.
     582We therefore leave the computation of the delay time to the environment.
     583
     584We use only the P1 and P3 lines despite the MCS-51 having four output lines, P0--P3.
     585This is because P0 and P2 become inoperable if the processor is equipped with XRAM (which we assume it is).
     586
     587The UART port can work in several modes, depending on the how the SFRs are set.
     588In an asyncrhonous mode, the UART transmits eight bits at a time, using a ninth line for syncrhonization.
     589In a syncrhonous mode the ninth line is used to transmit an additional bit.
    597590
    598591%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
     
    709702Our use of dependent types will also help to maintain invariants when we prove the correctness of the CerCo prototype compiler.
    710703
    711 Finally, in~\cite{Susmit Sarkar, Pater Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant Magnus O. Myreen, and Jade Alglave. The semantics of x86-CC multiprocessor machine code. In Principles of Programming Languages (POPL). ACM, 2009.} Sarkar et al provide an executable semantics for x86-CC multiprocessor machine code, which exhibits an high degree of non uniformity as the 8051. However, they only consider a very small subset of the
    712 instructions and they over-approximate the possibilities of unorthogonality of
    713 the instruction set, dodging the problems we had to face.
    714 The most interesting idea to us in their formalization is the specification of
    715 the decode function, that is particularly error prone. What they did is to
    716 formalize in HOL a small language of patterns that is used in the data sheets
    717 of the x86, so that the decoding function is later implemented simply by
    718 copying the relevant lines from the manual into the HOL script.
    719 We are currently considering if implementing a similar solution in Matita.
    720 However, we would prefer to certify in Matita a compiler for the pattern
    721 language so that the data sheets could be compiled down to the efficient code
    722 that we provide in place of having to inefficiently interpret the data sheets
    723 every time an instruction is executed.
    724 
     704Finally, in~\cite{Susmit Sarkar, Pater Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant Magnus O. Myreen, and Jade Alglave. The semantics of x86-CC multiprocessor machine code. In Principles of Programming Languages (POPL). ACM, 2009.} Sarkar et al provide an executable semantics for x86-CC multiprocessor machine code.
     705This machine code exhibits a high degree of non-uniformity similar to the MCS-51.
     706However, only a very small subset of the instruction set is considered, and they over-approximate the possibilities of unorthogonality of the instruction set, largely dodging the problems we had to face.
     707
     708Further, it seems that the definition of the decode function is potentially error prone.
     709A small domain specific language of patterns is formalised in HOL4.
     710This is similar to the specification language of the x86 instruction set found in manufacturer's data sheets.
     711A decode function is implemented by copying lines from data sheets into the proof script.
     712
     713We are currently considering implementing a similar domain specific language in Matita.
     714However, we would prefer to certify in Matita the compiler for this language.
     715Data sheets could then be compiled down to the efficient code that we currently provide, instead of inefficiently interpreting the data sheets every time an instruction is executed.
    725716
    726717%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset for help on using the changeset viewer.