TriCheck
Abstract
Memory consistency models (MCMs) which govern inter-module interactions in a shared memory system, are a significant, yet often under-appreciated, aspect of system design. MCMs are defined at the various layers of the hardware-software stack, requiring thoroughly verified specifications, compilers, and implementations at the interfaces between layers. Current verification techniques evaluate segments of the system stack in isolation, such as proving compiler mappings from a high-level language (HLL) to an ISA or proving validity of a microarchitectural implementation of an ISA.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Apr 04, 2017
- Source ID
- 10.1145/3093337.3037719
Entities
People
- Caroline Trippel
- Daniel Lustig
- Margaret Martonosi
- Michael Pellauer
- Yatin A. Manerkar
Organizations
- Defense Advanced Research Projects Agency
- National Science Foundation
- Nvidia
- Princeton University