Compositional CompCert

8 years 4 days ago
Compositional CompCert
This paper reports on the development of Compositional CompCert, 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...
Gordon Stewart, Lennart Beringer, Santiago Cuellar
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where POPL
Authors Gordon Stewart, Lennart Beringer, Santiago Cuellar, Andrew W. Appel
Comments (0)