Monotonic Prefix Consistency in Distributed Systems

Abstract

We study the issue of data consistency in distributed systems. Specifically, we consider a distributed system that replicates its data at multiple sites, which is prone to partitions, and which is assumed to be available (in the sense that queries are always eventually answered). In such a setting, strong consistency, where all replicas of the system apply synchronously every operation, is not possible to implement. However, many weaker consistency criteria that allow a greater number of behaviors than strong consistency, are implementable in available distributed systems.

We focus on determining the strongest consistency criterion that can be implemented in a convergent and available distributed system that tolerates partitions. We focus on objects where the set of operations can be split into updates and queries. We show that no criterion stronger than Monotonic Prefix Consistency (MPC) can be implemented.

Appendices

A Proof of Feasibility of MPC

Proposition 1. Let $\mathcal {I}$ be the implementation of Fig. 2. Then $\mathcal {I}\preceq \texttt {MPC}$.

Proof

Let , we establish an inductive invariant that holds for every finite prefix $e'$ of e. Let A be the set of action identifiers of $e'$. Let $\ell \in \mathbb {N}^*$ be the sequence of values that appear in a broadcast message $\texttt {Apply}$ from Site 1, in the order they appear in $e'$.

Let $\mathbb {P}$ be the set of process identifiers. For each site $\textit{pid}\in \mathbb {P}$, consider the unique run r for the projection $e'|_{\textit{pid}}$, and let $\ell _\textit{pid}\in \mathbb {N}^*$ be the sequence maintained in the local state of Site $\textit{pid}$ at the end of the run r.

Let $t' = \mathsf{tr}({e'})$ be the trace of $e'$, with $t' = (t_r,W)$.

Then, we have the following properties.

• 1. For every $\texttt {Apply}(d)$ message with $d \in \mathbb {N}$ that appears in $e'$ (from Site 1), we have $d \in W$.

• 2. For every $\texttt {Forwarded}(d)$ message with $d \in \mathbb {N}$ that appears in $e'$ (from Site i with $i > 1$), we have $d \in W$.

• 3. The elements of $\ell$ are in W.

• 4. For every $\textit{pid}\in \mathbb {P}$, $l_\textit{pid}\sqsubseteq \ell$.

• 5. For every query $(\_,\textit{pid},\mathtt{read}\ \ell ')$ in e with $\textit{pid}\in \mathbb {P}$, we have $\ell ' \sqsubseteq \ell _\textit{pid}$.

• 6. Consistency: For all $\textit{aid}\in A$, and for any element $d \in \mathbb {N}$ of $\textsf {label}(\textit{aid})$, we have $d \in W$.

• 7. Prefix: For any all $\textit{aid},\textit{aid}\,' \in A$, $\textsf {label}(\textit{aid}) \sqsubseteq \textsf {label}(\textit{aid}\,')$ or $\textsf {label}(\textit{aid}\,') \sqsubseteq \textsf {label}(\textit{aid})$.

• 8. Monotonicity: For all $\textit{aid},\textit{aid}\,' \in A$, if $\textit{aid}< \textit{aid}\,'$, then $\textsf {label}(\textit{aid}) \sqsubseteq \textsf {label}(\textit{aid}\,')$.

We can see that this invariant holds for the empty execution, and that any action that the implementation can take maintains it.

B Closure Properties of Implementations

Lemma 2 (Query Availability). Let $\mathcal {I}$ be an implementation. Let be a finite execution and $\textit{pid}\in \mathbb {P}$. Then, there exist $\textit{aid}\in \mathbb {N}$ and $\ell \in \mathbb {N}^*$ such that the execution $e' = e \cdot (\textit{aid},\textit{pid},\mathtt{read}(\ell ))$ belongs to .

Proof

Similar to the proof of Lemma 1, but using the query handler, instead of the update handler. This proof is also simpler, as there is no need to consider messages, since the query handler cannot broadcast any message. Therefore, in this proof, only case 1 needs to be considered.    $\square$

Lemma 3 (Invisible Reads). Let $\mathcal {I}$ be an implementation. Let be an execution (finite or infinite) of the form $e_1 \cdot (\textit{aid},\textit{pid},\mathtt{read}(\ell )) \cdot e_2$, where $\textit{aid}\in \mathbb {N}$, $\textit{pid}\in \mathbb {P}$ and $\ell \in \mathbb {N}^*$. Then, .

Proof

This is a direct consequence of Definition 5, which specifies that query actions do not modify the local state of sites, and do not broadcast messages.    $\square$

Lemma 4 (Limit). Let $\mathcal {I}$ be an implementation. Let $e_1\dots ,e_n,\dots$ be an infinite sequence of finite executions, such that for all $i \ge 1$, , $e_i \sqsubset e_{i+1}$, and such that for all $i \ge 1$, for all broadcast actions in $e_i$, and for all $\textit{pid}\in \mathbb {P}$, there exists $j \ge 1$ such that $e_j$ contains a corresponding receive action.

Then, the limit $e^\infty$ of $e_1\dots ,e_n,\dots$ belongs to .

Proof

According to Definition 6, we have three points to prove.

• (1) (Projection) First, we want to show that, for all $\textit{pid}\in \mathbb {P}$, the projection $e^\infty |_{\textit{pid}}$ follows $\mathcal {I}$. For all $i \ge 1$, we know that , and deduce that $e_i|_{\textit{pid}}$ follows $\mathcal {I}$. Let $r_i$ be the run of $e_i|_{\textit{pid}}$. Note that for all $i \ge 1$, we have $r_i \sqsubset r_{i+1}$. Let $r^\infty _\textit{pid}$ be the limit of the runs $r_1,\dots ,r_n,\dots$ By construction, $r^\infty _\textit{pid}$ is a run of $e^\infty |_{\textit{pid}}$, which shows that $e^\infty |_{\textit{pid}}$ follows $\mathcal {I}$.

• (2) (Causality) We need to prove that every receive action $\sigma$ in $e^\infty$ has a corresponding broadcast action $\sigma '$ that precedes it in $e^\infty$. Let $e_i$ be a prefix of $e^\infty$ that contains $\sigma$. Since , we know that there exists a broadcast action $\sigma '$ corresponding to $\sigma$, and that precedes $\sigma$ in $e_i$. Finally, since $e_i \sqsubset e^\infty$, $\sigma '$ precedes $\sigma$ in $e^\infty$.

• (3) (Fairness) We want to prove that for every broadcast action $\sigma$ of $e^\infty$ and for every site $\textit{pid}\in \mathbb {P}$, there exists a corresponding receive action $\sigma '$. Let $e_i$ be a prefix of $e^\infty$ that contains $\sigma$. By assumption of the current lemma, there exists $j \ge 1$ such that $e_j$ contains a receive action $\sigma '$ corresponding to $\sigma$. Moreover, since $e_j \sqsubset e^\infty$, $\sigma '$ belongs to $e^\infty$, which concludes our proof.

   $\square$