Formal automatic verification of cache coherence in multiprocessors with relaxed memory models

State-based, formal methods have been successfully applied to the automatic verification of cache coherence in sequentially consistent systems. Howeve r, coherence in shared-memory multiprocessors under a relaxed memory model is much more complex to verify automatically. With relaxed memory models, i ncoming invalidations and outgoing updates can be delayed in each cache whi le processors are allowed to race ahead. This buffering of memory accesses considerably increases the amount of state in each cache and the complexity of protocol interactions. Moreover, because caches can hold inconsistent c opies of the same data for long periods of time, coherence cannot be verifi ed by simply checking that cached copies are identical at all times. This p aper makes two major contributions. First, we demonstrate how to model and verify cache coherence under a relaxed memory model in the context of state -based verification methods. Frameworks for modeling the hardware and for g enerating correct memory access sequences driving the hardware model are de veloped. We also show correctness properties which must be verified on the hardware model. Second, we demonstrate a successful application of a state- based verification tool called SSM for the verification of the delayed prot ocol, an aggressive protocol for relaxed memory models. SSM is based on an abstraction technique preserving the properties to verify. We show that wit h classical, explicit approaches the verification of cache coherence is rea listically unfeasible because of the state space explosion problem, whereas SSM is able to verify protocols both at both behavioral and message-passin g levels.