Changeset 1032


Ignore:
Timestamp:
Jun 21, 2011, 3:04:05 PM (8 years ago)
Author:
sacerdot
Message:

Final version.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1031 r1032  
    585585If 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.
    586586
    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
     587Our formalization exploits dependent types in different ways and for multiple
     588purposes. The first purpose is to reduce potential errors in the formalization
     589of the microprocessor. In particular,
     590dependent types are used to constraint the size of bit-vectors and
     591tries that represent memory quantities and memory areas respectively.
     592They are also used as explained in~\cite{mulligan:executable:2011}.
     593to simulate polymorphic variants in Matita. Polymorphic variants nicely
     594capture the absolutely unorthogonal instruction set of the MCS-51 where every
     595opcode must accept its own subset of the 11 addressing mode of the processor.
     596
     597The second purpose is to single out the sources of incompleteness. By
     598abstracting our functions over the dependent type of correct policies, we were
     599able to manifest the fact that the compiler never refuses to compile a program
     600where a correct policy exists. This also allowed to simplify the
     601initial proof by dropping lemmas establishing that one function fails if and
     602only if some other one does so.
     603
     604Finally, dependent types, together with Matita's liberal system of coercions,
     605allow to simulate almost entirely in user space the proof methodology
     606``Russell'' of Sozeau~\cite{sozeau:subset:2006}. However, not every
     607proof has been done this way: we only used this style to prove that a
     608function satisfies a specification that only involves that function in a
     609significant way. For example, it would be innatural to see the proof that
     610fetch and assembly commute as the specification of one of the two functions.
    590611
    591612\subsection{Related work}
     
    618639\label{subsect.resources}
    619640
    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 MCS-51, 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 onerous---very few concern anything more interesting than, say, stating that converting from a natural number to a bitvector and back again is the identity---and what axioms remain are rapidly being closed as work continues.
     641All 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
     642proof of correctness described here is still in progress. In particular, we
     643have assumed several properties of ``library functions'' related in particular
     644to modular arithmetics and datastructures manipulation. Moreover, we only
     645completed the interesting cases of some of the main theorems that proceed by
     646cases on all the possible opcodes.
     647We thus believe that the proof strategy is sound and that we will be able to
     648close soon all axioms, up to possible minor bugs that should have local fixes
     649that do not affect the global proof strategy.
     650
     651The development, including the definition of the executable semantics of the MCS-51, is spread across 17 files, totalling around 11,500 lines of Matita source.
     652The 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
     653of 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
     654the number of lines of proof is unusual. It is justified by the fact that
     655the pseudo-assembly and the assembly language share most constructs and that
     656large parts of the semantics is also shared. Thus many lines of code are
     657required to describe the complex semantics of the processor, but, for
     658the shared cases, the proof of preservation of the semantics is essentially
     659trivial.
    626660
    627661\bibliography{cpp-2011.bib}
Note: See TracChangeset for help on using the changeset viewer.