Changeset 1201

Timestamp:

Sep 9, 2011, 11:27:45 AM (8 years ago)

Author:

mulligan

Message:

more changes to reduce length

File:

• Deliverables/D4.1/ITP-Paper/itp-2011.tex (modified) (7 diffs)

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

@@ -97 +97 @@
 Specifications are therefore also given at a high level and correctness can be proved by reasoning on the program's source code.
 The code that is actually run is not the high level source code that we reason on, but low level code generated by the compiler.
-A few questions now arise:
-\begin{itemize*}
-\item
-What properties are preserved during compilation?
-\item
+
+Questions now arise:  What properties are preserved during compilation?
 What properties are affected by the compilation strategy?
-\item
 To what extent can you trust your compiler in preserving those properties?
-\end{itemize*}
 These and other questions motivate a current `hot topic' in computer science research: \emph{compiler verification} (e.g.~\cite{chlipala:verified:2010,leroy:formal:2009}, and so on).
 So far, the field has only been focused on the first and last questions.
@@ -267 +262 @@
 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 extra 128 bytes of IRAM of the 8052 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.
+For instance, the extra 128 bytes of IRAM of the 8052 cannot be addressed using indirect addressing; rather, external (in)direct addressing must be used.
+Some memory segments are also 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.
@@ -658 +654 @@
 We leave the computation of the delay time to the environment.
 
-We use only the P1 and P3 lines despite the MCS-51 having~4 output lines, P0--P3.
-This is because P0 and P2 become inoperable if XRAM is present (we assume it is).
+We use only the P1 and P3 lines.
+This is because the other lines become inoperable if XRAM is present (we assume it is).
 
 The UART port can work in several modes, depending on the how the SFRs are set.
@@ -740 +736 @@
 We are interested in providing a precise specification of the behaviour of the microprocessor in order to prove the correctness of a compiler which will target the processor.
 In particular, we are interested in intentional properties of the processor; precise timings of instruction execution in clock cycles.
-Moreover, in addition to formalising the interface of an MCS-51 processor, we have also built a complete MCS-51 ecosystem: UART, I/O lines, and hardware timers, complete with an assembler.
+We have also built a complete MCS-51 ecosystem: UART, I/O lines, and hardware timers, complete with an assembler.
 
 Work closely related to our own can be found in~\cite{fox:trustworthy:2010}.
@@ -762 +758 @@
 In contrast, the various ARM instruction sets and memory models are relatively uniform.
 
-Two close projects to CerCo are CompCert~\cite{leroy:formally:2009} and the CLI Stack.
+Other related projects CompCert~\cite{leroy:formally:2009} and the CLI Stack.
 CompCert concerns the certification of a C compiler and includes a formalisation in Coq of a subset of PowerPC.
-The CLI Stack consists of the design and verification of a whole chain of artifacts including a 32-bit microprocessor, the Piton assembler and two compilers for high-level languages.
+The CLI Stack consists of the design and verification of a whole chain of artefacts including a 32-bit microprocessor, the Piton assembler and two compilers.
 Like CerCo, the CLI Stack compilers gave the cost of high-level instructions in processor cycles.
-However, unlike CerCo, both the CLI Stack high-level languages ($\mu$Gypsy and Nqthm Lisp) and FM9001 microprocessor were not commercial products, but designs created for the purpose of verification (see~\cite{moore:grand:2005}).
+The CLI Stack high-level languages ($\mu$Gypsy and Nqthm Lisp) and FM9001 microprocessor were not commercial products, but bespoke designs for the purpose of verification (see~\cite{moore:grand:2005}).
 
 The CompCert C compiler is extracted to O'Caml using Coq's code extraction facility.
@@ -781 +777 @@
 Our formalisation is \emph{directly} executable, while the one in CompCert only provides a relation that describes execution.
 In CompCert I/O is only described as a synchronous external function call and there is no I/O at the processor level.
-Moreover an idealized abstract and uniform memory model is assumed, while we take into account the complicated overlapping memory model of the MCS-51 architecture.
+CompCert assumes an idealized abstract and uniform memory model; we take into account the complicated overlapping memory model of the MCS-51 architecture.
 Finally, 82 instructions of the more than 200 offered by the processor are formalised in CompCert, and the assembly language is augmented with macro instructions that are turned into `real' instructions only during communication with the external assembler.
-Even from a technical level the two formalisations differ: we tried to exploit dependent types whilst CompCert largely sticks to a non-dependent fragment of Coq.
+Even from a technical level the two formalisations differ: we use dependent types whilst CompCert largely sticks to non-dependent types.
 
 In~\cite{atkey:coqjvm:2007} an executable specification of the Java Virtual Machine, using dependent types, is presented.
@@ -813 +809 @@
 
 The formalisation is done at machine level and not at assembly level; we also formalise fetching and decoding.
-We separately provide an assembly language, enhanched with labels and pseudoinstructions, and an assembler from this language to machine code.
+We provide an assembly language, enhanched with labels and pseudoinstructions, and an assembler from this language to machine code.
 This assembly language is similar to those found in `industrial strength' compilers, such as SDCC.
 We introduce cost labels in the machine language to relate the data flow of the assembly program to that of the C source language, in order to associate costs to the C program.