Conflict free replicated data types

《Conflict free replicated data types》 阅读笔记。

论文地址

1. 最终一致性

1.1. Eventual Consistency

一个分布式系统是最终一致的，需满足以下条件：

• Eventual delivery: 在健康节点上执行的更新操作最终会被传递至所有健康节点，也就是说 $f \in c_i \Rightarrow \lozenge f \in c_j, \forall i, j \in [1, \dots, n]$，其中 $c_i$ 是节点 $p_i$ 的 causal history
• Convergence: causal history 相同的健康节点最终会收敛至相同的状态，也就是说 $\square c_i = c_j \Rightarrow \lozenge \square s_i \equiv s_j, \forall i, j \in [1, \dots, n]$
• Termination: 所有操作会终止

在上述说明中，$\lozenge$ 表示 eventually，$\square$ 表示 always，详见 Temporal logic。至于 causal history，可以理解为该节点已执行操作的集合。

1.2. Strong Eventual Consistency

一个分布式系统是强最终一致的，需在满足最终一致的条件下，额外满足以下约束：

• Strong Convergence: 执行相同操作集合的健康节点具有相同的状态，也就是说 $c_i = c_j \Rightarrow s_i \equiv s_j, \forall i, j \in [1, \dots, n]$

PS: 最终一致性只包含 liveness guarantee，而强最终一致对系统的中间状态进行了约束 (safety guarantee)

2. 系统模型

2.1. 符号说明

2.2. State-based Convergent Replicated Data Type(CvRDT)

Causal History

我们定义一个对象的 causal hisatory(stated-based) 为 $\mathcal{C} = [c_1, \dots, c_n]$，其中 $c_i$ 经历了一系列中间态 $c_i^0, \dots, c_i^k, \dots$。初始时，$c_i^0 = \emptyset, \forall i \in [1, \dots, n]$，在节点 $p_i$ 上执行的 $k^{th}$ 操作分为以下三种情况：

$$c_i^k = \begin{cases}
c_i^{k-1}, & f = q \cr c_i^{k-1} \cup \{u_i^k(a)\}, & f = u_i^k(a) \cr c_i^{k-1} \cup c_{i'}^{k'}, & f = m_i^k(s_{i'}^{k'}) \end{cases}$$

Monotonic semilattice object

我们用 $(\mathcal{S}, \le, s^0, q, u, m)$ 表示基于状态的对象，其中 $\le$ 表示 partial order。若其满足以下约束，我们称其为 monotonic semilattice object:

1. Poset $(\mathcal{S}, \le)$ 构成一个 Join-semilattice
2. Merge 操作满足: $s \cdot m(s') = s \vee s'$
3. 在更新操作下状态 $s$ 满足单调性，即 $s \le s \cdot u$

回顾之前的知识，可以知道第 1 条约束的意思是集合 $\mathcal{S}$ 中任意非空子集都有 join，第 2 条约束说明 merge 即为 join。

CvRDT

Assuming eventual delivery and termination, any state-based object that satisfies the monotonic semilattice property is SEC.

CvRDT 使用 $(\mathcal{S}, \le, s^0, q, u, m)$ 表示。

从上可以看出，在 CvRDT 中， 需要满足以下条件：

• 状态满足单调性，消息最终可达
• 状态更改操作为 Merge 需满足交换律，结合律，幂等

2.3. Op-based Commutative Replicated Data Type(CmRDT)

Causal History

我们定义一个对象的 causal hisatory(op-based) 为 $\mathcal{C} = [c_1, \dots, c_n]$，其中 $c_i$ 经历了一系列中间态 $c_i^0, \dots, c_i^k, \dots$。初始时，$c_i^0 = \emptyset, \forall i \in [1, \dots, n]$，在节点 $p_i$ 上执行的 $k^{th}$ 操作分为以下两种情况：

$$c_i^k = \begin{cases}
c_i^{k-1}, & f = q, t \cr c_i^{k-1} \cup \{u_i^k(a)\}, & f = u_i^k(a) \end{cases}$$

Happened-before

Update $(t, u)$ happended-before $(t', u')$ iff the former is delivered when the latter executes: $(t, u) \rightarrow (t', u') \Leftrightarrow u \in c_j^{k-1}$, where $t'$ executeds at $p_j$ and $k = K_j(t')$.

Commutativity

Updates $(t, u)$ and $(t', u')$ commute, iff for any reachable replica state $s$ where both $u$ and $u'$ are enabled, $u$ (resp. $u'$) remains enabled in state $s \cdot u'$(resp. $s \cdot u$), and $s \cdot u \cdot u' \equiv s \cdot u' \cdot u$.

CmRDT

Assuming causal delivery of updates and method termination, any op-based object that satisfies the commutativity property for all concurrent updates, and whose delivery precondition is satisfied by causal delivery, is SEC.

CmRDT 使用 $(\mathcal{S}, s^0, q, t, u, \mathcal{P})$ 表示。

从上可以看出，在 CmRDT 中， 需要满足以下条件：

• Update 操作要么可确定明确的因果顺序，要么满足可交换
• 消息传输提供 exactly once 的保证

3. 一些结论

• CvRDTs and CmRDTs are equivalent
• SEC is incomparable to sequential consistency

4. CRDT 示例

4.1. Counters

我们使用 CvRDT 的框架来构造一个分布式计数器 $(\mathcal{S}, \le^n, s^0, value, inc, max^n)$:

可以发现上述定义的是一个只增计数器，如果想可增可减的话，可以使用两个只增计数器构成。

4.2. Set

一个 add-only 的集合可以构造为 $(\mathcal{S}, \subseteq, \emptyset, value, add(e), \cup)$，其中 $s \cdot add(e) = s \cup \{e\}$，很明显这也是一个 CRDT。

在 A comprehensive study of Convergent and Commutative Replicated Data Types 中作者定义了可增可减的两种 Set，但是也有较强的 assumption…

• 2P-Set：维护两个集合：add-only 和 remove-only。只能适用于集合中的元素只会被 add/remove 一次的情况
• U-Set: 维护一个支持 add/remove 的集合。需要满足两个条件:
  • remove 过的元素不会再 add
  • add 操作确保在 remove 前