Changeset 555 for Deliverables/D4.1/ITP-Paper/itp-2011.tex

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

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

File:
1 edited

Legend:

Unmodified
 r554 \usepackage{fancybox} \usepackage{graphicx} \usepackage[colorlinks]{hyperref} \usepackage[utf8x]{inputenc} \usepackage{listings} \institute{Dipartimento di Scienze dell'Informazione, Universit\a di Bologna} \bibliographystyle{alpha} \bibliographystyle{plain} \begin{document} To what extent can you trust your compiler in preserving those properties? \end{itemize*} 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). 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). So far, the field has been focused on the first and last questions only. In 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. In 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. With modern processors, though possible~\cite{??,??,??}, it is difficult to compute exact costs or to reasonably approximate them. With 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. This is because the execution of a program itself has an influence on the speed of processing. For instance, caching, memory effects and other advanced features such as branch prediction all have a profound effect on execution speeds. These 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. 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. In 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. The latter work is what we describe in this paper. The main focus of the formalisation has been on capturing the intensional behaviour of the processor. \end{figure} 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. 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. In 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}. 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. 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. In Matita, we are able to use the full power of dependent types to always work with vectors of a known size: The next instruction to be processed, indexed by the program counter, is fetched from code memory with \texttt{fetch}. An updated program counter, along with the concrete cost, in processor cycles for executing this instruction, is also returned. 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. 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 particular derivatives of the processor. \begin{lstlisting} definition fetch: Executability is another key difference between our work and~\cite{fox:trustworthy:2010}. Our formalisation is executable: applying the emulation function to an input state eventually reduces to an output state that already satisfies the appropriate conditions. This is because Matita is based on a logic that internalizes conversion. 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. We do not need single step theorems of this form. This is because Matita is based on a logic that internalizes conversion. 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. Our main difficulties resided in the non-uniformity of an old 8-bit architecture, in terms of the instruction set, addressing modes and memory models.