Specifying and verifying a broadcast and a multicast snooping cache coherence protocol
- 7 August 2002
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Parallel and Distributed Systems
- Vol. 13 (6) , 556-578
- https://doi.org/10.1109/tpds.2002.1011412
Abstract
We develop a specification methodology that documents and specifies a cache coherence protocol in eight tables: the states, events, actions, and transitions of the cache and memory controllers. We then use this methodology to specify a detailed, modern three-state broadcast snooping protocol with an unordered data network and an ordered address network that allows arbitrary skew. We also present a detailed specification of a new protocol called multicast snooping (Bilir et al., 1999) and, in doing so, we better illustrate the utility of the table-based specification methodology. Finally, we demonstrate a technique for verification of the multicast snooping protocol, through the sketch of a manual proof that the specification satisfies a sequentially consistent memory model.Keywords
This publication has 17 references indexed in Scilit:
- Verifying sequential consistency on shared-memory multiprocessors by model checkingIEEE Transactions on Parallel and Distributed Systems, 2003
- Origin system design methodology and experience: 1M-gate ASICs and beyondPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal automatic verification of cache coherence in multiprocessors with relaxed memory modelsIEEE Transactions on Parallel and Distributed Systems, 2000
- Using Lamport clocks to reason about relaxed memory modelsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1999
- Design verification of the S3.mp cache-coherent shared-memory systemIEEE Transactions on Computers, 1998
- Using “test model-checking” to verify the Runway-PA8000 memory modelPublished by Association for Computing Machinery (ACM) ,1998
- Verification techniques for cache coherence protocolsACM Computing Surveys, 1997
- An executable specification, analyzer and verifier for RMO (relaxed memory order)Published by Association for Computing Machinery (ACM) ,1995
- Using formal verification/analysis methods on the critical path in system design: A case studyPublished by Springer Nature ,1995
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess ProgramsIEEE Transactions on Computers, 1979