1. [Publications](/publications)
2. Full-Stack Memory Model Verification with TriCheck
 
 # Full-Stack Memory Model Verification with TriCheck

  ![Publication image](/sites/default/files/styles/wide/public/default_images/default.jpeg?itok=qUFsuJCP "Publication image")

 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.



 ## Authors



Caroline Trippel (Princeton)

Yatin A. Manerkar (Princeton)

[Daniel Lustig](/person/daniel-lustig)

[Michael Pellauer](/person/michael-pellauer)

Margaret Martonosi (Princeton)

 

 

 ## Publication Date



Friday, May 11, 2018

 

 ## Published in



[IEEE Micro (Issue: Top Picks of the 2017 Computer Architecture Conferences)](https://ieeexplore.ieee.org/document/8357999)

 

 ## Research Area



[Computer Architecture](/research-area/computer-architecture)

 

 

 ## External Links



[IEEE Digital Library](https://ieeexplore.ieee.org/document/8357999)

 

 

 ## Copyright



This material is posted here with permission of the IEEE. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to <pubs-permissions@ieee.org>.