Changeset 568 for Deliverables
- Timestamp:
- Feb 18, 2011, 10:10:49 AM (10 years ago)
- Location:
- Deliverables/D4.1/ITP-Paper
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.bib
r557 r568 36 36 author = {Jun Yan and Wei Zhang}, 37 37 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}, 39 39 pages = {80--89}, 40 40 year = {2008} … … 45 45 author = {Robert Atkey}, 46 46 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}, 48 48 pages = {18--32}, 49 series = {Lecture Noted in Computer Science},50 volume = {4941},51 49 year = {2007} 52 50 } … … 56 54 author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy}, 57 55 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}, 61 57 pages = {460--475}, 62 58 year = {2006} … … 67 63 author = {Adam Chlipala}, 68 64 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}, 73 66 pages = {93--106}, 74 67 year = {2010} … … 79 72 author = {Anthony Fox and Magnus O. Myreen}, 80 73 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}, 83 75 pages = {243--258}, 84 76 year = {2010} … … 97 89 author = {Daan Leijen and Erik Meijer}, 98 90 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}, 101 92 pages = {109--122}, 102 volume = {2},103 93 year = {1999} 104 94 } … … 108 98 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}, 109 99 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}, 112 101 pages = {379--391}, 113 volume = {44},114 issue = {1},115 102 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} 116 121 } 117 122 -
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r565 r568 78 78 Both the O'Caml and Matita emulators are `executable'. 79 79 Assembly 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. 80 The formalisation is a major component of the ongoing EU-funded CerCo project. 82 81 \end{abstract} 83 82 … … 136 135 These are still widely used in embedded systems, with the advantage of an easily predictable cost model due to their relative paucity of features. 137 136 138 We have fully formalised an executable formal semantics of a family of 8 137 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. 139 138 The latter is what we describe in this paper. 140 139 The focus of the formalisation has been on capturing the intensional behaviour of the processor. … … 146 145 \label{subsect.8051-8052} 147 146 148 The MCS-51 is an eightbit microprocessor introduced by Intel in the late 1970s.147 The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s. 149 148 Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers. 150 149 Further, the processor, its immediate successor the 8052, and many derivatives are still manufactured \emph{en masse} by a host of semiconductor suppliers. … … 239 238 240 239 External 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 sixteenbits to address fully.240 XRAM is accessed using a dedicated instruction, and requires 16 bits to address fully. 242 241 External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size. 243 242 However, depending on the particular manufacturer and processor model, a dedicated on-die read-only memory area for program code (ICODE) may also be supplied. … … 245 244 Memory may be addressed in numerous ways: immediate, direct, indirect, external direct and code indirect. 246 245 As 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 16bits.248 249 The 8051 series possesses an eight bit Arithmetic and Logic Unit (ALU), with a widevariety 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.246 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-bit pointers while others require 16-bits. 247 248 The 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. 249 Two 8-bit general purpose accumulators, A and B, are provided. 251 250 252 251 Communication 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 sixteenbit timers included with the 8051, which can be set to multiple modes of operation.254 (The 8052 provides an additional sixteenbit timer.)252 Serial 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.) 255 254 As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port. 256 255 … … 303 302 We began with an emulator written in O'Caml to `iron out' any bugs in our design and implementation. 304 303 O'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.304 Once we were happy with the design of the O'Caml emulator, we moved Matita. 306 305 307 306 Matita's syntax is lexically similar to O'Caml's. … … 342 341 \end{figure} 343 342 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, 9bits).343 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). 345 344 To avoid size mismatch bugs difficult to spot, we represent all of these quantities using bitvectors, i.e. fixed length vectors of booleans. 346 345 In 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}. … … 483 482 484 483 A 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 of361.484 For instance, the \texttt{MOV} instruction, can be invoked using one of 16 combinations of addressing modes out of a possible 361. 486 485 487 486 % Show example of pattern matching with polymorphic variants … … 564 563 ... 565 564 \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 ofa register, direct, indirect or data addressing mode.565 The 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. 567 566 568 567 % One of these coercions opens up a proof obligation which needs discussing … … 570 569 The 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. 571 570 The 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}.571 These 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}. 573 572 In Matita all coercions can open proof obligations. 574 573 … … 645 644 646 645 The UART port can work in several modes, depending on the how the SFRs are set. 647 In an asyncrhonous mode, the UART transmits eightbits at a time, using a ninth line for syncrhonization.646 In an asyncrhonous mode, the UART transmits 8 bits at a time, using a ninth line for syncrhonization. 648 647 In a syncrhonous mode the ninth line is used to transmit an additional bit. 649 648
Note: See TracChangeset
for help on using the changeset viewer.