Conflict free replicated data types 阅读笔记。


论文地址

最终一致性

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: 执行相同操作集合的健康节点最终会收敛至相同的状态,也就是说 $\square c_i = c_j \Rightarrow \lozenge \square s_i \equiv s_j, \forall i, j \in [1, \dots, n]$
  • Termination: 所有操作会终止

在上述说明中,$\lozenge$ 表示可能性,$\square$ 表示必然性,详见 Modal logicS5 modal logic。至于 causal history,可以简单理解为操作的集合。

Strong Eventual Consistency

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

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

系统模型

符号说明

符号 含义
$p_i$ process $i$
$s_i$ process $p_i$ has state $s_i \in \mathcal{S}$, called its payload
$s^0$ 初始状态
$q$ query
$t$ prepare-update
$u$ update
$m$ merge
$\mathcal{P}$ communication protocol
$f_i^k(a)$ 在节点 $p_i$ 上执行的 $k^{th}$ 操作, $f$ 是 $q$, $u$ 或 $m$, $a$ 是参数
$K_i(f)$ 在节点 $p_i$ 上操作 $f$ 执行的序数

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 \
c_i^{k-1} \cup {u_i^k(a)} & f = u_i^k(a) \
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 需满足交换律,结合律,幂等

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 \
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 的保证

一些结论

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

CRDT 示例

Counters

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

符号 含义
$\mathcal{S}$ 状态集合,其中 $s = \vec{v} = [v_1, \dots, v_n]$ 表示计数器的状态
$\le^n$ $\vec{v} \le^n \vec{v'} \Leftrightarrow v_i \le v'_i, \forall i \in [1, \dots, n]$
$s^0$ $[0, \dots, 0]$
$value$ $value(\vec{v}) = \sum_{i}v_i$
$inc$ 在节点 $p_i$ 上 $inc(\vec{v}) = \vec{v'}$,其中 $v'i = v_i + 1 \cdot \mathbb{I}{{j}}(i), \forall i \in [1, \dots, n]$
$max^n$ $s \cdot max^n(s') = [max(v_1, v'_1), \dots, max(v_n, v'_n)]$

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

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 前