Chandy–Lamport 分布式快照

形式陈述 ​

经典 Chandy–Lamport 算法运行在有限消息传递系统公理库消息传递系统Message-passing system进程仅通过发送和接收消息交互的分布式模型。上。每条有向通道可靠、FIFO，发送的消息最终且恰好一次到达；快照期间进程不崩溃，所有需记录的进程都可从发起者沿通信图到达。记录本地状态与发送 marker 相对本地应用事件是原子的。算法不暂停应用消息，只要求每个 marker 带有快照标识，使并发快照不会混淆。

对一次快照，发起者 $p$ 执行以下规则：

1. 记录自己的本地状态；
2. 在发送任何后续应用消息之前，向每条出通道发送一个 marker；
3. 从此记录每条入通道上收到的应用消息，直到该通道的 marker 到达。

尚未记录本地状态的进程 $q$ 首次从入通道 $c$ 收到该快照的 marker 时：先记录本地状态，把 $c$ 的通道状态记录为空；随后在发送任何后续应用消息前，向所有出通道发送 marker；最后开始记录其他每条入通道上的应用消息。已经记录本地状态的进程后来从入通道 $c^{\prime }$ 收到 marker 时，停止记录 $c^{\prime }$，此前“本地记录之后、该 marker 之前”从 $c^{\prime }$ 收到的应用消息就是该通道的快照状态。marker 是控制边界，不计入应用通道状态。

算法输出所有进程记录的局部状态，以及每条通道记录的消息序列。正确性包含三项独立证明义务。

• 唯一记录：发起者或首次 marker 只触发一次本地记录；每条入通道在其唯一 marker 到达时关闭一次记录区间，所以每个局部状态和通道状态恰记录一次。
• 一致性：若某应用消息的接收被纳入进程局部前缀，其发送也必在发送者前缀内；而发送已纳入、接收尚未纳入的消息，恰被记录为在途消息。因此结果对应一个一致切片公理库一致切片Consistent cut · Consistent global cut对事件因果前驱向下闭合、因而可解释为分布式全局状态的执行切片。。
• 终止性：在有限、可达的通信图中，每个首次收到 marker 的进程都会向所有出边继续传播；可靠最终交付和无崩溃保证每个进程最终记录本地状态、每条通道最终收到 marker 并停止记录。

一致性论证的关键正是 FIFO。发送者记录状态后会先发 marker，再发任何快照后的应用消息；同一通道上 marker 必先到达，接收者会在可能接收这类应用消息前记录自己的状态。于是不存在“发送在切片外、接收却在切片内”的消息。发送在切片内而尚未接收的消息，则位于发送与 marker 之间，接收方会把它收入通道状态。

直觉 ​

marker 像沿每条 FIFO 河道漂下的分界浮标。浮标之前发送的应用消息属于快照前，之后发送的属于快照后。不同进程看到浮标的时刻可以相差很远；算法依靠每条通道的顺序，把这些局部边界拼成一条不会越过因果关系的弯曲切线。

进程不需要停机等全局口令。先看到 marker 的进程照常处理业务，只是在其他入通道的 marker 到达前，把收到的消息抄进该通道的快照记录。这样既保留运行并发，也补上仅记录本地内存会漏掉的在途状态。

例子与边界 ​

账户服务 P 已从源账户扣除转账 $\tau$，并把 credit(τ) 发往账户服务 Q；Q 尚未收到时，P 发起快照。P 记录“源账户已扣款”，随后在出通道发送 marker。由于 credit(τ) 在 marker 前发送，FIFO 保证 Q 先收到转账消息。若 Q 在另一条入通道的 marker 触发下已经记录本地状态，它会把 credit(τ) 记入 P→Q 的通道状态，直到 P 的 marker 到达。快照的进程余额看似少了一笔，但加上在途转账后资金守恒。

若 Q 在收到 credit(τ) 后才首次收到 P 的 marker并记录本地状态，则转入金额已经体现在 Q 的局部状态，P→Q 通道记为空。两种快照都合法：一份把转账放在通道里，另一份把它放在接收方状态里；算法保证不会既遗漏，又不会同时算入两个位置。

非 FIFO 通道破坏这条推理。P 在记录后先发 marker，再发快照后的应用消息 $m$；若 $m$ 能越过 marker，Q 可能在记录本地状态前收到 $m$，于是快照包含接收却不包含发送，切片不一致。此时需要 Lai–Yang 等通过消息着色或额外元数据识别边界的变体，不能直接宣称经典规则仍正确。

消息丢失会让某条通道永远等不到 marker，进程崩溃也可能截断传播和状态上报；经典终止证明不覆盖这些执行。系统若要在故障中取快照，需要重传、稳定存储、成员视图或容错快照协议，并重新说明得到的是哪些正确进程的状态。

推论与应用 ​

快照结果是与实际执行相容的一个可能全局状态，不保证现实中存在某个物理瞬间，所有记录值恰好同时成立。一致切片公理库一致切片Consistent cut · Consistent global cut对事件因果前驱向下闭合、因而可解释为分布式全局状态的执行切片。提供正确性对象，marker 算法只负责在局部观察下构造它；把二者分开，才能清楚看出哪些结论来自因果闭包，哪些来自 FIFO 与可靠交付。

分布式检查点、稳定性质检测、调试、垃圾回收和死锁检测都可消费这种一致状态。对非稳定谓词还要谨慎：快照证明某个可能全局状态满足谓词，不一定说明谓词在记录完成时仍成立；应用必须结合谓词的稳定性和后续执行语义解释结果。

参考资料

• K. Mani Chandy and Leslie Lamport, “Distributed Snapshots: Determining Global States of Distributed Systems,” ACM Transactions on Computer Systems 3(1), 1985, pp. 63–75。
• Ajay D. Kshemkalyani and Mukesh Singhal, Distributed Computing: Principles, Algorithms, and Systems, Cambridge University Press, 2008，distributed snapshots chapter。
• Ten H. Lai and Tao H. Yang, “On Distributed Snapshots,” Information Processing Letters 25(3), 1987, pp. 153–158。