Compositional comp cert

Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

29 Scopus citations

Abstract

This paper reports on the development of Compositional Comp- Cert, the first verified separate compiler for C. Specifying and proving separate compilation for C is made challenging by the coincidence of: compiler optimizations, such as register spilling, that introduce compiler-managed (private) memory regions into function stack frames, and C's stack-allocated addressable local variables, which may leak portions of stack frames to other modules when their addresses are passed as arguments to external function calls. The CompCert compiler, as built/proved by Leroy et al. 2006-2014, has proofs of correctness for whole programs, but its simulation relations are too weak to specify or prove separately compiled modules. Our technical contributions that make Compositional CompCert possible include: language-independent linking, a new operational model of multilanguage linking that supports strong semantic contextual equivalences; and structured simulations, a refinement of Beringer et al.'s logical simulation relations that enables expressive module-local invariants on the state communicated between compilation units at runtime. All the results in the paper have been formalized in Coq and are available for download together with the Compositional CompCert compiler.

Original languageEnglish (US)
Title of host publicationPOPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
PublisherAssociation for Computing Machinery
Pages275-287
Number of pages13
ISBN (Electronic)9781450333009
DOIs
StatePublished - Jan 14 2015
Event42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015 - Mumbai, India
Duration: Jan 12 2015Jan 18 2015

Publication series

NameConference Record of the Annual ACM Symposium on Principles of Programming Languages
Volume2015-January
ISSN (Print)0730-8566

Other

Other42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015
CountryIndia
CityMumbai
Period1/12/151/18/15

All Science Journal Classification (ASJC) codes

  • Software

Keywords

  • Compcert
  • Compiler correctness

Fingerprint Dive into the research topics of 'Compositional comp cert'. Together they form a unique fingerprint.

  • Cite this

    Stewart, G., Beringer, L., Cuellar, S., & Appel, A. W. (2015). Compositional comp cert. In POPL 2015 - Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (pp. 275-287). (Conference Record of the Annual ACM Symposium on Principles of Programming Languages; Vol. 2015-January). Association for Computing Machinery. https://doi.org/10.1145/2676726.2676985