Changeset 568 for Deliverables

Timestamp:

Feb 18, 2011, 10:10:49 AM (10 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:

• itp-2011.bib (modified) (7 diffs)
• itp-2011.tex (modified) (11 diffs)

Deliverables/D4.1/ITP-Paper/itp-2011.bib

@@ -36 +36 @@
   author = {Jun Yan and Wei Zhang},
   title = {{WCET} Analysis for Multi-Core Processors with Shared {L2} Instruction Caches},
-  booktitle = {Proceedings of the Fourteenth {IEEE} Symposium on Real-time and Embedded Technology and Applications ({RTAS 2008})},
+  booktitle = {Proceedings of the $\mathrm{14^{th}}$ {IEEE} Symposium on Real-time and Embedded Technology and Applications},
   pages = {80--89},
   year = {2008}
@@ -45 +45 @@
   author = {Robert Atkey},
   title = {{CoqJVM}: An executable specification of the Java virtual machine using dependent types},
-  booktitle = {Proceedings of the Conference of the {TYPES} Project {(TYPES 2007)}},
+  booktitle = {Proceedings of the Conference of the {TYPES} Project},
   pages = {18--32},
-  series = {Lecture Noted in Computer Science},
-  volume = {4941},
   year = {2007}
 }
@@ -56 +54 @@
   author = {Sandrine Blazy and Zaynah Dargaye and Xavier Leroy},
   title = {Formal Verification of a {C} Compiler Front-End},
-  booktitle = {Proceedings of the International Symposium on Formal Methods ({FM 2006})},
-  series = {Lecture Notes in Computer Science},
-  volume = {4085},
+  booktitle = {Proceedings of the International Symposium on Formal Methods},
   pages = {460--475},
   year = {2006}
@@ -67 +63 @@
   author = {Adam Chlipala},
   title = {A verified compiler for an impure functional language},
-  booktitle = {Proceedings of the Thirty Seventh Annual Symposium on Principles of Programming Languages {(POPL 2010)}},
-  series = {{ACM SIGPLAN} Notices},
-  volume = {45},
-  issue = {1},
+  booktitle = {Proceedings of the $\mathrm{37^{th}}$ Annual Symposium on Principles of Programming Languages},
   pages = {93--106},
   year = {2010}
@@ -79 +72 @@
   author = {Anthony Fox and Magnus O. Myreen},
   title = {A Trustworthy Monadic Formalization of the {ARMv7} Instruction Set Architecture},
-  booktitle = {Proceedings of the First International Conference on Interactive Theorem Proving ({ITP 2010})},
-  series = {Lecture Notes in Computer Science},
+  booktitle = {Proceedings of the $\mathrm{1^{st}}$ International Conference on Interactive Theorem Proving},
   pages = {243--258},
   year = {2010}
@@ -97 +89 @@
   author = {Daan Leijen and Erik Meijer},
   title = {Domain specific embedded compilers},
-  booktitle = {Proceedings of the Second Conference on Domain Specific Languages {(DSL 1999)}},
-  series = {{ACM SIGPLAN} Notices},
+  booktitle = {Proceedings of the $\mathrm{2^{nd}}$ Conference on Domain Specific Languages},
   pages = {109--122},
-  volume = {2},
   year = {1999}
 }
@@ -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},
   title = {The semantics of {x86-CC} multiprocessor machine code},
-  booktitle = {Proceedings of the Thirty Sixth Annual Symposium on Principles of Programming Languages {(POPL 2009)}},
-  series = {{ACM SIGPLAN} Notices},
+  booktitle = {Proceedings of the $\mathrm{36^{th}}$ Annual Symposium on Principles of Programming Languages},
   pages = {379--391},
-  volume = {44},
-  issue = {1},
   year = {2009}
