Verified Separate Compilation for C

Abstract:

A separate compiler independently translates a program’s components
in a way that preserves correctness of the program as a whole.
This dissertation develops techniques and tools for verified (mechanically
proved) separate compilation of programs in 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–
2015 and upon which this dissertation builds, has proofs of correctness
for whole programs, but its simulation relations are too weak to
specify or prove separately compiled modules.
The main contributions of the dissertation are:
(i) language-independent linking, a new operational model of multilanguage
module interaction that supports the statement and proof
of cross-language contextual equivalence;
(ii) structured simulations, a program-equivalence proof method
that enables expressive module-local invariants on the state communicated
between compilation units at runtime;
(iii) the application of the above techniques to Compositional Comp-
Cert, a verified separate compiler for C. As additional validation, the
dissertation demonstrates the connection of Compositional CompCert
to the Verifiable C program logic.