# Changeset 548

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

Fixed English in conclusion and discussion of I/O.

File:
1 edited

### Legend:

Unmodified
 r546 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 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 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: To accurately model timers and I/O, we add an unbounded integral field \texttt{clock} to the central \texttt{status} record. This 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. Before every execution step, \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 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 We use \emph{continuation} as a description of the behaviour of the environment: \begin{lstlisting} type line = [Out of (time -> line -> time * continuation)] \end{lstlisting} 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. At 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. If 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'$. Moreover the status is immediately updated with the continuation $k'$ where $\pi_2(k)(\tau,o) = \langle \tau',k' \rangle$. Further, 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'$. This input will become visible to the processor only at time $\tau' + \epsilon$. The time required to perform an I/O operation is partially specified in the data sheets of the UART module. However, this computation is complex so we prefer to abstract over it. We therefore leave the computation of the delay time to the environment. 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 how the SFRs are set. In an asyncrhonous mode, the UART transmits eight bits at a time, using a ninth line for syncrhonization. In a syncrhonous mode the ninth line is used to transmit an additional bit. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Our use of dependent types will also help to maintain invariants when we prove the correctness of the CerCo prototype compiler. 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 instructions and they over-approximate the possibilities of unorthogonality of the instruction set, dodging the problems we had to face. The most interesting idea to us in their formalization is the specification of the decode function, that is particularly error prone. What they did is to formalize in HOL a small language of patterns that is used in the data sheets of the x86, so that the decoding function is later implemented simply by copying the relevant lines from the manual into the HOL script. We are currently considering if implementing a similar solution in Matita. However, we would prefer to certify in Matita a compiler for the pattern language so that the data sheets could be compiled down to the efficient code that we provide in place of having to inefficiently interpret the data sheets every time an instruction is executed. 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. This machine code exhibits a high degree of non-uniformity similar to the MCS-51. However, 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. Further, it seems that the definition of the decode function is potentially error prone. A small domain specific language of patterns is formalised in HOL4. This is similar to the specification language of the x86 instruction set found in manufacturer's data sheets. A decode function is implemented by copying lines from data sheets into the proof script. We are currently considering implementing a similar domain specific language in Matita. However, we would prefer to certify in Matita the compiler for this language. Data 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. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%