Specifying and verifying a broadcast and a multicast snooping cache coherence protocol

Journal Article (Journal Article)

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 skews. We also present a detailed specification of a new protocol called Multicast Snooping [6] 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.

Full Text

Duke Authors

Cited Authors

  • Sorin, DJ; Plakal, M; Condon, AE; Hill, MD; Martin, MMK; Wood, DA

Published Date

  • June 1, 2002

Published In

Volume / Issue

  • 13 / 6

Start / End Page

  • 556 - 578

International Standard Serial Number (ISSN)

  • 1045-9219

Digital Object Identifier (DOI)

  • 10.1109/TPDS.2002.1011412

Citation Source

  • Scopus