Causal-Broadcast Memory

Abstract

We investigate the precise consistency guarantees provided by a simple and prominent distributed implementation of shared memory (a.k.a. key-value store) based on the causal broadcast abstraction. We formalize these guarantees within a weak memory model, which we call “causal-broadcast memory” ( $$\text {CBM}$$ , for short), and relate it to several established weak memory models. In particular, our study reveals that $$\text {CBM}$$ is strictly stronger than “causal memory” consistency, previously proposed to encapsulate the same distributed implementation. Additionally, we address two core verification challenges for $$\text {CBM}$$ : (i) deciding whether a single abstract execution graph is consistent, which we show is solvable in polynomial time, and (ii) verifying reachability of control states for client programs operating atop causal-broadcast memory, which we prove to be undecidable.