Issue No.06 - June (2002 vol.13)
<p>In this paper, 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 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.</p>
Cache coherence, protocol specification, protocol verification, memory consistency, multicast snooping.
Daniel J. Sorin, Manoj Plakal, Anne E. Condon, Mark D. Hill, Milo M.K. Martin, David A. Wood, "Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol", IEEE Transactions on Parallel & Distributed Systems, vol.13, no. 6, pp. 556-578, June 2002, doi:10.1109/TPDS.2002.1011412