Committee

  • Andrew Appel (advisor)
  • Aarti Gupta
  • David Walker

Title

Inlining Compositional CompCert

Abstract

The first verified separate compiler for C, Compositional CompCert, was recently introduced with an operational model supporting language-independent linking and machine-checked proofs of vertical and horizontal composition, strengthening Leroy’s original CompCert proofs. The key techniques for its verification are structured simulations: logical relations between runtime states that enforce safety invariants in the presence of compiler-managed memory regions (private) and addressable portions of the stack frames that might be leaked to foreign modules through external function calls (public). However, the invariants are too strict to allow merging of stack frame as needed, for example, in function inlining optimizations. Moreover, changing the simulation is challenging since they strike a delicate balance that satisfies relies and guarantees among the compiled modules. In this work we present a refinement of the structured simulations that admits a larger number of compiler transformations (e.g. Function inlining) while maintaining compatibility with the operational model and the semantics preservation proof of the full compiler. The relaxation of the simulation works together with a strengthening of the proof for the composition of compiler phases (transitivity) by controlling module-ownership of memory, thus ensuring that stack frames from different compilations units are not merged together. The entire development has been written and verified in the proof assistant Coq.

Reading List

Papers

  1. [A. W. Appel] VeriSmall: Verified Smallfoot Shape Analysis. In First International Conf. on Certified Programs and Proofs Dec. 2011
  2. [L. Beringer, G. Stewart, and A. W. Appel] Verified compilation for shared-memory C. In Esop’ 14: The 23rd European Symposium on Programming, 2014.
  3. [Leroy 2009] X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52(7):107–115, 2009. (link)
  4. [James T. Perconti and Amal Ahmed] Verifying an Open Compiler Using Multi-Language Semantics. Programming Languages and Systems 2014 (link)
  5. [Reynolds 2002] J.C. Reynolds. Separation Logic: a Logic for Shared Mutable Data Structures. In LICS’02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55 - 74, 2002. (link)
  6. [Lerner 2003] S. Lerner, T. Millstein, and C. Chambers. Automatically Proving the Correctness of Compiler Optimizations. In PLDI’03: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2003.
  7. [Leroy and Blazy 2008] X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. J. Automated Reasoning, 41(1):1–31, 2008.
  8. [G. Morrisett and D. Walker] From System F to Typed Assembly Language (link)

Textbooks

  1. A. W. Appel. Modern Compiler Implementation in ML. Cambridge University Press, 1998
    • Part I. Fundamentals of Compilation
      • 13. Garbage Collection
      • 15. Functional Programming Languages
      • 17. Dataflow Analysis
      • 19. Static Single-Assignment Form
  2. B. Pierce. Types and Programming Languages. 2002.
    • Part I. Untyped Systems
    • Part II. Simple Types
    • Part IV. Recursive Types
    • Part V. Polymorphism
      • 23. Type Reconstruction
      • 24. Universal Types
      • 25. Existential Types
      • 26. An ML Implementation of System F