Changeset 564 for Deliverables
- Timestamp:
- Feb 17, 2011, 5:36:07 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.1/ITP-Paper/itp-2011.tex
r563 r564 759 759 760 760 Despite 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. 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. Our formalization is directly executable, while the 762 one in CompCert only provides a relation that describes execution. 762 763 I/O is also not considered at all in CompCert. 763 764 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. 764 Finally, around 90instructions 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.765 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. 765 766 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. 766 767 … … 788 789 \label{sect.conclusions} 789 790 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? 791 In the EU project CerCo (`Certified Complexity') we are interested in the 792 certification of a compiler for C that induces a precise cost model on the 793 source code. The cost model assigns costs to blocks of instructions by tracing 794 the way blocks are compiled and by computing the exact costs on the generated 795 assembly code. In order to perform this accurately, we have provided an 796 executable semantics for the MCS-51 family of processors, better known as 797 8051/8052. The formalization was done twice, first in O'Caml and then in Matita, 798 and also captures the exact timings of the processor. Moreover, the O'Caml one 799 also considers timers and I/O. Adding support for I/O and timers in Matita is 800 an on-going work that will not present any major problem. It was delayed only 801 because not immediately useful for the formalization of the CerCo compiler. 802 803 The formalization is done at machine level and not at assembly level: 804 we also formalize fetching and decoding. However, we separately provide also 805 an assembly language, enhanched with labels and pseudo-instructions, and 806 an assembler from this language to machine code. We also introduce cost labels 807 in the machine language to relate the data flow of the assembly program to that 808 of the C source language, in order to associate costs to the C program. 809 Finally, for the O'Caml version, we provide a parser and pretty printer from 810 the memory representation to the Intel HEX format. Hence we can easily perform 811 testing on programs compiled using any free or commercial compiler. 812 813 Compared with previous formalizations of micro-processors, the main difficulties 814 in formalizing the MCS-51 are due to the unorthogonality of its memory model 815 and instruction set. These are easily handled in O'Caml by using advanced 816 language features like polymorphic variants and phantom types to simulate 817 Generalized Abstract Data Types. In Matita, we use dependent types to recover 818 the same flexibility, to reduce spurious partiality and to grant invariants 819 that will be useful in the formalization of the CerCo compiler. 820 821 The formalization has been partially verified by computing execution traces on 822 selected programs and comparing them with an exhisting emulator. All 823 instructions have been tested at least once, but we have not yet pushed testing 824 further, for example with random testing or by means of development boards. 825 I/O in particular has not been tested yet, and it is currently unclear how 826 to provide exhaustive testing in presence of I/O. Finally, we are aware of 827 having over-specified the processor in several places, by fixing a behaviour 828 hopefully consistent with the real machine where the data sheets of the 829 vendors do not specify one. 797 830 798 831 \bibliography{itp-2011.bib}
Note: See TracChangeset
for help on using the changeset viewer.