The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.06 - June (2002 vol.13)
pp: 556-578
ABSTRACT
<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>
INDEX TERMS
Cache coherence, protocol specification, protocol verification, memory consistency, multicast snooping.
CITATION
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
6 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool