Changeset 568


Ignore:
Timestamp:
Feb 18, 2011, 10:10:49 AM (6 years ago)
Author:
mulligan
Message:

Added two missing references, reduced back down to 16 pages by rewording some sentences and gaming bibtex file

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

Legend:

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

    r557 r568  
    3636  author = {Jun Yan and Wei Zhang},
    3737  title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
    38   booktitle = {Proceedings of the Fourteenth {IEEE} Symposium on Real-time and Embedded Technology and Applications ({RTAS 2008})},
     38  booktitle = {Proceedings of the $\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
    3939  pages = {80--89},
    4040  year = {2008}
     
    4545  author = {Robert Atkey},
    4646  title = {{CoqJVM}: An executable specification of the Java virtual machine using dependent types},
    47   booktitle = {Proceedings of the Conference of the {TYPES} Project {(TYPES 2007)}},
     47  booktitle = {Proceedings of the Conference of the {TYPES} Project},
    4848  pages = {18--32},
    49   series = {Lecture Noted in Computer Science},
    50   volume = {4941},
    5149  year = {2007}
    5250}
     
    5654  author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
    5755  title = {Formal Verification of a {C} Compiler Front-End},
    58   booktitle = {Proceedings of the International Symposium on Formal Methods ({FM 2006})},
    59   series = {Lecture Notes in Computer Science},
    60   volume = {4085},
     56  booktitle = {Proceedings of the International Symposium on Formal Methods},
    6157  pages = {460--475},
    6258  year = {2006}
     
    6763  author = {Adam Chlipala},
    6864  title = {A verified compiler for an impure functional language},
    69   booktitle = {Proceedings of the Thirty Seventh Annual Symposium on Principles of Programming Languages {(POPL 2010)}},
    70   series = {{ACM SIGPLAN} Notices},
    71   volume = {45},
    72   issue = {1},
     65  booktitle = {Proceedings of the $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},
    7366  pages = {93--106},
    7467  year = {2010}
     
    7972  author = {Anthony Fox and Magnus O. Myreen},
    8073  title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
    81   booktitle = {Proceedings of the First International Conference on Interactive Theorem Proving ({ITP 2010})},
    82   series = {Lecture Notes in Computer Science},
     74  booktitle = {Proceedings of the $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
    8375  pages = {243--258},
    8476  year = {2010}
     
    9789  author = {Daan Leijen and Erik Meijer},
    9890  title = {Domain specific embedded compilers},
    99   booktitle = {Proceedings of the Second Conference on Domain Specific Languages {(DSL 1999)}},
    100   series = {{ACM SIGPLAN} Notices},
     91  booktitle = {Proceedings of the $\mathrm{2^{nd}}$ Conference on Domain Specific Languages},
    10192  pages = {109--122},
    102   volume = {2},
    10393  year = {1999}
    10494}
     
    10898  author = {Susmit Sarkar and Peter Sewell and Francesco Zappa Nardelli and Scott Owens and Tom Ridge and Thomas Braibant and Magnus O. Myreen and Jade Alglave},
    10999  title = {The semantics of {x86-CC} multiprocessor machine code},
    110   booktitle = {Proceedings of the Thirty Sixth Annual Symposium on Principles of Programming Languages {(POPL 2009)}},
    111   series = {{ACM SIGPLAN} Notices},
     100  booktitle = {Proceedings of the $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
    112101  pages = {379--391},
    113   volume = {44},
    114   issue = {1},
    115102  year = {2009}
     103}
     104
     105@inproceedings
     106{ shankar:principles:1999,
     107  author = {Natarajan Shankar and Sam Owre},
     108  title = {Principles and Pragmatics of Subtyping in {PVS}},
     109  booktitle = {Recent Trends in Algebraic Development Techniques},
     110  pages = {37--52},
     111  year = {1999}
     112}
     113
     114@inproceedings
     115{ sozeau:subset:2006,
     116  author = {Matthieu Sozeau},
     117  title = {Subset coercions in {Coq}},
     118  booktitle = {Proceedings of the Conference of the {TYPES} Project},
     119  pages = {237--252},
     120  year = {2006}
    116121}
    117122
  • Deliverables/D4.1/ITP-Paper/itp-2011.tex

    r565 r568  
    7878Both the O'Caml and Matita emulators are `executable'.
    7979Assembly programs may be animated within Matita, producing a trace of instructions executed.
    80 
    81 Our formalisation is a major component of the ongoing EU-funded CerCo project.
     80The formalisation is a major component of the ongoing EU-funded CerCo project.
    8281\end{abstract}
    8382
     
    136135These are still widely used in embedded systems, with the advantage of an easily predictable cost model due to their relative paucity of features.
    137136
    138 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.
     137We 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.
    139138The latter is what we describe in this paper.
    140139The focus of the formalisation has been on capturing the intensional behaviour of the processor.
     
    146145\label{subsect.8051-8052}
    147146
    148 The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
     147The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s.
    149148Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
    150149Further, the processor, its immediate successor the 8052, and many derivatives are still manufactured \emph{en masse} by a host of semiconductor suppliers.
     
    239238
    240239External RAM (XRAM), limited to a maximum size of 64 kilobytes, is optional, and may be provided on or off chip, depending on the manufacturer.
    241 XRAM is accessed using a dedicated instruction, and requires sixteen bits to address fully.
     240XRAM is accessed using a dedicated instruction, and requires 16 bits to address fully.
    242241External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
    243242However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied.
     
    245244Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect.
    246245As the latter two addressing modes hint, there are some restrictions enforced by the 8051 and its derivatives on which addressing modes may be used with specific types of memory.
    247 For instance, the 128 bytes of extra internal RAM that the 8052 features cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used. Moreover, some memory segments are addressed using 8 bits pointers while others require 16 bits.
    248 
    249 The 8051 series possesses an eight bit Arithmetic and Logic Unit (ALU), with a wide variety of instructions for performing arithmetic and logical operations on bits and integers.
    250 Further, the processor possesses two eight bit general purpose accumulators, A and B.
     246For instance, the 128 bytes of extra internal RAM that the 8052 features cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used. Moreover, some memory segments are addressed using 8-bit pointers while others require 16-bits.
     247
     248The 8051 possesses an 8-bit Arithmetic and Logic Unit (ALU), with a variety of instructions for performing arithmetic and logical operations on bits and integers.
     249Two 8-bit general purpose accumulators, A and B, are provided.
    251250
    252251Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
    253 Serial baud rate is determined by one of two sixteen bit timers included with the 8051, which can be set to multiple modes of operation.
    254 (The 8052 provides an additional sixteen bit timer.)
     252Serial baud rate is determined by one of two 16-bit timers included with the 8051, which can be set to multiple modes of operation.
     253(The 8052 provides an additional 16-bit timer.)
    255254As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
    256255
     
    303302We began with an emulator written in O'Caml to `iron out' any bugs in our design and implementation.
    304303O'Caml's ability to perform file I/O also eased debugging and validation.
    305 Once we were happy with the performance and design of the O'Caml emulator, we moved to the Matita formalisation.
     304Once we were happy with the design of the O'Caml emulator, we moved Matita.
    306305
    307306Matita's syntax is lexically similar to O'Caml's.
     
    342341\end{figure}
    343342
    344 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).
     343The 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).
    345344To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans.
    346345In our O'Caml emulator, we `faked' bitvectors using phantom types~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
     
    483482
    484483A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
    485 For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes out of 361.
     484For instance, the \texttt{MOV} instruction, can be invoked using one of 16 combinations of addressing modes out of a possible 361.
    486485
    487486% Show example of pattern matching with polymorphic variants
     
    564563...
    565564\end{lstlisting}
    566 We see that the constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), and the second being one of a register, direct, indirect or data addressing mode.
     565The constructor \texttt{ADD} expects two parameters, the first being the accumulator A (\texttt{acc\_a}), the second being a register, direct, indirect or data addressing mode.
    567566
    568567% One of these coercions opens up a proof obligation which needs discussing
     
    570569The final, missing component is a pair of type coercions from \texttt{addressing\_mode} to \texttt{subaddressing\_mode} and from \texttt{subaddressing\_mode} to \texttt{Type$\lbrack0\rbrack$}, respectively.
    571570The first is a forgetful coercion, while the second opens a proof obligation wherein we must prove that the provided value is in the admissible set.
    572 These coercions were first introduced by PVS to implement subset types~\cite{pvs?}, and later in Coq as an addition~\cite{russell}.
     571These coercions were first introduced by PVS to implement subset types~\cite{shankar:principles:1999}, and later in Coq as an addition~\cite{sozeau:subset:2006}.
    573572In Matita all coercions can open proof obligations.
    574573
     
    645644
    646645The UART port can work in several modes, depending on the how the SFRs are set.
    647 In an asyncrhonous mode, the UART transmits eight bits at a time, using a ninth line for syncrhonization.
     646In an asyncrhonous mode, the UART transmits 8 bits at a time, using a ninth line for syncrhonization.
    648647In a syncrhonous mode the ninth line is used to transmit an additional bit.
    649648
Note: See TracChangeset for help on using the changeset viewer.