Changeset 579


Ignore:
Timestamp:
Feb 18, 2011, 3:08:04 PM (6 years ago)
Author:
mulligan
Message:

slight tweaks

Location:
Deliverables/D4.1/ITP-Paper
Files:
2 edited

Legend:

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

    r577 r579  
     1@article
     2{ asperti:user:2007,
     3  author = {Andrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli},
     4  title = {User interaction with the {Matita} proof assistant},
     5  journal = {Journal of Automated Reasoning},
     6  pages = {109--139},
     7  volume = {39},
     8  issue = {2},
     9  year = {2007}
     10}
     11
    112@article
    213{ bate:wcet:2011,
     
    8192  author = {Jacques Garrigue},
    8293  title = {Programming with polymorphic variants},
    83   booktitle = {The {ML} Workshop},
     94  booktitle = {{ML} Workshop},
    8495  year = {1998}
    8596}
     
    130141
    131142@misc
     143{ cerco-code:2011,
     144  title = {{CerCo Deliverable D4.1}: Matita and O'Caml code},
     145  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1_Code.tar.gz}},
     146  year = {2011},
     147  key = {{CerCo-code}}
     148}
     149
     150@misc
    132151{ cerco-report:2011,
    133   title = {D4.1: executable formal semantics of machine code},
     152  title = {{CerCo Deliverable D4.1}:: executable formal semantics of machine code},
    134153  howpublished = {\url{http://cerco.cs.unibo.it/raw-attachment/wiki/WikiStart/D4_1.pdf}},
    135154  year = {2011},
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r578 r579  
    122122A user can certify that `deadlines' are met whilst wringing as many clock cycles from the processor---using a cost model that does not over-estimate---as possible.
    123123
    124 We also see our approach as being relevant to compiler verification (and construction) itself.
     124We also see our approach as being relevant to compiler verification (and construction).
    125125\emph{An optimisation specified only extensionally is only half specified}.
    126 Though the optimisation may preserve the denotational semantics of a program, there is no guarantee that any intensional properties of the program will be improved.
     126Though the optimisation may preserve the denotational semantics of a program, there is no guarantee that intensional properties of the program improve.
    127127
    128128Another potential application is toward completeness and correctness of the compilation process in the presence of space constraints.
     
    142142However, the design of the MCS-51 itself has caused problems in the formalisation.
    143143For example, the MCS-51 has a highly unorthogonal instruction set.
    144 To cope with this unorthogonality, and to produce an executable specification, we rely on Matita's dependent types.
     144To cope with this unorthogonality, and to produce an executable specification, we rely on the dependent types of Matita, an interactive proof assistant~\cite{asperti:user:2007}.
    145145
    146146\paragraph{The MCS-51}\quad
    147147The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s.
    148148Commonly called the 8051, in the decades since its introduction the processor has become a popular component of embedded systems.
    149 The processor, its successor the 8052, and derivatives are still manufactured \emph{en masse} by a host of vendors.
     149The processor and derivatives are still manufactured \emph{en masse} by a host of vendors.
    150150
    151151The 8051 is a well documented processor, and has the support of numerous open source and commercial tools, such as compilers and emulators.
     
    287287\label{sect.design.issues.formalisation}
    288288
    289 From hereonin, we typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}}.
     289We typeset O'Caml source with \texttt{\color{blue}{blue}} and Matita source with \texttt{\color{red}{red}}.
    290290Matita's syntax is straightforward if familiar with Coq or O'Caml.
    291 One subtlety is the use of `\texttt{?}' or `\texttt{$\ldots$}' in an argument position denoting an argument or arguments to be inferred, respectively.
     291One subtlety is the use of `\texttt{?}' or `\texttt{$\ldots$}' denoting an argument or arguments to be inferred, respectively.
    292292
    293293A full account of the formalisation can be found in~\cite{cerco-report:2011}.
     294All source code is available from the CerCo project website~\cite{cerco-code:2011}.
    294295
    295296\subsection{Development strategy}
     
    404405To specify global data via labels, we introduced a preamble before the program where labels and the size of reserved space for data is stored.
    405406A pseudoinstruction \texttt{Mov} moves (16-bit) data stored at a label into the MCS-51's one 16-bit register, \texttt{DPTR}.
     407(This register is used for indirect addressing of data stored in external memory.)
    406408
    407409The pseudoinstructions and labels induce an assembly language similar to that of SDCC's.
     
    443445The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
    444446An updated program counter, along with its concrete cost in processor cycles, is also returned.
    445 These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary across manufacturers and derivatives of the processor.
     447These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary between particular implementations.
    446448\begin{lstlisting}
    447449definition fetch: BitVectorTrie Byte 16 $\rightarrow$ Word $\rightarrow$ instruction $\times$ Word $\times$ nat
     
    468470\end{lstlisting}
    469471This differs from the O'Caml emulator, which executed a program indefinitely.
    470 A callback function was also accepted as an argument, which could `witness' the execution as it happened, providing a print-out of the processor state.
     472A callback function was also accepted as an argument, which `witnessed' the execution as it happened.
    471473Due to Matita's termination requirement, \texttt{execute} cannot execute a program indefinitely.
    472474An alternative approach would be to produce an infinite stream of statuses representing an execution trace.
     
    659661\label{sect.validation}
    660662
     663\begin{figure}[t]
     664\begin{scriptsize}
     665\begin{verbatim}
     66608: mov 81 #07
     667
     668 Processor status:                               
     669
     670   ACC: 0   B: 0   PSW: 0
     671    with flags set as:
     672     CY: false    AC: false   FO: false   RS1: false
     673     RS0: false   OV: false   UD: false   P: false
     674   SP: 7   IP: 0   PC: 8   DPL: 0   DPH: 0   SCON: 0
     675   SBUF: 0   TMOD: 0   TCON: 0
     676   Registers:                                   
     677    R0: 0   R1: 0   R2: 0   R3: 0   R4: 0   R5: 0   R6: 0   R7: 0
     678\end{verbatim}
     679\end{scriptsize}
     680\caption{An example snippet from an emulator execution trace}
     681\label{fig.execution.trace}
     682\end{figure}
     683
    661684We spent considerable effort attempting to ensure that what we have formalised is an accurate model of the MCS-51 microprocessor.
    662685
    663 We made use of multiple data sheets, each from a different semiconductor manufacturer.
     686We made use of multiple data sheets, each from a different manufacturer.
    664687This helped us triangulate errors in the specification of the processor's instruction set, and its behaviour, for instance, in a data sheet from Philips Semiconductor.
    665688
     
    671694Further, we can produce a HEX file from the emulator's code memory for loading into third party tools.
    672695After each step of execution, we can print out both the instruction that had been executed and a snapshot of the processor's state, including all flags and register contents.
    673 For example:
    674 \begin{frametxt}
    675 \begin{small}
    676 \begin{verbatim}
    677 ...
    678 08: mov 81 #07
    679 
    680  Processor status:                               
    681 
    682    ACC: 0   B: 0   PSW: 0
    683     with flags set as:
    684      CY: false  AC: false  FO: false  RS1: false
    685      RS0: false  OV: false UD: false  P: false
    686    SP: 7  IP: 0  PC: 8  DPL: 0  DPH: 0  SCON: 0
    687    SBUF: 0  TMOD: 0  TCON: 0
    688    Registers:                                   
    689     R0: 0  R1: 0  R2: 0  R3: 0  R4: 0  R5: 0  R6: 0  R7: 0
    690 ...
    691 \end{verbatim}
    692 \end{small}
    693 \end{frametxt}
     696
     697A snippet from an execution trace is found in Figure~\ref{fig.execution.trace}.
    694698Here, the trace indicates that the instruction \texttt{mov 81 \#07} has just been executed by the processor, which is now in the state indicated.
    695699These traces were useful in spotting anything that was `obviously' wrong with the execution of the program.
     
    697701We further used MCU 8051 IDE as a reference, which allows a user to step through an assembly program one instruction at a time.
    698702Using these execution traces, we were able to step through a compiled program in MCU 8051 IDE and compare the resulting execution trace with the trace produced by our emulator.
     703
     704We partially validated the assembly function by checking that on defined opcodes the \texttt{assembly\_1} and \texttt{fetch} functions are inverse.
    699705
    700706The Matita formalisation was largely copied from the O'Caml source code, apart from the changes already mentioned.
     
    726732Our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state.
    727733This is because Matita is based on a logic, CIC, which internalizes conversion.
    728 In~\cite{fox:trustworthy:2010} the authors provide an automation layer to derive single step theorems: if the processor is in a particular state that satisfies some preconditions, then after execution of an instruction it will reside in another state satisfying some postconditions.
     734In~\cite{fox:trustworthy:2010} the authors provide an automation layer to derive single step theorems: if the processor is in a state that satisfies some preconditions, then after execution of an instruction it will reside in a state satisfying some postconditions.
    729735We do not need single step theorems of this form.
    730736
     
    780786This assembly language is similar to those found in `industrial strength' compilers, such as SDCC.
    781787We introduce cost labels in the machine language to relate the data flow of the assembly program to that of the C source language, in order to associate costs to the C program.
    782 For the O'Caml version, we provide a parser and pretty printer from code memory to Intel HEX format.
     788For the O'Caml version, we provide a parser and pretty printer from code memory to Intel HEX.
    783789Hence we can perform testing on programs compiled using any free or commercial compiler.
    784790
Note: See TracChangeset for help on using the changeset viewer.