<p>When they define PRAM (page 11 of the <a href="https://arxiv.org/pdf/1512.00168.pdf" rel="nofollow noreferrer">arxiv preprint</a>) 
they actually state that <em>vis</em> is a <strong>partial order</strong> (in particular, transitive):</p>

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

<p>Thus, the offending arrow in your diagram, from $w(x)0$ to $r(x)0$, is superfluous, as it is in the <strong>transitive</strong> closure of the other <em>vis</em> 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.</p>

CC BY-SA 4.0
2018-08-25T07:31:54.960Z
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
CC BY-SA 4.0
2018-08-26T04:38:24.500Z
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
CC BY-SA 4.0
2018-08-26T07:51:24.743Z
Hmm yes it seems that in some parts of the paper they don't assume transitivity of *vis*
Bjørn Kjos-Hanssen
CC BY-SA 4.0
2018-08-26T09:31:34.743Z
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
CC BY-SA 4.0
2018-08-25T03:01:57.237Z
2018-08-25T03:01:57.237Z
Bjørn Kjos-Hanssen
<p>I am reading the paper <a href="https://dl.acm.org/citation.cfm?id=2926965" rel="nofollow noreferrer">"Consistency in Non-Transactional Distributed Storage Systems"</a> 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 <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/final-printversion-10-5-14.pdf" rel="nofollow noreferrer">Burckhardt (book)</a>.</p>

<p>I have some difficulty in understanding the definition of <a href="https://en.wikipedia.org/wiki/PRAM_consistency" rel="nofollow noreferrer">PRAM consistency (wiki)</a>. 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.</p>

<p>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.$$</p>

<p>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$.</p>

<p><a href="https://i.sstatic.net/I3v3Y.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/I3v3Y.png" alt="pram-non-example"></a></p>

<p>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.</p>

<p>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\}$. </p>

<p>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.)</p>

<p>What is wrong with my arguments above?</p>

<pl.programming-languages><dc.distributed-comp><dc.parallel-comp><concurrency><formal-methods>
Confusion about a formal definition of PRAM consistency
hengxin
# Confusion about a formal definition of PRAM consistency

(Asked by: username_0 on 2018-08-21)

I am reading the paper ["Consistency in Non-Transactional Distributed Storage Systems"](https://dl.acm.org/citation.cfm?id=2926965) 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)](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/final-printversion-10-5-14.pdf).

I have some difficulty in understanding the definition of [PRAM consistency (wiki)](https://en.wikipedia.org/wiki/PRAM_consistency). 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](https://i.sstatic.net/I3v3Y.png)](https://i.sstatic.net/I3v3Y.png)

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?

**Tags:** pl.programming-languages, dc.distributed-comp, dc.parallel-comp, concurrency, formal-methods

---

## 1 answers

### Answer by username_1 on 2018-08-25. Score: 2

When they define PRAM (page 11 of the [arxiv preprint](https://arxiv.org/pdf/1512.00168.pdf))
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.

> **Comments:**
> **username_0**: 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?  
> **username_0**: 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$".  
> **username_1**: Hmm yes it seems that in some parts of the paper they don't assume transitivity of *vis*  
> **username_0**: 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).  

---

