Full-Stack Memory Model Verification with TriCheck

Caroline Trippel; Yatin A. Manerkar; Daniel Lustig; Michael Pellauer; Margaret Martonosi

doi:10.1109/MM.2018.032271062

Full-Stack Memory Model Verification with TriCheck

Caroline Trippel, Yatin A. Manerkar, Daniel Lustig, Michael Pellauer, Margaret Martonosi

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

3 Scopus citations

Abstract

Memory consistency models (MCMs) govern inter-module interactions in a shared memory system and are defined at the various layers of the hardware-software stack. TriCheck is the first tool for full-stack MCM verification. Using TriCheck, we uncovered under-specifications in the draft RISC-V instruction set architecture (ISA) and identified flaws in previously 'proven-correct' C11 compiler mappings.

Original language	English (US)
Pages (from-to)	58-68
Number of pages	11
Journal	IEEE Micro
Volume	38
Issue number	3
DOIs	https://doi.org/10.1109/MM.2018.032271062
State	Published - May 1 2018

All Science Journal Classification (ASJC) codes

Software
Hardware and Architecture
Electrical and Electronic Engineering

Keywords

computer architecture
hardware
heterogeneous parallelism
memory consistency
shared memory

Access to Document

10.1109/MM.2018.032271062

Cite this

@article{c81f2f445ab64f0da96f414bd478439d,

title = "Full-Stack Memory Model Verification with TriCheck",

abstract = "Memory consistency models (MCMs) govern inter-module interactions in a shared memory system and are defined at the various layers of the hardware-software stack. TriCheck is the first tool for full-stack MCM verification. Using TriCheck, we uncovered under-specifications in the draft RISC-V instruction set architecture (ISA) and identified flaws in previously 'proven-correct' C11 compiler mappings.",

keywords = "computer architecture, hardware, heterogeneous parallelism, memory consistency, shared memory",

author = "Caroline Trippel and Manerkar, \{Yatin A.\} and Daniel Lustig and Michael Pellauer and Margaret Martonosi",

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

year = "2018",

month = may,

day = "1",

doi = "10.1109/MM.2018.032271062",

language = "English (US)",

volume = "38",

pages = "58--68",

journal = "IEEE Micro",

issn = "0272-1732",

publisher = "IEEE Computer Society",

number = "3",

}

TY - JOUR

T1 - Full-Stack Memory Model Verification with TriCheck

AU - Trippel, Caroline

AU - Manerkar, Yatin A.

AU - Lustig, Daniel

AU - Pellauer, Michael

AU - Martonosi, Margaret

PY - 2018/5/1

Y1 - 2018/5/1

N2 - Memory consistency models (MCMs) govern inter-module interactions in a shared memory system and are defined at the various layers of the hardware-software stack. TriCheck is the first tool for full-stack MCM verification. Using TriCheck, we uncovered under-specifications in the draft RISC-V instruction set architecture (ISA) and identified flaws in previously 'proven-correct' C11 compiler mappings.

AB - Memory consistency models (MCMs) govern inter-module interactions in a shared memory system and are defined at the various layers of the hardware-software stack. TriCheck is the first tool for full-stack MCM verification. Using TriCheck, we uncovered under-specifications in the draft RISC-V instruction set architecture (ISA) and identified flaws in previously 'proven-correct' C11 compiler mappings.

KW - computer architecture

KW - hardware

KW - heterogeneous parallelism

KW - memory consistency

KW - shared memory

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

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

U2 - 10.1109/MM.2018.032271062

DO - 10.1109/MM.2018.032271062

M3 - Article

AN - SCOPUS:85047014570

SN - 0272-1732

VL - 38

SP - 58

EP - 68

JO - IEEE Micro

JF - IEEE Micro

IS - 3

ER -

Full-Stack Memory Model Verification with TriCheck

Abstract

All Science Journal Classification (ASJC) codes

Keywords

Access to Document

Other files and links

Fingerprint

Cite this