Verified Compilation for Shared-memory C

Lennart Beringer, Gordon Stewart, Robert Dockins, and Andrew W. Appel


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 languages, and a new proof technique, called logical simulation relations, for compositionally proving compiler correctness with respect to this interaction model. We apply our techniques to CompCert’s primary memory-reorganizing compilation phase, Cminorgen. Our results are formalized in Coq, based on the recently released CompCert 2.0.


Online version of Appendix A: Proofs in Coq

Figure 3 core_semantics.v CoreSemantics
Definition 1 forward_simulations.v Forward_simulation_*
Theorem 1 forward_simulations_trans.v coop_sim_trans
Figure 6 mem_interpolation_*.v (e.g., mem_interpolation_II.v ) interpolation_*
Definition 2 safety_preservation.v safeN
Theorem 2 safety_preservation.v safety_preservation
Adaptation of Cminorgenproof CminorgenproofSIM.v transl_program_correct