Analyzing Cache Coherence with TLA+

Mark Tuttle
Compaq Computer Corporation

We used the specification language TLA+ to analyze the correctness of
two cache-coherence protocols for shared-memory multiprocessors based
on two generations (EV6 and EV7) of the Alpha processor.  The
EV6-based multiprocessor uses a highly-optimized, very complicated
cache-coherence protocol.  After more than two man-years of effort,
four of us were able to write a 1900-line specification of the
algorithm, a 200-line specification of the Alpha memory model, and
about 3000 lines of proof that the algorithm implements the memory
model.  This was far from a complete proof, but enough of a proof to
subject the algorithm to a rigorous analysis, and to discover one bug
in the protocol and one bug in the memory model.  The cache-coherence
protocol for EV7-based multiprocessors is much simpler, bringing a
complete correctness proof within the realm of possibility.  A new
tool, a model checker for TLA+ called TLC, increased the odds of
success.  Using TLC to check multiple invariants uncovered a number of
errors.  The analysis of the first protocol was largely a research
project, but the analysis of the second protocol was a part of the
engineers' own verification process.

This work is joint work with Homayoon Akhiani, Damien Doligez, Paul
Harter, Leslie Lamport, Joshua Scheid, and Yuan Yu.