37 citations · 42 across the 6 of their papers we have counts for
7 papers
täkōFormal: Enabling Robust Software for Programmable Memory Hierarchies (Extended Version)
Pranav Srinivasan, Manos Kapritsos, Yatin A. Manerkar
Accelerators provide large performance and energy-efficiency benefits, but can significantly change the hardware-software interface. The täkō programmable memory hierarchy accelera…
SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns
Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
Microarchitectural security verification of software has seen the emergence of two broad classes of approaches. The first is based on semantic security properties (e.g., non-interf…
Automated Conversion of Axiomatic to Operational Models: Theory and Practice
Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia
A system may be modelled as an operational model (which has explicit notions of state and transitions between states) or an axiomatic model (which is specified entirely as a set of…
UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis
Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu +6
UCLID5 is a tool for the multi-modal formal modeling, verification, and synthesis of systems. It enables one to tackle verification problems for heterogeneous systems such as combi…
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…
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…