# Changeset 562 for Deliverables/D4.1/ITP-Paper

Ignore:
Timestamp:
Feb 17, 2011, 4:41:37 PM (9 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r561 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: \emph{continuation} which is 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 event performed in the future by the processor. 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. Let $\pi_2(k)(\tau,o) = \langle \tau',k' \rangle$. 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$. Moreover the status is immediately updated with the continuation $k'$. 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'$. We spent considerable effort attempting to ensure that our formalisation is correct, that is, what we have formalised really is an accurate model of the MCS-51 microprocessor. First, we made use of multiple data sheets, each from a different semiconductor manufacturer. This helped us spot errors in the specification of the processor's instruction set, and its behaviour. First, we made use of multiple data sheets, each from a different semiconductor manufacturer.  This helped us spot errors in the specification of the processor's instruction set, and its behaviour, for instance, in a datasheet from Philips. The O'Caml prototype was especially useful for validation purposes. For example: \begin{frametxt} \begin{small} \begin{verbatim} ... ... \end{verbatim} \end{small} \end{frametxt} Here, the traces indicates that the instruction \texttt{mov 81 \#07} has just been executed by the processor, which is now in the state indicated. There exists a large body of literature on the formalisation of microprocessors. The majority of it aims to prove correctness of the implementation of the microprocessor at the microcode or gate level. However, we are interested in providing a precise specification of the behaviour of the microprocessor in order to prove the correctness of a compiler which will target the processor. We are interested in providing a precise specification of the behaviour of the microprocessor in order to prove the correctness of a compiler which will target the processor. In particular, we are interested in intensional properties of the processor; precise timings of instruction execution in clock cycles. Moreover, in addition to formalising the interface of an MCS-51 processor, we have also built a complete MCS-51 ecosystem: the UART, the I/O lines, and hardware timers, along with an assembler. This formalisation also considers the machine code level, as opposed to only considering an abstract assembly language. In particular, instruction decoding is explicitly modelled inside HOL4's logic. However, we go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction to machine code. We go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction to machine code. Further, in~\cite{fox:trustworthy:2010} the authors validated their formalisation by using development boards and random testing. However, we currently rely on non-exhaustive testing against a third party emulator. We leave similar exhaustive testing for future work. We currently rely on non-exhaustive testing against a third party emulator. We leave exhaustive testing for future work. Executability is another key difference between our work and~\cite{fox:trustworthy:2010}. In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably. Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009,blazy:formal:2006}. Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009}. CompCert concerns the certification of an ARM compiler and includes a formalisation in Coq of a subset of ARM. Coq and Matita essentially share the same logic.