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