Changeset 564 for Deliverables

Timestamp:

Feb 17, 2011, 5:36:07 PM (10 years ago)

Author:

sacerdot

Message:

Tentative conclusions.

File:

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

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

@@ -759 +759 @@
 
 Despite this similarity, the two formalisations do not have much in common.
-First, CompCert provides a formalisation at the assembly level (no instruction decoding), and this impels them to trust an unformalised assembler and linker, whereas we provide our own.
+First, CompCert provides a formalisation at the assembly level (no instruction decoding), and this impels them to trust an unformalised assembler and linker, whereas we provide our own. Our formalization is directly executable, while the
+one in CompCert only provides a relation that describes execution.
 I/O is also not considered at all in CompCert.
 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.
-Finally, around 90 instructions of the 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.
+Finally, 82 instructions of the 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: while we tried to exploit dependent types as often as possible, CompCert largely sticks to the non-dependent fragment of Coq.
 
@@ -788 +789 @@
 \label{sect.conclusions}
 
-\CSC{Tell what is NOT formalized/formalizable: the HEX parser/pretty printer
- and/or the I/O procedure}
-\CSC{Decode: two implementations}
-\CSC{Discuss over-specification}
-
-- WE FORMALIZE ALSO I/O ETC. NOT ONLY THE INSTRUCTION SELECTION (??)
-  How to test it? Specify it?
+In the EU project CerCo (`Certified Complexity') we are interested in the
+certification of a compiler for C that induces a precise cost model on the
+source code. The cost model assigns costs to blocks of instructions by tracing
+the way blocks are compiled and by computing the exact costs on the generated
+assembly code. In order to perform this accurately, we have provided an
+executable semantics for the MCS-51 family of processors, better known as
+8051/8052. The formalization was done twice, first in O'Caml and then in Matita,
+and also captures the exact timings of the processor. Moreover, the O'Caml one
+also considers timers and I/O. Adding support for I/O and timers in Matita is
+an on-going work that will not present any major problem. It was delayed only
+because not immediately useful for the formalization of the CerCo compiler.
+
+The formalization is done at machine level and not at assembly level:
+we also formalize fetching and decoding. However, we separately provide also
+an assembly language, enhanched with labels and pseudo-instructions, and
+an assembler from this language to machine code. We also 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.
+Finally, for the O'Caml version, we provide a parser and pretty printer from
+the memory representation to the Intel HEX format. Hence we can easily perform
+testing on programs compiled using any free or commercial compiler.
+
+Compared with previous formalizations of micro-processors, the main difficulties
+in formalizing the MCS-51 are due to the unorthogonality of its memory model
+and instruction set. These are easily handled in O'Caml by using advanced
+language features like polymorphic variants and phantom types to simulate
+Generalized Abstract Data Types. In Matita, we use dependent types to recover
+the same flexibility, to reduce spurious partiality and to grant invariants
+that will be useful in the formalization of the CerCo compiler.
+
+The formalization has been partially verified by computing execution traces on
+selected programs and comparing them with an exhisting emulator. All
+instructions have been tested at least once, but we have not yet pushed testing
+further, for example with random testing or by means of development boards.
+I/O in particular has not been tested yet, and it is currently unclear how
+to provide exhaustive testing in presence of I/O. Finally, we are aware of
+having over-specified the processor in several places, by fixing a behaviour
+hopefully consistent with the real machine where the data sheets of the
+vendors do not specify one.
 
 \bibliography{itp-2011.bib}