Changes between Version 11 and Version 12 of Proposal1.2


Ignore:
Timestamp:
Jun 15, 2010, 6:22:24 PM (7 years ago)
Author:
sacerdot
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Proposal1.2

    v11 v12  
    11== [[BR]] Progress beyond state of the art ==
    22
    3 Automatic verification of properties of software components has reached a level of maturity allowing complete correctness proofs of entire compilers; that is of the semantic equivalence between the generated assembly code and its source program. For instance, in the framework of the http://www.info.uni-karlsruhe.de/publications.php/id=213Verifix Project a compiler from a subset of Common Lisp to Transputer code was formally checked in PVS (see [[[node60.html#Dold|Dold and Vialard]]]). [[[node60.html#Strecker|Strecker]]] and [[[node60.html#Klein|Klein and Nipkow]]] certified bytecode compilers from a subset of Java to a subset of the Java Virtual Machine in Isabelle. In the same system, [[[node60.html#Leinenbach|Leinenbach et al.]]] formally verified a compiler from a subset of C to a DLX assembly code. [[[node60.html#Chlipala|Chlipala]]] recently wrote in Coq a certified compiler from the simply-typed lambda calculus to assembly language, making an extensive use of dependent types. Perhaps, the most advanced project is http://pauillac.inria.fr/�xleroy/compcert/Compcert, headed by Leroy, based on the use of Coq both for programming the compiler and proving its correctness. In particular, both the back-end ([[[node60.html#Leroy06|Leroy]]]) and the front-end ([[[node60.html#Leroy08|Leroy and Tristan]]]) of an optimising compiler from a subset of C to PowerPC assembly have been certified in this way.
     3Automatic verification of properties of software components has reached a level of maturity allowing complete correctness proofs of entire compilers; that is of the semantic equivalence between the generated assembly code and its source program. For instance, in the framework of the http://www.info.uni-karlsruhe.de/publications.php/id=213Verifix Project a compiler from a subset of Common Lisp to Transputer code was formally checked in PVS (see [wiki:Proposal4#Dold Dold and Vialard]). [[[node60.html#Strecker|Strecker]]] and [[[node60.html#Klein|Klein and Nipkow]]] certified bytecode compilers from a subset of Java to a subset of the Java Virtual Machine in Isabelle. In the same system, [[[node60.html#Leinenbach|Leinenbach et al.]]] formally verified a compiler from a subset of C to a DLX assembly code. [[[node60.html#Chlipala|Chlipala]]] recently wrote in Coq a certified compiler from the simply-typed lambda calculus to assembly language, making an extensive use of dependent types. Perhaps, the most advanced project is http://pauillac.inria.fr/�xleroy/compcert/Compcert, headed by Leroy, based on the use of Coq both for programming the compiler and proving its correctness. In particular, both the back-end ([[[node60.html#Leroy06|Leroy]]]) and the front-end ([[[node60.html#Leroy08|Leroy and Tristan]]]) of an optimising compiler from a subset of C to PowerPC assembly have been certified in this way.
    44
    55However, very little is known about the preservation of intensional properties of programs, and in particular about their (concrete) complexity. The theoretical study of the complexity impact of program transformations between different computational models has so far been confined to very foundational devices. Here we propose to address a concrete case of compilation from a typical high-level language to assembly. It is worth remarking that it is unlikely to have constant-time transformations between foundational models: for instance coding a multitape Turing machine into a single tape one could introduce a polynomial slow-down. Thus, complexity is architecture dependent, and the claim that you may pass from one language to another, preserving the performance of your algorithms, must be taken with the due caution. In particular, as surprising as it may be, very little is known about the complexity behaviour of a compiled code with respect to its source; as a matter of fact, most industries producing robots or devices with strong temporal constraints (such as, e.g. photoelectric safety barriers) still program such devices in assembly.