复制描述数据存在哪里,一致性描述哪些观测是合法的。

学习目标

比较线性一致、顺序一致、因果一致与最终收敛;检查单寄存器历史,并区分它与事务隔离。

前置:因果与操作历史。

一个对象,多种约定

寄存器初值为 0。A 写 1 并收到成功,之后 B 读出 0。如果读在写完成后才开始,线性一致禁止这种历史:所有已完成操作必须能放进一个符合真实时间先后的合法顺序执行。与写重叠的读仍可能返回 0,因为可以把它的生效点放在写前。

A: write(1) ├──────┤ 成功
B:                         read() ├────┤ → 0
线性一致:不允许。顺序一致:可把 B 排在 A 前。

顺序一致保留每个客户端的程序顺序,不要求不同客户端间的真实时间先后。上例把 B 唯一的读排在 A 唯一的写前,可以满足这个更弱的约定。因果一致保留依赖,包括通过消息传递的观测;独立写不必在所有地方呈现同一个顺序。最终收敛承诺:更新停止且通信、合并能持续进行后,副本最终一致;它本身不给每次读取规定新鲜度时限。

这些是不同的约定,不是能替所有应用选答案的排行榜。要求后续请求立刻看见的配置更新,与离线协作草稿需求不同。还需定义冲突合并规则、故障假设和对象范围。

有复制不等于选好了一致性

异步复制可能暴露旧值。“问多数派”本身也不是完整的线性一致算法:版本顺序、读协议、回写和成员变更规则都很关键。本 Lab 用 etcd 的状态机复制作为具体实现,不使用“R + W > N 证明一切”的简化论证。

etcd 默认 KV 路径提供强顺序约定;显式指定 serializable 的读可以读取本地状态,可能落后于多数派。Watch 有独立的语义且通知可能延迟,不能悄悄把 Watch 流当作新鲜的线性一致读取。

单对象线性一致与多对象事务隔离回答不同问题。两次分别线性一致的读取不自动构成一次事务快照。需要抵抗并发更新的应用读改写,应使用原子比较更新或事务。

动手:比较两个模型

在检查台加载“旧值读”,先检查线性一致,再检查顺序一致。同一组已完成操作在前者失败,在后者通过。查看找到的顺序,不能只看绿色标签。把读改成 9:没有任何写产生过 9,因此两个模型都没有合法寄存器执行。

有界搜索依次探索满足前置关系的操作:写更新状态,读只在等于当前整数值时允许。它按“已选操作集合、寄存器值”记忆状态。穷尽全部合法顺序才报告失败;预算耗尽则报告未判定。这只检查输入历史在小模型中是否成立,不是对 etcd 或任意实现的正确性证明。

自测

搜索成功,能证明服务的所有执行都正确吗?

不能。它只为这段有限历史找到一个合法解释,没有检查其他操作、调度、对象与故障。

多数派读是否总能读到最新值?

缺少完整协议时不能保证。Quorum 相交是构件,它不单独定义版本、不解决并发写,也不防止过期 Leader。

原始资料