57 citations · 97 across the 4 of their papers we have counts for
5 papers
RealityCheck: Bringing Modularity, Hierarchy, and Abstraction to Automated Microarchitectural Memory Consistency Verification
Yatin A. Manerkar, Daniel Lustig, Margaret Martonosi
Modern SoCs are heterogeneous parallel systems comprised of components developed by distinct teams and possibly even different vendors. The memory consistency model (MCM) of proces…
MeltdownPrime and SpectrePrime: Automatically-Synthesized Attacks Exploiting Invalidation-Based Coherence Protocols
Caroline Trippel, Daniel Lustig, Margaret Martonosi
The recent Meltdown and Spectre attacks highlight the importance of automated verification techniques for identifying hardware security vulnerabilities. We have developed a tool fo…
Weak Memory Models with Matching Axiomatic and Operational Definitions
Sizhuo Zhang, Muralidaran Vijayaraghavan, Dan Lustig +1
Memory consistency models are notorious for being difficult to define precisely, to reason about, and to verify. More than a decade of effort has gone into nailing down the definit…
Counterexamples and Proof Loophole for the C/C++ to POWER and ARMv7 Trailing-Sync Compiler Mappings
Yatin A. Manerkar, Caroline Trippel, Daniel Lustig +2
The C and C++ high-level languages provide programmers with atomic operations for writing high-performance concurrent code. At the assembly language level, C and C++ atomics get ma…
TriCheck: Memory Model Verification at the Trisection of Software, Hardware, and ISA
Caroline Trippel, Yatin A. Manerkar, Daniel Lustig +2
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…