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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Causal-Broadcast Memory

  • Amir Karniel,
  • Ori Lahav

摘要

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.