Consistency models with global operation sequencing and their composition (extended version)

TL;DR

This paper introduces a unified consistency model called Global Sequence Consistency (GSC) that encompasses various weaker consistency models, analyzes their composition, and explores their indistinguishability under certain conditions.

Contribution

The paper defines GSC, a unified model for weaker consistency guarantees, and proves key properties including composability and indistinguishability among models like TSO and dual TSO.

Findings

GSC unifies several weaker consistency models.

Objects satisfying GSC can be composed under certain conditions.

Clients cannot distinguish between GSC, TSO, and dual TSO without out-of-band communication.

Abstract

Modern distributed systems often achieve availability and scalability by providing consistency guarantees about the data they manage weaker than linearizability. We consider a class of such consistency models that, despite this weakening, guarantee that clients eventually agree on a global sequence of operations, while seeing a subsequence of this final sequence at any given point of time. Examples of such models include the classical Total Store Order (TSO) and recently proposed dual TSO, Global Sequence Protocol (GSP) and Ordered Sequential Consistency. We define a unified model, called Global Sequence Consistency (GSC), that has the above models as its special cases, and investigate its key properties. First, we propose a condition under which multiple objects each satisfying GSC can be composed so that the whole set of objects satisfies GSC. Second, we prove an interesting relationship between special cases of GSC---GSP, TSO and dual TSO: we show that clients that do not communicate out-of-band cannot tell the difference between these models. To obtain these results, we propose a novel axiomatic specification of GSC and prove its equivalence to the operational definition of the model.