Transistency Models: Memory Ordering at the Hardware-OS Interface

Daniel Lustig; Geet Sethi; Abhishek Bhattacharjee; Margaret Rose Martonosi

doi:10.1109/MM.2017.69

Transistency Models: Memory Ordering at the Hardware-OS Interface

Daniel Lustig, Geet Sethi, Abhishek Bhattacharjee, Margaret Rose Martonosi

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

2 Scopus citations

Abstract

This article introduces the transistency model, a set of memory ordering rules at the intersection of virtual-to-physical address translation and memory consistency models. Using their COATCheck tool, the authors show how to rigorously model, analyze, and verify the correctness of a given system's microarchitecture and software stack with respect to its transistency model specification.

Original language	English (US)
Article number	7948679
Pages (from-to)	88-97
Number of pages	10
Journal	IEEE Micro
Volume	37
Issue number	3
DOIs	https://doi.org/10.1109/MM.2017.69
State	Published - 2017

All Science Journal Classification (ASJC) codes

Software
Hardware and Architecture
Electrical and Electronic Engineering

Keywords

COATCheck
Hardware-software
Transistency model
formal verification
memory consistency
memory ordering
modeling

Access to Document

10.1109/MM.2017.69

Cite this

@article{d6236175ae9947d5b662ddc3d2124ab6,

title = "Transistency Models: Memory Ordering at the Hardware-OS Interface",

abstract = "This article introduces the transistency model, a set of memory ordering rules at the intersection of virtual-to-physical address translation and memory consistency models. Using their COATCheck tool, the authors show how to rigorously model, analyze, and verify the correctness of a given system's microarchitecture and software stack with respect to its transistency model specification.",

keywords = "COATCheck, Hardware-software, Transistency model, formal verification, memory consistency, memory ordering, modeling",

author = "Daniel Lustig and Geet Sethi and Abhishek Bhattacharjee and Martonosi, \{Margaret Rose\}",

note = "Publisher Copyright: {\textcopyright} 2017 IEEE.",

year = "2017",

doi = "10.1109/MM.2017.69",

language = "English (US)",

volume = "37",

pages = "88--97",

journal = "IEEE Micro",

issn = "0272-1732",

publisher = "IEEE Computer Society",

number = "3",

}

TY - JOUR

T1 - Transistency Models

T2 - Memory Ordering at the Hardware-OS Interface

AU - Lustig, Daniel

AU - Sethi, Geet

AU - Bhattacharjee, Abhishek

AU - Martonosi, Margaret Rose

PY - 2017

Y1 - 2017

N2 - This article introduces the transistency model, a set of memory ordering rules at the intersection of virtual-to-physical address translation and memory consistency models. Using their COATCheck tool, the authors show how to rigorously model, analyze, and verify the correctness of a given system's microarchitecture and software stack with respect to its transistency model specification.

AB - This article introduces the transistency model, a set of memory ordering rules at the intersection of virtual-to-physical address translation and memory consistency models. Using their COATCheck tool, the authors show how to rigorously model, analyze, and verify the correctness of a given system's microarchitecture and software stack with respect to its transistency model specification.

KW - COATCheck

KW - Hardware-software

KW - Transistency model

KW - formal verification

KW - memory consistency

KW - memory ordering

KW - modeling

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

UR - https://www.scopus.com/inward/citedby.url?scp=85021095445&partnerID=8YFLogxK

U2 - 10.1109/MM.2017.69

DO - 10.1109/MM.2017.69

M3 - Article

AN - SCOPUS:85021095445

SN - 0272-1732

VL - 37

SP - 88

EP - 97

JO - IEEE Micro

JF - IEEE Micro

IS - 3

M1 - 7948679

ER -

Transistency Models: Memory Ordering at the Hardware-OS Interface

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this