5
$\begingroup$

I am reading the paper "Consistency in Non-Transactional Distributed Storage Systems" by Paolo Viotti and Marko Vukolić. The authors provide a comprehensive survey of various consistency semantics based on the notions of history, abstract execution, and the $vis$ (visibility) and $ar$ (arbitration) relations, following Burckhardt (book).

I have some difficulty in understanding the definition of PRAM consistency (wiki). Informally, PRAM requires all processes see memory writes from one process in the order they were issued from the process. Writes from different processes may be seen in a different order on different processes.

In this paper (page 10), the authors define PRAM consistency by requiring the visibility relation ($vis$) to be a superset of session order ($so$; aka, program order). Formally, $$\text{PRAM} \triangleq so \subseteq vis.$$

Consider the history below, where $w(x)0$ denotes a write of $0$ to $x$ and $r(x)0$ a read of $0$ from $x$.

pram-non-example

This history does not satisfy PRAM consistency, because the only serial view of process $p_1$ is $w(x)0, w(x)1, r(x)1, r(x)0$ which is invalid.

However, according to the definition above, $r(x)1$ can be justified by the serial view of $w(x)1, r(x)1$, since the visibility set of $r(x)1$ is $vis^{-1}(r(x)1) = \{w(x)1\}$. Similarly, $r(x)0$ can be justified by the serial view of $r(x)1, w(x)0, r(x)0$, since the visible set of $r(x)0$ is $vis^{-1}(r(x)0) = \{w(x)0, r(x)1\}$.

To make $w(x)1$ visible to $r(x)0$, we require $(vis;so) \subseteq vis$. Therefore, in my opinion, PRAM should be defined as $$\text{PRAM} \triangleq so \subseteq vis \land (vis;so) \subseteq vis.$$ (By the way, I think the predicate $RVal(\mathcal{F})$ is also needed.)

What is wrong with my arguments above?

$\endgroup$

1 Answer 1

2
+25
$\begingroup$

When they define PRAM (page 11 of the arxiv preprint) they actually state that vis is a partial order (in particular, transitive):

We define PRAM consistency by requiring the visibility partial order to be a superset of session order: $$\text{PRAM} \triangleq so \subseteq vis.$$

Thus, the offending arrow in your diagram, from $w(x)0$ to $r(x)0$, is superfluous, as it is in the transitive closure of the other vis arrows. So the $w(x)1$ write is already visible at the time when you would do $r(x)0$, so that read does not occur.

$\endgroup$
4
  • $\begingroup$ Great thanks. This resolves my confusion about this example. However, the "transitivity" requirement of $vis$ seems too strong for PRAM. Consider a history involving three processes: $p_0$ with $w(x)0, w(x)1$, $p_1$ with $r(x)1, w(x) 2$, and $p_3$ with $r(x)2, r(x)0$. This history satisfies PRAM. However, the read $r(x)0$ cannot be justified according to the definition with "transitive" $vis$. What do you think of it? $\endgroup$
    – hengxin
    Aug 25, 2018 at 7:31
  • $\begingroup$ According to Theorem 3.2 of "A Unified Theory of Shared Memory Consistency" (JACM'04), the operations visible (informally, not the $vis$ relation) to each process are its own reads and all writes. In particular, all processes are not required to observe all operatoins. Therefore, $p_0$ can be justified by the serial view of "$w(x)0, w(x)1, w(x)2$", $p_1$ by "$w(x)0, w(x)1, r(x)1, w(x)2$", and $p_2$ by "$w(x)2, r(x)2, w(x)0, r(x)0, w(x)1$". $\endgroup$
    – hengxin
    Aug 26, 2018 at 4:38
  • 1
    $\begingroup$ Hmm yes it seems that in some parts of the paper they don't assume transitivity of vis $\endgroup$ Aug 26, 2018 at 7:51
  • $\begingroup$ On page 5, it only requires $vis$ to be an acyclic natural relation. In Section 3.5, it seems that the transitivity of $vis$ is required to define causality (in particular, the happened-before relation). $\endgroup$
    – hengxin
    Aug 26, 2018 at 9:31

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.