PipeProof: Automated memory consistency proofs for microarchitectural specifications

Yatin A. Manerkar, Daniel Lustig, Margaret Rose Martonosi, Aarti Gupta

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

9 Scopus citations


Memory consistency models (MCMs) specify rules which constrain the values that can be returned by load instructions in parallel programs. To ensure that parallel programs run correctly, verification of hardware MCM implementations would ideally be complete; i.e. verified as being correct across all possible executions of all possible programs. However, no existing automated approach is capable of such complete verification. To help fill this verification gap, we present PipeProof, a methodology and tool for complete MCM verification of an axiomatic microarchitectural (hardware-level) ordering specification against an axiomatic ISA-level MCM specification. PipeProof can automatically prove a microarchitecture correct in all cases, or return an indication (often a counterexample) that the microarchitecture could not be verified. To accomplish unbounded verification, PipeProof introduces the novel Transitive Chain Abstraction to represent microarchitectural executions of an arbitrary number of instructions using only a small, finite number of instructions. With the help of this abstraction, PipeProof proves microarchitectural correctness using an automatic abstraction refinement approach. PipeProof's implementation also includes algorithmic optimizations which improve runtime by greatly reducing the number of cases considered. As a proof-of-concept study, we present results for modelling and proving correct simple microarchitectures implementing the SC and TSO MCMs. PipeProof verifies both case studies in under an hour, showing that it is indeed possible to automate microarchitectural MCM correctness proofs.

Original languageEnglish (US)
Title of host publicationProceedings - 51st Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2018
PublisherIEEE Computer Society
Number of pages14
ISBN (Electronic)9781538662403
StatePublished - Dec 12 2018
Event51st Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2018 - Fukuoka, Japan
Duration: Oct 20 2018Oct 24 2018

Publication series

NameProceedings of the Annual International Symposium on Microarchitecture, MICRO
ISSN (Print)1072-4451


Other51st Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2018

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture


  • Abstraction refinement
  • Automated verification
  • Formal verification
  • Happens-before graphs
  • Memory consistency models


Dive into the research topics of 'PipeProof: Automated memory consistency proofs for microarchitectural specifications'. Together they form a unique fingerprint.

Cite this