ProtoGen: Automatically generating directory cache coherence protocols from atomic specifications


Conference Paper

© 2018 IEEE. Designing directory cache coherence protocols is complicated because coherence transactions are not atomic in modern multicore processors. A coherence transaction comprises multiple messages, and these messages can interleave with other conflicting coherence transactions initiated by other cores. To overcome this architectural challenge, we present ProtoGen, an automated tool for taking the description of a directory protocol with atomic transactions (i.e., no concurrency) and generating the corresponding protocol for a multicore with non-atomic transactions. ProtoGen outputs the finite state Machines for the cache and directory controllers, including all of the transient states that are possible with concurrent transactions. We have used ProtoGen to generate complete MSI, MESI, and MOSI protocols given their stable state protocol specifications. We have verified the generated protocols for safety and deadlock freedom using the MurĪ• model checker. Our generated protocols are identical to or better than manually generated protocols, at times even discovering opportunities to reduce stalling.

Full Text

Duke Authors

Cited Authors

  • Oswald, N; Nagarajan, V; Sorin, DJ

Published Date

  • July 19, 2018

Published In

Start / End Page

  • 247 - 260

International Standard Serial Number (ISSN)

  • 1063-6897

International Standard Book Number 13 (ISBN-13)

  • 9781538659847

Digital Object Identifier (DOI)

  • 10.1109/ISCA.2018.00030

Citation Source

  • Scopus