Verifying cache coherence protocols
Kenneth L. McMillan · IEEE Spectrum · 1996
The shared-memory multiprocessor architecture is becoming prevalent in high-end servers designed to handle many users or large parallel computations. In such a machine, several parallel processors share a common store. To avoid communications bottlenecks, each processor has its own local cache memory that stores recently accessed data from the shared memory. One of the machine's most complex parts is its cache coherence protocol, a system of messages implemented in hardware, by which the processors ensure that their local caches are consistent. Simulation of such systems is particularly unreliable because of their highly asynchronous nature: the exact time at which a given processor will access a given memory location and the exact time delay of messages are unpredictable. As a result, many "race conditions" must be considered in the design and test of the protocol.