Pipe Check: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models

Daniel Lustig, Michael Pellauer, Margaret Rose Martonosi

Research output: Contribution to journalConference articlepeer-review

19 Scopus citations


We present Pipe Check, a methodology and automated tool for verifying that a particular micro architecture correctly implements the consistency model required by its architectural specification. Pipe Check adapts the notion of a "happens before" graph from architecture-level analysis techniques to the micro architecture space. Each node in the "micro architecturally happens before" (μhb) graph represents not only a memory instruction, but also a particular location (e.g., Pipeline stage) within the micro architecture. Architectural specifications such as "preserved program order" are then treated as propositions to be verified, rather than simply as assumptions. Pipe Check allows an architect to easily and rigorously test whether a micro architecture is stronger than, equal in strength to, or weaker than its architecturally-specified consistency model. We also specify and analyze the behavior of common micro architectural optimizations such as speculative load reordering which technically violate formal architecture-level definitions. We evaluate Pipe Check using a library of established litmus tests on a set of open-source pipelines. Using Pipe Check, we were able to validate the largest pipeline, the Open SPARC T2, in just minutes. We also identified a bug in the O3 pipeline of the gem5 simulator.

Original languageEnglish (US)
Article number7011423
Pages (from-to)635-646
Number of pages12
JournalProceedings of the Annual International Symposium on Microarchitecture, MICRO
Issue numberJanuary
StatePublished - Jan 15 2015
Event47th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2014 - Cambridge, United Kingdom
Duration: Dec 13 2014Dec 17 2014

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture


Dive into the research topics of 'Pipe Check: Specifying and Verifying Microarchitectural Enforcement of Memory Consistency Models'. Together they form a unique fingerprint.

Cite this