Verified Compilation for Shared-memory C
Lennart Beringer,
Gordon Stewart,
Robert Dockins, and
Andrew W. Appel
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
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.
Files
Online version of Appendix A: Proofs in Coq