Ignore:
Timestamp:
Feb 17, 2011, 2:17:11 PM (9 years ago)
Author:
mulligan
Message:

Resolved conflict, updated bibtex, finished bibliography, and llncs.cls updated to latest version.

File:
1 edited

Legend:

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

    r554 r555  
    88\usepackage{fancybox}
    99\usepackage{graphicx}
     10\usepackage[colorlinks]{hyperref}
    1011\usepackage[utf8x]{inputenc}
    1112\usepackage{listings}
     
    5859\institute{Dipartimento di Scienze dell'Informazione, Universit\`a di Bologna}
    5960
    60 \bibliographystyle{alpha}
     61\bibliographystyle{plain}
    6162
    6263\begin{document}
     
    101102To what extent can you trust your compiler in preserving those properties?
    102103\end{itemize*}
    103 These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification} (for instance~\cite{leroy:formal:2009, chlipala:verified:2010}, and many others).
     104These questions, and others like them, motivate a current `hot topic' in computer science research: \emph{compiler verification} (for instance~\cite{leroy:formal:2009,chlipala:verified:2010}, and many others).
    104105So far, the field has been focused on the first and last questions only.
    105106In particular, much attention has been placed on verifying compiler correctness with respect to extensional properties of programs, which are easily preserved during compilation; it is sufficient to completely preserve the denotational semantics of the input program.
     
    130131
    131132In the methodology proposed in CerCo we assume we are able to compute on the object code exact and realistic costs for sequential blocks of instructions.
    132 With modern processors, though possible~\cite{??,??,??}, it is difficult to compute exact costs or to reasonably approximate them.
     133With modern processors, though possible (see~\cite{bate:wcet:2011,yan:wcet:2008} for instance), it is difficult to compute exact costs or to reasonably approximate them.
    133134This is because the execution of a program itself has an influence on the speed of processing.
    134135For instance, caching, memory effects and other advanced features such as branch prediction all have a profound effect on execution speeds.
     
    136137These are still widely used in embedded systems, and have the advantage of an easily predictable cost model due to the relative sparcity of features that they possess.
    137138
    138 In particular, we have fully formalised an executable formal semantics of a family of 8 bit Freescale Microprocessors~\cite{oliboni}, and provided a similar executable formal semantics for the MCS-51 microprocessor.
     139In particular, we have fully formalised an executable formal semantics of a family of 8 bit Freescale Microprocessors~\cite{oliboni:matita:2008}, and provided a similar executable formal semantics for the MCS-51 microprocessor.
    139140The latter work is what we describe in this paper.
    140141The main focus of the formalisation has been on capturing the intensional behaviour of the processor.
     
    279280\end{figure}
    280281
    281 The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits). To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
     282The formalization of MCS-51 must deal with bytes (8 bits), words (16 bits) but also with more exoteric quantities (7 bits, 3 bits, 9 bits).
     283To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
    282284In our O'Caml emulator, we `faked' bitvectors using phantom types implemented with polymorphic variants\cite{phantom_types_ocaml}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
    283 From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes. However, the module's interface (right column) enforces the size invariants in the rest of the code.
     285From within the bitvector module (left column) bitvectors are just lists of bits and no guarantee is provided on sizes.
     286However, the module's interface (right column) enforces the size invariants in the rest of the code.
    284287
    285288In Matita, we are able to use the full power of dependent types to always work with vectors of a known size:
     
    387390The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}.
    388391An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned.
    389 These costs are taken from a Siemen's data sheet for the MCS-51, and will likely vary across manufacturers and particular derivatives of the processor.
     392These costs are taken from a Siemens Semiconductor Group data sheet for the MCS-51~\cite{siemens:2011}, and will likely vary across manufacturers and particular derivatives of the processor.
    390393\begin{lstlisting}
    391394definition fetch:
     
    680683
    681684Executability is another key difference between our work and~\cite{fox:trustworthy:2010}.
     685Our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state that already satisfies the appropriate conditions.
     686This is because Matita is based on a logic that internalizes conversion.
    682687In~\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.
    683688We do not need single step theorems of this form.
    684 This is because Matita is based on a logic that internalizes conversion.
    685 As a result, our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state that already satisfies the appropriate conditions.
    686689
    687690Our main difficulties resided in the non-uniformity of an old 8-bit architecture, in terms of the instruction set, addressing modes and memory models.
Note: See TracChangeset for help on using the changeset viewer.