ProtoGen: Automatically Generating Directory Cache Coherence Protocols from Atomic Specifications

Nicolai Oswald, Vijay Nagarajan, Daniel J. Sorin

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.
Original languageEnglish
Title of host publication2018 ACM/IEEE 45th Annual International Symposium on Computer Architecture (ISCA)
Place of PublicationLos Angeles, California, USA
PublisherInstitute of Electrical and Electronics Engineers (IEEE)
Number of pages14
ISBN (Electronic)978-1-5386-5984-7
ISBN (Print)978-1-5386-5985-4
Publication statusPublished - 23 Jul 2018
EventThe 45th International Symposium on Computer Architecture - InterContinental Los Angeles Downtown, Los Angeles, United States
Duration: 2 Jun 20186 Jun 2018

Publication series

ISSN (Electronic)2575-713X


ConferenceThe 45th International Symposium on Computer Architecture
Abbreviated titleISCA 2018
Country/TerritoryUnited States
CityLos Angeles
Internet address


Dive into the research topics of 'ProtoGen: Automatically Generating Directory Cache Coherence Protocols from Atomic Specifications'. Together they form a unique fingerprint.

Cite this