#StackBounty: #pl.programming-languages #dc.distributed-comp #dc.parallel-comp #concurrency #formal-methods Confusion about a formal de…

Bounty: 50

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)0, w(x)1, r(x)1$ and $r(x)0$ can be justified by the serial view of $w(x)0$, since the visible set ($vis^{-1}$) of $r(x)0$ contains only $w(x)0$.

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?


Get this bounty!!!

Leave a Reply

This site uses Akismet to reduce spam. Learn how your comment data is processed.