+}
+
+@inproceedings
+{ shankar:principles:1999,
+  author = {Natarajan Shankar and Sam Owre},
+  title = {Principles and Pragmatics of Subtyping in {PVS}},
+  booktitle = {Recent Trends in Algebraic Development Techniques},
+  pages = {37--52},
+  year = {1999}
+}
+
+@inproceedings
+{ sozeau:subset:2006,
+  author = {Matthieu Sozeau},
+  title = {Subset coercions in {Coq}},
+  booktitle = {Proceedings of the Conference of the {TYPES} Project},
+  pages = {237--252},
+  year = {2006}
 }
 

Deliverables/D4.1/ITP-Paper/itp-2011.tex

@@ -78 +78 @@
 Both the O'Caml and Matita emulators are `executable'.
 Assembly programs may be animated within Matita, producing a trace of instructions executed.
-
-Our formalisation is a major component of the ongoing EU-funded CerCo project.
+The formalisation is a major component of the ongoing EU-funded CerCo project.
 \end{abstract}
 
@@ -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.
 
-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.
+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 is what we describe in this paper.
 The focus of the formalisation has been on capturing the intensional behaviour of the processor.
@@ -146 +145 @@
 \label{subsect.8051-8052}
 
-The MCS-51 is an eight bit microprocessor introduced by Intel in the late 1970s.
+The MCS-51 is an 8-bit microprocessor introduced by Intel in the late 1970s.
 Commonly called the 8051, in the three decades since its introduction the processor has become a highly popular target for embedded systems engineers.
 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 @@
 
 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.
-XRAM is accessed using a dedicated instruction, and requires sixteen bits to address fully.
+XRAM is accessed using a dedicated instruction, and requires 16 bits to address fully.
 External code memory (XCODE) is often stored in the form of an EPROM, and limited to 64 kilobytes in size.
 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.
 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.
-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.
-
-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.
-Further, the processor possesses two eight bit general purpose accumulators, A and B.
+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.
+
+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.
+Two 8-bit general purpose accumulators, A and B, are provided.
 
 Communication with the device is facilitated by an onboard UART serial port, and associated serial controller, which can operate in numerous modes.
-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.
-(The 8052 provides an additional sixteen bit timer.)
+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.
+(The 8052 provides an additional 16-bit timer.)
 As an additional method of communication, the 8051 also provides a four byte bit-addressable input-output port.
 
@@ -303 +302 @@
 We began with an emulator written in O'Caml to `iron out' any bugs in our design and implementation.
 O'Caml's ability to perform file I/O also eased debugging and validation.
-Once we were happy with the performance and design of the O'Caml emulator, we moved to the Matita formalisation.
+Once we were happy with the design of the O'Caml emulator, we moved Matita.
 
 Matita's syntax is lexically similar to O'Caml's.
@@ -342 +341 @@
 \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).
+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~\cite{leijen:domain:1999} implemented with polymorphic variants~\cite{garrigue:programming:1998}, as in Figure~\ref{fig.ocaml.implementation.bitvectors}.
@@ -483 +482 @@
 
 A peculiarity of the MCS-51 is the non-orthogonality of its instruction set.
-For instance, the \texttt{MOV} instruction, can be invoked using one of sixteen combinations of addressing modes out of 361.
+For instance, the \texttt{MOV} instruction, can be invoked using one of 16 combinations of addressing modes out of a possible 361.
 
 % Show example of pattern matching with polymorphic variants
@@ -564 +563 @@
 ...
 \end{lstlisting}
-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.
+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.
 
 % 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.
 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.
-These coercions were first introduced by PVS to implement subset types~\cite{pvs?}, and later in Coq as an addition~\cite{russell}.
+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}.
 In Matita all coercions can open proof obligations.
 
@@ -645 +644 @@
 
 The UART port can work in several modes, depending on the how the SFRs are set.
-In an asyncrhonous mode, the UART transmits eight bits at a time, using a ninth line for syncrhonization.
+In an asyncrhonous mode, the UART transmits 8 bits at a time, using a ninth line for syncrhonization.
 In a syncrhonous mode the ninth line is used to transmit an additional bit.