Changeset 562


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

...

File:
1 edited

Legend:

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

    r561 r562  
    635635Before every execution step, \texttt{clock} is incremented by the number of processor cycles that the instruction just fetched will take to execute.
    636636The 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
    637 We use \emph{continuation} as a description of the behaviour of the environment:
     637\emph{continuation} which is a description of the behaviour of the environment:
    638638\begin{lstlisting}
    639639type line =
     
    644644  [`Out of (time -> line -> time * continuation)]
    645645\end{lstlisting}
    646 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.
     646At 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$.
    647647If 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'$.
    648 Moreover the status is immediately updated with the continuation $k'$ where $\pi_2(k)(\tau,o) = \langle \tau',k' \rangle$.
     648Moreover the status is immediately updated with the continuation $k'$.
    649649
    650650Further, 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'$.
     
    685685We 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.
    686686
    687 First, we made use of multiple data sheets, each from a different semiconductor manufacturer.
    688 This helped us spot errors in the specification of the processor's instruction set, and its behaviour.
     687First, 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.
    689688
    690689The O'Caml prototype was especially useful for validation purposes.
     
    697696For example:
    698697\begin{frametxt}
     698\begin{small}
    699699\begin{verbatim}
    700700...
     
    713713...
    714714\end{verbatim}
     715\end{small}
    715716\end{frametxt}
    716717Here, the traces indicates that the instruction \texttt{mov 81 \#07} has just been executed by the processor, which is now in the state indicated.
     
    730731There exists a large body of literature on the formalisation of microprocessors.
    731732The majority of it aims to prove correctness of the implementation of the microprocessor at the microcode or gate level.
    732 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.
     733 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.
    733734In particular, we are interested in intensional properties of the processor; precise timings of instruction execution in clock cycles.
    734735Moreover, 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.
     
    738739This formalisation also considers the machine code level, as opposed to only considering an abstract assembly language.
    739740In particular, instruction decoding is explicitly modelled inside HOL4's logic.
    740 However, we go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction to machine code.
     741We go further in also providing an assembly language, complete with assembler, to translate instructions and pseudoinstruction to machine code.
    741742
    742743Further, in~\cite{fox:trustworthy:2010} the authors validated their formalisation by using development boards and random testing.
    743 However, we currently rely on non-exhaustive testing against a third party emulator.
    744 We leave similar exhaustive testing for future work.
     744We currently rely on non-exhaustive testing against a third party emulator.
     745We leave exhaustive testing for future work.
    745746
    746747Executability is another key difference between our work and~\cite{fox:trustworthy:2010}.
     
    753754In contrast, the ARM instruction set and memory model is relatively uniform, simplifying any formalisation considerably.
    754755
    755 Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009,blazy:formal:2006}.
     756Perhaps the closest project to CerCo is CompCert~\cite{leroy:formal:2009,leroy:formally:2009}.
    756757CompCert concerns the certification of an ARM compiler and includes a formalisation in Coq of a subset of ARM.
    757758Coq and Matita essentially share the same logic.
Note: See TracChangeset for help on using the changeset viewer.