The design and implementation of a certifying compiler
| Autor: | Peter Lee, George C. Necula |
|---|---|
| Rok vydání: | 2004 |
| Předmět: |
Correctness
Intrinsic function Typed assembly language Computer science Optimizing compiler Dynamic compilation computer.software_genre Dead code elimination Compiler construction Manifest expression Type safety Compilation error Interprocedural optimization Proof-carrying code Memory safety Formal verification computer.programming_language Compiler correctness Assembly language Programming language Program transformation Inline expansion Program optimization Computer Graphics and Computer-Aided Design Functional compiler TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Single Compilation Unit Compiler computer Software Compile time |
| Zdroj: | PLDI |
| ISSN: | 1558-1160 0362-1340 |
| DOI: | 10.1145/989393.989454 |
| Popis: | This paper presents the design and implementation of a compiler that translates programs written in a type-safe subset of the C programming language into highly optimized DEC Alpha assembly language programs, and a certifier that automatically checks the type safety and memory safety of any assembly language program produced by the compiler. The result of the certifier is either a formal proof of type safety or a counterexample pointing to a potential violation of the type system by the target program. The ensemble of the compiler and the certifier is called a certifying compiler .Several advantages of certifying compilation over previous approaches can be claimed. The notion of a certifying compiler is significantly easier to employ than a formal compiler verification, in part because it is generally easier to verify the correctness of the result of a computation than to prove the correctness of the computation itself. Also, the approach can be applied even to highly optimizing compilers, as demonstrated by the fact that our compiler generates target code, for a range of realistic C programs, which is competitive with both the cc and gcc compilers with all optimizations enabled. The certifier also drastically improves the effectiveness of compiler testing because, for each test case, it statically signals compilation errors that might otherwise require many executions to detect. Finally, this approach is a practical way to produce the safety proofs for a Proof-Carrying Code system, and thus may be useful in a system for safe mobile code. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|