The Design and Implementation of a Certifying Compiler George C. Necula Peter Lee School of Computer Science Carnegie Mellon University Pittsburgh, Pennsylvania 15213-3891 {necula,petel}@cs.cmu.ecJu Abstract This paper presents the design and implementation of a com- piler 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 au- tomatically 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 certi,fying compiler. Several advantages of certifying compilation over previ- ous approaches can be claimed. The notion of a certify- ing 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 compil- ers, 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 gee compilers with all op- timizations enabled. The certifier also drastically improves the effectiveness of compiler testing because, for each test case, it statically signals compilation errors that might oth- erwise require many executions to detect. Finally, this ap- proach 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. 1 Introduction The question of compiler correctness is as old as the first compiler implementations. In a paper published in 1963, This research was sponsored in part by the Advanced Research Projects Agency CSTO under the title “The Fox Project: Advanced Languages for Systems Software,” ARPA Order No. C533, issued by ESC/ENS under Contract No. F19628-95-C-0050. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the Advanced Research Projects Agency or the U.S. Government. 0 1998 ACM 0.89791-987-4198/0008...S6.00 John McCarthy refers to this problem as “one of the most interesting and useful goals for the mathematical science of computation” (McCarthy 1963). However, despite a large body of work in the area (Dybjer 1986; Guttman, Ramsdell, and Wand 1995; Moore 1989; Morris 1973; Oliva, Ramsdell, and Wand 1995; Thatcher, Wagner, and Wright 1980; Young 1989), we still lack the technology to prove automatically the correctness of an optimizing compiler. Even manual proofs are rare, and they tend to verify only the algorithms rather than the implementations. Plus, the correctness proofs need to be redone after even the slightest modification or improve- ment to the compiler. Proving compiler correctness is just a means towards the actual goal of ensuring that only correct output is ever pro- duced by the compiler. In this paper we propose a poten- tially more practical approach to the same goal. Instead of verifying the compiler once and for all, we check aspects of the correctness of every individual compilation. This will not ensure that the compiler is bug-free, but it will signal most incorrect compiler outputs as soon as they are pro- duced. To reduce the complexity of the checking process, we do not try to check full equivalence of the source and target programs, but instead we verify only that the target program has certain key properties that can be verified using a small amount of information about the source program. We present in this paper the design and implementa- tion of Touchstone, an optimizing compiler that translates a strongly typed programming language (essentially a type- safe subset of C) into DEC Alpha assembly language, and a certifier that checks the type safety of any assembly lan- guage program produced by the compiler. The result of the certifier is either a formal proof of type safety or a counterex- ample pointing to a potential violation of the type system by the assembly-language target program. We refer to the ensemble of the compiler and the certifier as a certifying compiler. Our approach provides several advantages: l This method is significantly easier to employ than a formal verification of the compiler, even if the formal verification is restricted to proving that only type-safe code is emitted. This is because it is easier in general to verify the correctness of the result of a computation than to prove the correctness of the computation it- self. Furthermore, with this approach, most compiler revisions and improvements do not require any change to the certifier. l This method can be applied to optimizing compilers, because the design of the certifier does not restrict the 333Type Specification Annotated Code ProofKounterexample Figure 1: Overview of the Touchstone certifying compiler. optimizations that the compiler is allowed to perform. Our optimizing compiler generates code that, for many programs, matches or is within 15% of the performance of both gee and cc with all optimizations enabled, the difference being due mostly to several optimizations that we have not yet implemented. Also, we have suc- cessfully tested the certifier on hand-optimized sssem- bly language. l The presence of the certifier drastically improves the effectiveness of compiler testing because, for each test case, it statically signals
View Full Document
Unlocking...