TY - JOUR
T1 - Compositional CompCert
AU - Stewart, Gordon
AU - Beringer, Lennart
AU - Cuellar, Santiago
AU - Appel, Andrew W.
PY - 2015/1
Y1 - 2015/1
N2 - 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.
AB - 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.
KW - CompCert
KW - Compiler correctness
UR - http://www.scopus.com/inward/record.url?scp=84950321922&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84950321922&partnerID=8YFLogxK
U2 - 10.1145/2676726.2676985
DO - 10.1145/2676726.2676985
M3 - Article
AN - SCOPUS:84950321922
VL - 50
SP - 275
EP - 287
JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
SN - 1523-2867
IS - 1
ER -