Credible Compilers

This paper presents a new concept in compiler correctness: instead of proving that the compiler performs all of its transformations correctly, the compiler generates a proof that the transformed program correctly implements the input program. A simple proof checker can then verify that the program was compiled correctly. We call a compiler that produces such proofs a {\em credible compiler}, because it produces verifiable evidence that it is operating correctly. Compiler optimizations usually consist of two steps --- an analysis step determines if it is legal to apply the optimization, and a transformation step applies the optimization to generate a transformed program that computes the same result as the original program. Our approach supports this two-step structure. It provides a logic that the compiler can use to prove that its program analysis results are correct, and a logic that the compiler can use to prove that the transformed program correctly simulates the original program. These logics are defined for a standard program representation, control flow graphs. This report defines these logics and proves that they are sound with respect to a standard operational semantics. It also presents detailed examples that demonstrate how a compiler can use the logics to prove the correctness of several standard optimizations. We believe that credible compilation has the potential to revolutionize the way compilers are built and used. Specifically, they will allow programmers to quickly determine if the compiler compiled their program correctly, help developers find and eliminate bugs in compiler passes, allow large groups of mutually untrusting people to collaborate productively on the same compiler, increase the speed with which compilers are developed and released, and make it possible to aggressively upgrade large, stable compiler systems without fear of inadvertantly introducing undetected errors.