activity
20152018
most citedWeak Memory Models: Balancing Definitional Simplicity and Implementation Flexibility

10 citations · 29 across the 6 of their papers we have counts for

collaborators

6 papers

cs.AR2018★ 7 cited

Constructing a Weak Memory Model

Sizhuo Zhang, Muralidaran Vijayaraghavan, Andrew Wright +2

Weak memory models are a consequence of the desire on part of architects to preserve all the uniprocessor optimizations while building a shared memory multiprocessor. The efforts t…

cs.PL2017

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…

cs.PL2017★ 10 cited

Weak Memory Models: Balancing Definitional Simplicity and Implementation Flexibility

Sizhuo Zhang, Muralidaran Vijayaraghavan, Arvind

The memory model for RISC-V, a newly developed open source ISA, has not been finalized yet and thus, offers an opportunity to evaluate existing memory models. We believe RISC-V sho…

cs.PL2017

An Operational Framework for Specifying Memory Models using Instantaneous Instruction Execution

Sizhuo Zhang, Muralidaran Vijayaraghavan, Arvind

There has been great progress recently in formally specifying the memory model of microprocessors like ARM and POWER. These specifications are, however, too complicated for reasoni…

cs.PL2016★ 3 cited

Taming Weak Memory Models

Sizhuo Zhang, Arvind, Muralidaran Vijayaraghavan

Speculative techniques in microarchitectures relax various dependencies in programs, which contributes to the complexity of (weak) memory models. We show using WMM, a new weak memo…

cs.DC2015★ 9 cited

A Proof of Correctness for the Tardis Cache Coherence Protocol

Xiangyao Yu, Muralidaran Vijayaraghavan, Srinivas Devadas

We prove the correctness of a recently-proposed cache coherence protocol, Tardis, which is simple, yet scalable to high processor counts, because it only requires O(logN) storage p…