Verifying Correct Microarchitectural Enforcement of Memory Consistency Models

Daniel Lustig; Michael Pellauer; Margaret Rose Martonosi

doi:10.1109/MM.2015.47

Verifying Correct Microarchitectural Enforcement of Memory Consistency Models

Daniel Lustig
, Michael Pellauer
, Margaret Rose Martonosi

Research output: Contribution to journal › Article › peer-review

6 Scopus citations

Abstract

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 language	English (US)
Article number	7106405
Pages (from-to)	72-82
Number of pages	11
Journal	IEEE Micro
Volume	35
Issue number	3
DOIs	https://doi.org/10.1109/MM.2015.47
State	Published - May 1 2015

All Science Journal Classification (ASJC) codes

Software
Hardware and Architecture
Electrical and Electronic Engineering

Keywords

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

Access to Document

10.1109/MM.2015.47

Cite this

@article{3b81749ca79f499e822dc333fdf008a1,

title = "Verifying Correct Microarchitectural Enforcement of Memory Consistency Models",

abstract = "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.",

keywords = "PipeCheck, computer architecture, formal verification, memory architecture, memory consistency model, processor microarchitecture",

author = "Daniel Lustig and Michael Pellauer and Martonosi, \{Margaret Rose\}",

note = "Publisher Copyright: {\textcopyright} 1981-2012 IEEE.",

year = "2015",

month = may,

day = "1",

doi = "10.1109/MM.2015.47",

language = "English (US)",

volume = "35",

pages = "72--82",

journal = "IEEE Micro",

issn = "0272-1732",

publisher = "IEEE Computer Society",

number = "3",

}

TY - JOUR

T1 - Verifying Correct Microarchitectural Enforcement of Memory Consistency Models

AU - Lustig, Daniel

AU - Pellauer, Michael

AU - Martonosi, Margaret Rose

PY - 2015/5/1

Y1 - 2015/5/1

N2 - 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.

AB - 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.

KW - PipeCheck

KW - computer architecture

KW - formal verification

KW - memory architecture

KW - memory consistency model

KW - processor microarchitecture

UR - https://www.scopus.com/pages/publications/84933056043

UR - https://www.scopus.com/pages/publications/84933056043#tab=citedBy

U2 - 10.1109/MM.2015.47

DO - 10.1109/MM.2015.47

M3 - Article

AN - SCOPUS:84933056043

SN - 0272-1732

VL - 35

SP - 72

EP - 82

JO - IEEE Micro

JF - IEEE Micro

IS - 3

M1 - 7106405

ER -

Verifying Correct Microarchitectural Enforcement of Memory Consistency Models

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this