In the POPL'14 paper "Replicated Data Types: Specification, Verification, Optimality" and the book "Principles of Eventual Consistency", the authors propose a formal framework for specifying distributed consistency models via the $vis$ (visibility) and $ar$ (arbitration) relations.

Visibility is an acyclic relation over operations. If an operation $a$ is visible to $b$, it means that the effect of $a$ is visible to the client performing $b$. $...$ We call two updates concurrent if they cannot see each other, i.e., are not ordered by visibility.

Arbitration is used to indicate how the system resolves update conflicts, i.e. how it handles concurrent updates that do not commute. It is a total order on operations. If an operation $a$ is arbitrated before $b$, it means that the system considers the operation $a$ to happen earlier than operation $b$.

A history $H$ (consisting of operations) satisfies a consistency guarantee $\mathcal{P}$ if it can be extended (by adding visibility and arbitration) to an abstract execution that satisfies them. One of the basic consistency guarantees is the return value consistency, which says that, in the context of read/write registers, each read should read from the last write visible ($vis$) to it according to the ordering specified by $ar$.

Given the background above, let us consider a simple consistency guarantee called read my writes:

Read my writes is a property that also applies to a sequence of operations performed by a single client. It guarantees the effects of all writes that were performed by the client are visible to the client's subsequent reads. If a client writes a new value for a data object and then reads this object, the read will return the value that was last written (emphasis added) by the client (or some other value that was later written by a different client).

The book above defines it as $$\text{RMW} \triangleq (so \subseteq vis)$$ where $so$ denotes the "same session relation".

The CSUR'16 survey "Consistency in Non-Transactional Distributed Storage Systems" defines it as $$\text{RMW} \triangleq \forall a \in H\vert_{wr}, \forall b \in H\vert_{rd}: a \to^{so} b \implies a \to^{vis} b \triangleq so\vert_{wr \to rd} \subseteq vis$$ where $wr$ and $rd$ denote the set of write operations and read operations, respectively.

However, I think these two definitions too weak to ensure the reads read from the last write, because they have specified only the visibility relation but not the arbitration relation. Without the arbitration order between the previous writes, a read may read from a stale write. Therefore, I think the definition for RMW should contain $so|_{wr} \subseteq ar$.

My questions are:

  1. Are the two definitions for RMW correct? If not, what should it be?

  2. More generally, what is the relationship between visibility and arbitration? Is it always required that $vis \subseteq ar$? If not, what are the consistency models that do not need $vis \subseteq ar$?

Related Post: Confusion about a formal definition of PRAM consistency



Your Answer

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