Verification of Cache Coherence Protocols
By Aggregation of Distributed Transactions
(Theory of Computing Systems, vol-31, 1998.)
Seungjoon Park and David L. Dill
This paper presents a method to verify the correctness of protocols
and distributed algorithms. The method compares a state graph of the
implementation with a specification which is a state graph
representing the desired abstract behavior. The steps in the
specification correspond to atomic transactions, which are not atomic
in the implementation.
The method relies on an {\em aggregation function}, which is a type of
abstraction function that aggregates the steps of each transaction in
the implementation into a single atomic transaction in the
specification. The key idea in defining the aggregation function is
that it must complete atomic transactions which have committed but are
not finished.
This paper illustrates the method on a directory-based cache coherence
protocol developed for the Stanford FLASH multiprocessor. The
coherence protocol consisting of more than a hundred different kinds
of implementation steps has been reduced to a specification with six
kinds of atomic transactions. Based on the reduced behavior, it is
very easy to prove crucial properties of the protocol including data
consistency of cached copies at the user level. This is the first
correctness proof verified by a theorem-prover for a cache coherence
protocol of this complexity. The aggregation method is also used to
prove that the reduced protocol satisfies a desired memory consistency
model.