Full-Stack Memory Model Verification with TriCheck

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

Research output: Contribution to journalArticlepeer-review

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 languageEnglish (US)
Pages (from-to)58-68
Number of pages11
JournalIEEE Micro
Volume38
Issue number3
DOIs
StatePublished - 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

Fingerprint Dive into the research topics of 'Full-Stack Memory Model Verification with TriCheck'. Together they form a unique fingerprint.

Cite this