Specifying and verifying a broadcast and a multicast snooping cache coherence protocol
Daniel J. Sorin, Manoj Plakal, Anne Condon, M.D. Hill, Milo M. K. Martin, David Alvra Wood · IEEE Transactions on Parallel and Distributed Systems · 2002
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.