Formal verification of complex coherence protocols using symbolic state models

Directory-based coherence protocols in shared-memory multiprocessors are so complex that verification techniques based on automated procedures are req uired to:establish their correctness. State enumeration approaches are well -suited to the verification of cache protocols but they face the problem of state space explosion, leading to unacceptable verification time and memor y consumption even for small system configurations. One way to manage this complexity and make the verification feasible is to map the system model to verify onto a symbolic state model (SSM). Since the number of symbolic sta tes is considerably less than the number of system states, an exhaustive st ate search becomes possible, even for large-scale systems and complex proto cols. In this paper, we develop the concepts and notations to verify some propert ies of a directory-based protocol designed for non-FIFO interconnection net works. We compare the verification of the protocol with SSM and with the St anford Mur phi, a verification tool enumerating system states. We show that SSM is much more efficient in terms of verification time and memory consum ption and therefore holds the promise of verifying much more complex protoc ols. A unique feature of SSM is that it verifies protocols for any system s ize and therefore provides reliable verification results in one run of the tool.