Report Number: CSL-TR-94-613
Institution: Stanford University, Department of Computer Science
Title: Design and Validation of Update-Based Cache Coherence Protocols
Author: Glasco, David B.
Author: Delagi, Bruce A.
Author: Flynn, Michael J.
Date: March 1994
Abstract: In this paper, we present the details of the two update-based cache coherence protocols for scalable shared-memory multiprocessors that were studied in our previous work. First, the directory structures required for the protocols are briefly reviewed. Next, the state diagrams and some examples of the two update-based protocols are presented; one of the protocols is based on a centralized directory, and the other is based on a singly-linked distributed directory. Protocol deadlock and the additional requirements placed the protocols to avoid such deadlock are also examined. Finally, protocol validation using an exhaustive validation tool known as Murphi is discussed.
http://i.stanford.edu/pub/cstr/reports/csl/tr/94/613/CSL-TR-94-613.pdf