Changeset 564


Ignore:
Timestamp:
Feb 17, 2011, 5:36:07 PM (6 years ago)
Author:
sacerdot
Message:

Tentative conclusions.

File:
1 edited

Legend:

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

    r563 r564  
    759759
    760760Despite this similarity, the two formalisations do not have much in common.
    761 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.
     761First, 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
     762one in CompCert only provides a relation that describes execution.
    762763I/O is also not considered at all in CompCert.
    763764Moreover an idealized abstract and uniform memory model is assumed, while we take into account the complicated overlapping memory model of the MCS-51 architecture.
    764 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.
     765Finally, 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.
    765766Even 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.
    766767
     
    788789\label{sect.conclusions}
    789790
    790 \CSC{Tell what is NOT formalized/formalizable: the HEX parser/pretty printer
    791  and/or the I/O procedure}
    792 \CSC{Decode: two implementations}
    793 \CSC{Discuss over-specification}
    794 
    795 - WE FORMALIZE ALSO I/O ETC. NOT ONLY THE INSTRUCTION SELECTION (??)
    796   How to test it? Specify it?
     791In the EU project CerCo (`Certified Complexity') we are interested in the
     792certification of a compiler for C that induces a precise cost model on the
     793source code. The cost model assigns costs to blocks of instructions by tracing
     794the way blocks are compiled and by computing the exact costs on the generated
     795assembly code. In order to perform this accurately, we have provided an
     796executable semantics for the MCS-51 family of processors, better known as
     7978051/8052. The formalization was done twice, first in O'Caml and then in Matita,
     798and also captures the exact timings of the processor. Moreover, the O'Caml one
     799also considers timers and I/O. Adding support for I/O and timers in Matita is
     800an on-going work that will not present any major problem. It was delayed only
     801because not immediately useful for the formalization of the CerCo compiler.
     802
     803The formalization is done at machine level and not at assembly level:
     804we also formalize fetching and decoding. However, we separately provide also
     805an assembly language, enhanched with labels and pseudo-instructions, and
     806an assembler from this language to machine code. We also introduce cost labels
     807in the machine language to relate the data flow of the assembly program to that
     808of the C source language, in order to associate costs to the C program.
     809Finally, for the O'Caml version, we provide a parser and pretty printer from
     810the memory representation to the Intel HEX format. Hence we can easily perform
     811testing on programs compiled using any free or commercial compiler.
     812
     813Compared with previous formalizations of micro-processors, the main difficulties
     814in formalizing the MCS-51 are due to the unorthogonality of its memory model
     815and instruction set. These are easily handled in O'Caml by using advanced
     816language features like polymorphic variants and phantom types to simulate
     817Generalized Abstract Data Types. In Matita, we use dependent types to recover
     818the same flexibility, to reduce spurious partiality and to grant invariants
     819that will be useful in the formalization of the CerCo compiler.
     820
     821The formalization has been partially verified by computing execution traces on
     822selected programs and comparing them with an exhisting emulator. All
     823instructions have been tested at least once, but we have not yet pushed testing
     824further, for example with random testing or by means of development boards.
     825I/O in particular has not been tested yet, and it is currently unclear how
     826to provide exhaustive testing in presence of I/O. Finally, we are aware of
     827having over-specified the processor in several places, by fixing a behaviour
     828hopefully consistent with the real machine where the data sheets of the
     829vendors do not specify one.
    797830
    798831\bibliography{itp-2011.bib}
Note: See TracChangeset for help on using the changeset viewer.