Communications - July 2009

interference edge are assigned different colors. We use the coloring heuristic of George and Appel. Since this heuris-

9

tic is difficult to prove correct directly, we implement it as unverified Caml code, then validate its results a posteriori using a simple verifier written and proved correct in Coq. Like many NP-hard problems, graph coloring is a paradigmatic example of an algorithm that is easier to validate a posteriori than to directly prove correct. The correctness conditions for the result j of the coloring are:

1. j (r) ≠ j (r ′) if r and r′ interfere

2. j (r) ≠ l if r and l interfere

3. j(r) and r have the same register class (int or float)

These conditions are checked by boolean-valued functions written in Coq and proved to be decision procedures for the three conditions. Compilation is aborted if the checks fail, which denotes a bug in the external graph coloring routine.

Finally, the original RTL code is rewritten. Each reference to pseudo-register r is replaced by a reference to its location j (r). Additionally, coalescing and dead code elimination are

→
performed. A side-effect-free instruction l : op(op, r , r, l′) or
→
l: load(k, mode, r , r, l′) is replaced by a no-op l: nop(l′) if the
result r is not live after l (dead code elimination). Likewise, a
move instruction l : op(move, r , r , l′) is replaced by a no-op
sd
l : nop(l′) if j (r ) = j (r ) (coalescing).
ds

4. 3. Proving semantic preservation

To prove that a program transformation preserves semantics, a standard technique used throughout the CompCert project is to show a simulation diagram: each transition in the original program must correspond to a sequence of transitions in the transformed program that have the same observable effects (same traces of input–output operations, in our case) and preserve as an invariant a given binary relation ∼ between execution states of the original and transformed programs. In the case of register allocation, each original transition corresponds to exactly one transformed transition, resulting in the following “lock-step” simulation diagram:

S 1

t

S 2

∼

S � 1

t

S � 2

(Solid lines represent hypotheses; dotted lines represent conclusions.) If, in addition, the invariant ∼ relates initial states as well as final states, such a simulation diagram implies that any execution of the original program corresponds to an execution of the transformed program that produces exactly the same trace of observable events. Semantic preservation therefore follows.

The gist of a proof by simulation is the definition of the ∼ relation. What are the conditions for two states S(Σ, g, s, l, R, M) and S(Σ′, g ′, s ′, l′, R′, M′) to be related? Intuitively, since register allocation preserves program structure and

control flows, the control points l and l′ must be identical, and the CFG g ′ must be the result of transforming g according to some register allocation j as described in Section 4. 2. Likewise, since register allocation preserves memory stores and allocations, the memory states and stack pointers must be identical: M′ = M and s ′ = s.

The nonobvious relation is between the register state R of the original program and the location state R′ of the transformed program. Given that each pseudo-register r is mapped to the location j (r), we could naively require that R(r) = R′(j (r) ) for all r. However, this requirement is much too strong, as it essentially precludes any sharing of a location between two pseudo-registers whose live ranges are disjoint. To obtain the correct requirement, we need to consider what it means, semantically, for a pseudo-register to be live or dead at a program point l. A dead pseudo-register r is such that its value at point l has no influence on the program execution, because either r is never read later, or it is always redefined before being read. Therefore, in setting up the correspondence between register and location values, we can safely ignore those registers that are dead at the current point l. It suffices to require the following condition:

R(r) = R′(j (r) ) for all pseudo-registers r live at point l.

Once the relation between states is set up, proving the simulation diagram above is a routine case inspection on the various transition rules of the RTL semantics. In doing so, one comes to the pleasant realization that the dataflow inequations defining liveness, as well as Chaitin’s rules for constructing the interference graph, are the minimal sufficient conditions for the invariant between register states R, R′ to be preserved in all cases.

5. ConCLusions AnD PeRsPeCTiVes

The CompCert experiment described in this paper is still ongoing, and much work remains to be done: handle a larger subset of C (e.g. including goto); deploy and prove correct more optimizations; target other processors beyond PowerPC; extend the semantic preservation proofs to shared-memory concurrency, etc. However, the preliminary results obtained so far provide strong evidence that the initial goal of formally verifying a realistic compiler can be achieved, within the limitations of today’s proof assistants, and using only elementary semantic and algorithmic approaches. The techniques and tools we used are very far from perfect—more proof automation, higher-level semantics and more modern intermediate representations all have the potential to significantly reduce the proof effort— but good enough to achieve the goal.

Looking back at the results obtained, we did not completely rule out all uncertainty concerning the correctness of the compiler, but reduced the problem of trusting the whole compiler down to trusting the following parts: