Causal-Broadcast Memory
摘要
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.