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.
D. J. Sorin, M. Plakal, A. E. Condon, M. D. Hill, M. M. Martin and D. A. Wood, "Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol," in IEEE Transactions on Parallel & Distributed Systems, vol. 13, no. , pp. 556-578, 2002.