“本页不覆盖恶意快照、永久介质损坏、跨版本不兼容序列化或把未记录的随机/外部输入重放出来；这些必须另有验证和迁移协议。全局通道快照记录分布式一致割，本页只是同一复制状态机前缀的压缩恢复，两者不…”
形式陈述
经典 Chandy–Lamport 算法运行在有限消息传递系统上。每条有向通道可靠、FIFO，发送的消息最终且恰好一次到达。这里按经典模型取无界缓冲，发送不因通道容量阻塞；有界缓冲实现须另证包括 marker 在内的每次发送都不会向已满缓冲追加消息。快照期间进程不崩溃，所有需记录的进程都可从发起者沿通信图到达。记录本地状态与发送 marker 相对本地应用事件是原子的。算法不暂停应用消息，只要求每个 marker 带有快照标识，使并发快照不会混淆。
对一次快照，发起者
- 记录自己的本地状态；
- 在发送任何后续应用消息之前，向每条出通道发送一个 marker；
- 从此记录每条入通道上收到的应用消息，直到该通道的 marker 到达。
尚未记录本地状态的进程
算法输出所有进程记录的局部状态，以及每条通道记录的消息序列。正确性包含三项独立证明义务。
- 唯一记录：发起者或首次 marker 只触发一次本地记录；每条入通道在其唯一 marker 到达时关闭一次记录区间，所以每个局部状态和通道状态恰记录一次。
- 一致性：若某应用消息的接收被纳入进程局部前缀，其发送也必在发送者前缀内；而发送已纳入、接收尚未纳入的消息，恰被记录为在途消息。因此结果对应一个一致切片。
- 终止性：在有限、可达的通信图中，每个首次收到 marker 的进程都会向所有出边继续传播；可靠最终交付和无崩溃保证每个进程最终记录本地状态、每条通道最终收到 marker 并停止记录。
一致性论证的关键正是 FIFO。发送者记录状态后会先发 marker，再发任何快照后的应用消息；同一通道上 marker 必先到达，接收者会在可能接收这类应用消息前记录自己的状态。于是不存在“发送在切片外、接收却在切片内”的消息。发送在切片内而尚未接收的消息，则位于发送与 marker 之间，接收方会把它收入通道状态。
一次快照在每条有向通道上恰发送一个 marker，因此控制消息数为
直觉
marker 像沿每条 FIFO 河道漂下的分界浮标。浮标之前发送的应用消息属于快照前，之后发送的属于快照后。不同进程看到浮标的时刻可以相差很远；算法依靠每条通道的顺序，把这些局部边界拼成一条不会越过因果关系的弯曲切线。
进程不需要停机等全局口令。先看到 marker 的进程照常处理业务，只是在其他入通道的 marker 到达前，把收到的消息抄进该通道的快照记录。这样既保留运行并发，也补上仅记录本地内存会漏掉的在途状态。
例子与边界
账户服务 P 已从源账户扣除转账 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，再发快照后的应用消息
消息丢失会让某条通道永远等不到 marker，进程崩溃也可能截断传播和状态上报；经典终止证明不覆盖这些执行。系统若要在故障中取快照，需要重传、稳定存储、成员视图或容错快照协议，并重新说明得到的是哪些正确进程的状态。
推论与应用
快照结果是与实际执行相容的一个可能全局状态，不保证现实中存在某个物理瞬间，所有记录值恰好同时成立。一致切片提供正确性对象，marker 算法只负责在局部观察下构造它；把二者分开，才能清楚看出哪些结论来自因果闭包，哪些来自 FIFO 与可靠交付。
共享内存的原子快照则要求扫描与数组更新共同线性一致，返回扫描调用区间内某个位置的向量。它不记录在途消息，也不以任意因果一致切片为返回规格；同名的“快照”不能替代对这两种目标的区分。
分布式检查点、稳定性质检测、调试、垃圾回收和死锁检测都可消费这种一致状态。终止检测给出具体的稳定谓词：全体节点被动，且基本信道为空；没有外部激活时，这一事实在后续执行中保持。非稳定谓词则不同：某个可能全局状态满足它，不一定说明记录完成时仍成立。
也可随计算维护较小的完成摘要：Dijkstra–Scholten保留未清回执与动态父树，信用分配把责任作为精确份额随任务传递，Safra通过计数和染色取得可信巡回。它们各有独立不变量，并非把完整快照结果换一个名字。
参考资料
- 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。