 Timestamp:
 Jun 21, 2011, 3:04:05 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r1031 r1032 585 585 If CompCert chooses to assume the existence of an optimising assembler, then care should be made to ensure that any assembly program produced by the CompCert compiler falls into the subset of programs that have a hope of having their semantics preserved by an optimising assembler. 586 586 587 In certain places in our formalisation (e.g. in proving \texttt{build\_maps} is correct) we made use of Matita's implementation of Russell~\cite{sozeau:subset:2006}. 588 In Matita, Russell may be implemented using two coercions and some notational sugaring. 589 % more 587 Our formalization exploits dependent types in different ways and for multiple 588 purposes. The first purpose is to reduce potential errors in the formalization 589 of the microprocessor. In particular, 590 dependent types are used to constraint the size of bitvectors and 591 tries that represent memory quantities and memory areas respectively. 592 They are also used as explained in~\cite{mulligan:executable:2011}. 593 to simulate polymorphic variants in Matita. Polymorphic variants nicely 594 capture the absolutely unorthogonal instruction set of the MCS51 where every 595 opcode must accept its own subset of the 11 addressing mode of the processor. 596 597 The second purpose is to single out the sources of incompleteness. By 598 abstracting our functions over the dependent type of correct policies, we were 599 able to manifest the fact that the compiler never refuses to compile a program 600 where a correct policy exists. This also allowed to simplify the 601 initial proof by dropping lemmas establishing that one function fails if and 602 only if some other one does so. 603 604 Finally, dependent types, together with Matita's liberal system of coercions, 605 allow to simulate almost entirely in user space the proof methodology 606 ``Russell'' of Sozeau~\cite{sozeau:subset:2006}. However, not every 607 proof has been done this way: we only used this style to prove that a 608 function satisfies a specification that only involves that function in a 609 significant way. For example, it would be innatural to see the proof that 610 fetch and assembly commute as the specification of one of the two functions. 590 611 591 612 \subsection{Related work} … … 618 639 \label{subsect.resources} 619 640 620 All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}. 621 Our development, including the definition of the executable semantics of the MCS51, is spread across 17 files, totalling around 13,000 lines of Matita source. 622 The bulk of the proof described herein is contained in a single file, \texttt{AssemblyProof.ma}, consisting of approximately 3000 lines of Matita source. 623 624 We admit to using a number of axioms in our development. 625 We do not believe the use of these axioms has been particularly onerousvery few concern anything more interesting than, say, stating that converting from a natural number to a bitvector and back again is the identityand what axioms remain are rapidly being closed as work continues. 641 All files relating to our formalisation effort can be found online at~\url{http://cerco.cs.unibo.it}. The code of the compiler has been completed, and the 642 proof of correctness described here is still in progress. In particular, we 643 have assumed several properties of ``library functions'' related in particular 644 to modular arithmetics and datastructures manipulation. Moreover, we only 645 completed the interesting cases of some of the main theorems that proceed by 646 cases on all the possible opcodes. 647 We thus believe that the proof strategy is sound and that we will be able to 648 close soon all axioms, up to possible minor bugs that should have local fixes 649 that do not affect the global proof strategy. 650 651 The development, including the definition of the executable semantics of the MCS51, is spread across 17 files, totalling around 11,500 lines of Matita source. 652 The bulk of the proof described herein is contained in a single file, \texttt{AssemblyProof.ma}, consisting at the moment of approximately 2500 lines of Matita source. Another 1000 lines of proofs are spread all over the development because 653 of dependent types and the Russell proof style, that do not allow to separate the code from the proofs. The low ratio between the number of lines of code and 654 the number of lines of proof is unusual. It is justified by the fact that 655 the pseudoassembly and the assembly language share most constructs and that 656 large parts of the semantics is also shared. Thus many lines of code are 657 required to describe the complex semantics of the processor, but, for 658 the shared cases, the proof of preservation of the semantics is essentially 659 trivial. 626 660 627 661 \bibliography{cpp2011.bib}
Note: See TracChangeset
for help on using the changeset viewer.