Arbitration-Free Consistency is Available (and Vice Versa)

TL;DR

The paper provides a unified semantic framework for distributed storage where object semantics and consistency models are expressed as storage specifications. It proves the Arbitration-Free Consistency theorem ($AFC$): a storage specification has an available implementation if and only if its consistency model is arbitration-free with respect to the operation specification, unifying prior results about coordination-free versus synchronized behavior. The authors develop an expressive model of storage executions based on histories and abstract executions, define basic and generalized operation specifications, and show how arbitration-freeness constrains the need for a total arbitration order. They also provide a constructive route: when arbitration-free, CC serves as the strongest available model, with explicit LTS-based implementations that ensure availability; when not arbitration-free, no available implementation exists. Overall, the work generalizes CAP-like and related results beyond simple read/write interfaces to broad object semantics and multi-object operations, clarifying the fundamental role of arbitration-order coordination in distributed storage systems.

Abstract

The fundamental tension between availability and consistency shapes the design of distributed storage systems. Classical results capture extreme points of this trade-off: the CAP theorem shows that strong models like linearizability preclude availability under partitions, while weak models like causal consistency remain implementable without coordination. These theorems apply to simple read-write interfaces, leaving open a precise explanation of the combinations of object semantics and consistency models that admit available implementations. This paper develops a general semantic framework in which storage specifications combine operation semantics and consistency models. The framework encompasses a broad range of objects (key-value stores, counters, sets, CRDTs, and transactional databases) and consistency models (from causal consistency and sequential consistency to snapshot isolation and transactional and non-transactional SQL). Within this framework, we prove the Arbitration-Free Consistency (AFC) theorem, showing that an object specification within a consistency model admits an available implementation if and only if it is arbitration-free, that is, it does not require a total arbitration order to resolve visibility or read dependencies. The AFC theorem unifies and generalizes previous results, revealing arbitration-freedom as the fundamental property that delineates coordination-free consistency from inherently synchronized behavior.

Figures (4)

• Figure 1: Different litmus programs with two concurrent sessions showing the absence of available implementations for selected pairs of consistency models and operation specifications.
• Figure 2: Two examples of histories for $\mathsf{faacas}$. Arrows represent $\soSoul$ and $\textcolor{wrColor}{\mathsf{wr}}$ relations. The initial event $\textup{init}$ defines the initial state where $x$ is $0$. Events $e_0$ and $e_1$ execute a fetch-and-add and compare-and-swap respectively, at different replicas.
• Figure 3: Abstract executions of the histories from \ref{['fig:example-history-faa']}. Arrows represent $\textcolor{arColor}{\mathsf{ar}}$ and $\textcolor{rbColor}{\mathsf{rb}}$ relations. For readability, we omit the $\soSoul$ and $\textcolor{wrColor}{\mathsf{wr}}$ relations. The event $e_0$ is received-before executing $e_1$ in \ref{['fig:example-exec-faa:sc']} but not in \ref{['fig:example-exec-faa:no-sc']}. The arbitration relation is the same in both executions.
• Figure 4: Visibility formulasrelations defining the homonymous consistency models Return-Value Consistency ($\textup{RVC}$, \ref{['fig:rvc']}), Causal Consistency ($\textup{CC}$, \ref{['fig:cc']}), Prefix Consistency ($\textup{PC}$, \ref{['fig:prefix']}) and Sequential Consistency/Serializability ($\textup{SC} / \textup{SER}$, \ref{['fig:ser']}). Solid edges describe the dependencies linking $\varepsilon_0$ and $\varepsilon_1$. We include the $\textcolor{wrColor}{\mathsf{wr}}_x$ edge (and its source $e$) as a visualization of the constraint $\textcolor{wrColor}{\mathsf{wr}}_x^{-1}(\varepsilon_1) \neq \emptyset$. Dashed $\textcolor{arColor}{\mathsf{ar}}$ edges are not part of the visibility formulasrelations. These capture the Last-Writer-Wins conflict resolution policy discussed later, requiring that the event $e$ being read succeeds all other events from the context in $\textcolor{arColor}{\mathsf{ar}}$.

Theorems & Definitions (13)

• Example 3.1
• Definition 3.2
• Example 3.3
• Definition 3.4
• Example 3.5
• Definition 4.1
• Definition 4.2
• Example 4.3
• Definition 5.1
• Definition 6.1