Verified Compilation for Shared-memory C

Abstract. We present a new architecture for specifying and proving op-timizing compilers in the presence of shared-memory interactions such as buffer-based system calls, shared-memory concurrency, and separate compilation. The architecture, which is implemented in the context of CompCert, includes a novel interaction-oriented model for C-like lan-guages, and a new proof technique, called logical simulation relations, for compositionally proving compiler correctness with respect to this inter-action model. We apply our techniques to CompCert’s primary memory-reorganizing compilation phase, Cminorgen. Our results are formalized in Coq, building on the recently released CompCert 2.0.