Full-Stack Memory Model Verification with TriCheck

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)
Margaret Martonosi (Princeton)

Publication Date

Research Area