一致切片 | Codeboy's Blog

形式陈述

设一次分布式执行的事件集合为 $E$ ，其happens-before 严格关系为 $\to$ 。切片是从每个进程的局部事件序列取一个有限前缀后得到的事件集合 $C\subseteq E$ ；前缀可以为空，此时对应该进程的初始局部状态。 $C$ 称为一致切片，当且仅当它对因果前驱向下闭合：

\forall e\in C,\ \forall e'\in E, \qquad e'\to e\Longrightarrow e'\in C.

换言之， $C$ 是 happens-before 偏序中的 order ideal。切片的 frontier 可由各非空前缀的最后一个局部事件表示；这些事件一般处于不同物理时刻，也可能彼此不可比。对有限执行，任一一致切片都可扩展为某个保持因果序的全序，使 $C$ 恰好成为该线性扩展的前缀，因此它可解释为一次合法观察中的全局边界，而不需要全局同时钟。

对消息 $m$ ，令 $s_m$ 与 $r_m$ 分别为发送和接收事件。由于 $s_m\to r_m$ ，一致性立即推出

r_m\in C\Longrightarrow s_m\in C.

反向蕴含并不成立： $s_m\in C$ 而 $r_m\notin C$ 完全合法，此时 $m$ 属于切片所对应的通道状态，是边界上正在传输的消息。由每个进程在其前缀末端的局部状态，再加上所有“发送已在切片内、接收尚在切片外”的消息，就得到相应分布式配置。

一致切片是数学对象，不指定怎样在线收集它。快照算法需要在只有局部观察的条件下记录局部状态和通道状态，并证明结果满足上述闭包；可靠信道、FIFO、marker 与故障假设属于具体算法，而不是 consistent cut 定义的一部分。

直觉

切片像用一条弯曲的线横穿多条进程时间轴。线不必垂直，也不代表同一墙上时刻；它只需保证线左边如果已经记录了一个结果，就不能把造成该结果的原因留在线右边。因果原因必须随结果一同纳入，尚未到达的消息则可以横跨边界，作为在途状态存在。

这一视角解释了为何分布式全局状态可以一致，却无法由任何机器瞬时读取。每个局部片段在不同时间记录，只要组合后不制造“收到一条从未发送的消息”，整个切片仍对应某个合法因果前缀。

一致切片允许消息跨越边界，但不允许接收事件失去发送前驱 — 左图的发送在切片内、接收在切片外，消息 m 作为在途状态存在；右图包含接收却排除发送，违反因果前驱闭包。

例子与边界

进程 P 执行事件 $p_1$ 后发送消息 $m$ ，进程 Q 接收 $m$ 后执行 $q_2$ 。若切片包含 Q 的接收与 $q_2$ ，却不包含 P 的发送，则 $r_m\in C$ 而 $s_m\notin C$ ，违反向下闭合：记录里出现了没有原因的结果。把发送加入后，切片恢复一致。

另一条切片包含 P 的发送，却在 Q 接收之前截断。它仍一致，消息 $m$ 只是出现在通道状态中。要求“所有通道都为空”会错误排除这种合法快照；异步系统里消息跨越记录边界是常态，完整全局状态正需要把它保存下来。

若 P 在发送前先扣减本地账户，Q 接收后才增加另一账户，切在两事件之间时局部余额之和暂时少了一笔，但加上通道中的在途转账后总量不变。这个例子说明一致性并不保证每个只看进程局部状态的业务谓词都成立；谓词必须对完整配置——包括通道——求值。

推论与应用

一致切片把因果偏序与全局状态验证连接起来。稳定性质检测、分布式断点、死锁检测和垃圾回收都可在某个一致全局状态上判断；若输入切片不一致，检测器可能把尚在途的证据误判为丢失，或凭空观察到没有发送来源的消息。

所有一致切片按集合包含形成格结构，向下闭包则提供构造与审计的直接判据。具体快照协议的任务是从运行中得到其中一个切片，并说明终止条件；本页不把算法的 marker 规则、FIFO 假设或无故障条件混入抽象对象。

参考资料

K. Mani Chandy and Leslie Lamport, “Distributed Snapshots: Determining Global States of Distributed Systems,” ACM TOCS 3(1), 1985, pp. 63–75。
Friedemann Mattern, “Virtual Time and Global States of Distributed Systems,” Parallel and Distributed Algorithms, 1989, pp. 215–226。
Colin J. Fidge, “Timestamps in Message-Passing Systems That Preserve the Partial Ordering,” Australian Computer Science Communications 10(1), 1988, pp. 56–66。

形式陈述 ​

反向链接

形式陈述