1
$\begingroup$

In Figure 5.1 of the book "Principles of Eventual Consistency" by Sebastin Burckhardt, 2014, Causal Consistency (CC); wiki is (mainly) defined as the conjunction of $hb \subseteq vis$ and $hb \subseteq ar$, where $hb \triangleq (so \cup vis)^{+}$.

An execution satisfies CC if it can be extended by adding $vis$ and $ar$ to an abstract execution which justifies the conditions above; see Definition 3.5.

See also the POPL'2014 paper and the CSUR'2016 paper.


Now, consider the execution in the figure below, where $w(x)0$ denotes a write of 0 to $x$ and $r(x)0$ a read of 0 from $x$.

pram-causal-ar

On the one hand, this execution satisfies CC according to the definition in wiki, because $r(x)1$ can be justified by the serial view of $w(x)0\; w(x)1\; r(x)1$ and $r(x)0$ by $w(x)1\; w(x)0\; r(x)0$.

On the other hand, however, (in my opinion,) it does not satisfy CC according to the $(vis, ar)$ definition for CC above. It is impossible to define the total order $ar$ which must put $w(x)0$ before $w(x)1$ (for justifying $r(x)1$) and put $w(x)1$ before $w(x)0$ (for justifying $r(x)0$).


My questions:

  1. What is wrong with my argument?
  2. How to justify this causally consistent execution in the $(vis, ar)$ framework?
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.