Verifying Correct Microarchitectural Enforcement of Memory Consistency Models

Daniel Lustig, Michael Pellauer, Margaret Rose Martonosi

Research output: Contribution to journalArticlepeer-review

5 Scopus citations


Memory consistency models define the rules and guarantees about the ordering and visibility of memory references on multithreaded CPUs and systems on chip. PipeCheck offers a methodology and automated tool for verifying that a particular microarchitecture correctly implements the consistency model required by its architectural specification.

Original languageEnglish (US)
Article number7106405
Pages (from-to)72-82
Number of pages11
JournalIEEE Micro
Issue number3
StatePublished - May 1 2015

All Science Journal Classification (ASJC) codes

  • Software
  • Hardware and Architecture
  • Electrical and Electronic Engineering


  • PipeCheck
  • computer architecture
  • formal verification
  • memory architecture
  • memory consistency model
  • processor microarchitecture


Dive into the research topics of 'Verifying Correct Microarchitectural Enforcement of Memory Consistency Models'. Together they form a unique fingerprint.

Cite this