# Confusion about a formal definition of PRAM consistency

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$. 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?

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.
• 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? – hengxin Aug 25 '18 at 7:31
• 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$". – hengxin Aug 26 '18 at 4:38
• 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). – hengxin Aug 26 '18 at 9:31