describes the structure of the CompCert compiler, its performance, and how the Coq proof assistant was used not
only to prove its correctness but also to program most of it.
By lack of space, we will not detail the formal verification of
every compilation pass. However, Section 4 provides a technical overview of such a verification for one crucial pass of
the compiler: register allocation. Finally, Section 5 presents
preliminary conclusions and directions for future work.
exists exactly one behavior B such that S ⇓ B, and similarly
for C. In this case, it is easy to prove that property ( 2) is equivalent to
∀B ∉Wrong, S ⇓ B ⇒ C ⇓ B
( 3)
2. APPRoAChes To TRus TeD CoMPiLATion
2. 1. notions of semantic preservation
Consider a source program S and a compiled program C
produced by a compiler. Our aim is to prove that the semantics of S was preserved during compilation. To make this
notion of semantic preservation precise, we assume given
semantics for the source and target languages that associate observable behaviors B to S and C. We write S ⇓ B
to mean that program S executes with observable behavior
B. The behaviors we observe in CompCert include termination, divergence, and “going wrong” (invoking an undefined
operation that could crash, such as accessing an array out
of bounds). In all cases, behaviors also include a trace of the
input–output operations (system calls) performed during
the execution of the program. Behaviors therefore reflect
accurately what the user of the program, or more generally
the outside world the program interacts with, can observe.
The strongest notion of semantic preservation during
compilation is that the source program S and the compiled
code C have exactly the same observable behaviors:
(Here, Wrong is the set of “going wrong” behaviors.) Property
( 3) is generally much easier to prove than property ( 2), since
the proof can proceed by induction on the execution of S.
This is the approach that we take in this work.
From a formal methods perspective, what we are really
interested in is whether the compiled code satisfies the functional specifications of the application. Assume that these
specifications are given as a predicate Spec(B) of the observable behavior. We say that C satisfies the specifications, and
write C Spec, if C cannot go wrong (C safe) and all behaviors of B satisfy Spec (∀B, C ⇓ B ⇒ Spec(B) ). The expected correctness property of the compiler is that it preserves the fact
that the source code S satisfies the specification, a fact that
has been established separately by formal verification of S:
S Spec ⇒ C Spec
( 4)
It is easy to show that property ( 2) implies property ( 4) for
all specifications Spec. Therefore, establishing property ( 2)
once and for all spares us from establishing property ( 4) for
every specification of interest.
A special case of property ( 4), of considerable historical
importance, is the preservation of type and memory safety,
which we can summarize as “if S does not go wrong, neither
does C”:
∀B, S⇓ B⇔C⇓ B
( 1)
S safe ⇒ C safe
( 5)
Notion ( 1) is too strong to be usable. If the source language is not deterministic, compilers are allowed to select
one of the possible behaviors of the source program. (For
instance, C compilers choose one particular evaluation
order for expressions among the several orders allowed by
the C specifications.) In this case, C will have fewer behaviors than S. Additionally, compiler optimizations can optimize away “going wrong” behaviors. For example, if S can go
wrong on an integer division by zero but the compiler eliminated this computation because its result is unused, C will
not go wrong. To account for these degrees of freedom in the
compiler, we relax definition ( 1) as follows:
Combined with a separate check that S is well-typed in a
sound type system, property ( 5) implies that C executes
without memory violations. Type-preserving compilation18 obtains this guarantee by different means: under the
assumption that S is well typed, C is proved to be well typed
in a sound type system, ensuring that it cannot go wrong.
Having proved properties ( 2) or ( 3) provides the same guarantee without having to equip the target and intermediate
languages with sound type systems and to prove type preservation for the compiler.
S safe ⇒ (∀B, C ⇓ B ⇒ S ⇓ B)
( 2) 2. 2. Verified, validated, certifying compilers
We now discuss several approaches to establishing that a
compiler preserves semantics of the compiled programs,
in the sense of Section 2. 1. In the following, we write S ≈ C,
where S is a source program and C is compiled code, to
denote one of the semantic preservation properties ( 1) to ( 5)
of Section 2. 1.
Verified Compilers. We model the compiler as a total function Comp from source programs to either compiled code
(written Comp(S) = OK(C)) or a compile-time error (written
Comp(S) = Error). Compile-time errors correspond to cases
where the compiler is unable to produce code, for instance
if the source program is incorrect (syntax error, type error,
(Here, S safe means that none of the possible behaviors of S
is a “going wrong” behavior.) In other words, if S does not go
wrong, then neither does C; moreover, all observable behaviors of C are acceptable behaviors of S.
In the CompCert experiment and the remainder of this
paper, we focus on source and target languages that are deterministic (programs change their behaviors only in response
to different inputs but not because of internal choices) and
on execution environments that are deterministic as well
(the inputs given to the programs are uniquely determined
by their previous outputs). Under these conditions, there
