这篇文章讨论了Chandy-Lamport协议。这篇文章由Federico Ponzi于2024年5月30日发布，并在2024年6月3日进行了最后更新。文章内容涵盖了分布式快照试图解决的问题、它的应用场景、系统模型、全局状态检测算法、快照一致性的定义、快照收集方法、实现该算法的系统、TLA+规范以及结论和参考文献。
关键点
- 进程在收到第一个标记消息时记录其本地状态。
- 进程开始记录来自通道的传入消息，直到在该通道上收到标记。
- 记录的消息必须满足两个一致性条件才能形成有效的全局快照：
- 如果记录消息为已接收，则也会记录发送事件。
- 如果某个进程记录了消息发送事件，则该消息不会被记录为被其他进程接收。
1985年，当Alfrey-Lamport的分布式快照论文首次发表时，一些形式的分布式快照已经存在了一段时间。Lamport认为该协议是Lamport时钟基本思想的直接应用。除了回顾这篇论文，在这篇文章中，我还将展示一些真实的实现示例和协议的TLA+规范。
试图解决什么问题？
您需要记录程序的全局状态。为什么？因为，例如，你有一些复杂的计算正在进行中，你想知道已经到了哪一步。或者您有一个长时间运行的计算，并且您希望拍摄快照作为备份，以便在任何机器出现故障时从检查点重新启动计算，而不是从头开始。
对于程序的状态，我们引用局部变量，通常引用程序所经历的状态历史。
为什么拍快照很难？首先，快照算法不应该干扰正在运行的计算。
其次，如果你的程序是一台机器上的一个进程，这很简单！您可以创建一个API来表示“在5秒内记录快照”或“每2小时”。对于在单机上运行的多线程/多进程程序，可以创建类似的API。
在分布式系统中，这个API不能工作，因为没有全局共享时钟。您可能最终会得到不同步的快照，从而提供不一致的系统视图。除了进程本身的状态之外，我们还可以在快照中包含动态消息。作为不一致快照的示例，进程B可以记录它从A接收到消息，而A的快照不包括该消息被发送到B。
这张纸有一个很好的视觉表现：想象你想拍一张充满候鸟的天空的照片。一张照片是不够的，你需要拍摄多张照片，并以一种提供一致景观的方式将它们拼接在一起。这就是本文试图解决的问题。
我们能用它做什么？
更一般地，我们可以使用这样的全局状态检测算法来验证稳定性属性。稳定性是单调的，如果它们现在保持不变，它们将永远保持不变。例如，像“计算是否到达第n步”或“是否存在死锁”这样的属性。
系统模型
系统由一组进程组成，这些进程之间使用通道进行通信任何进程都有一个通往其他进程的“逻辑”通道。
假设通道：
- 有无限的缓冲区，
- 没有错误，
- 具有有限的递送延迟，
- 按发送顺序（FIFO顺序）发送消息。
全局状态检测算法
执行是分散的，即，没有协调快照的“主”进程，并且可以由任何进程启动。同样重要的是要注意，即使两个进程在彼此不知道的情况下同时启动快照协议，算法也是正确的。
所提供的解决方案旨在仅解决此问题一次（拍摄一个快照）-将其扩展到多次运行应该是微不足道的。
该算法的工作原理是通过通道发送称为“标记消息”的特殊消息。进程的行为会有所不同，具体取决于它们之前是否收到过标记消息。这些标记消息是算法的一部分，而不是底层计算的一部分-它们不会出现在快照本身中。本质上，当进程通过通道接收到第一个标记消息时，它将记录自己的状态并开始记录来自所有通道的传入消息。它将停止记录传入的消息从一个通道，只要它收到一个标记消息通过那里。
Chandy-Lamport 分布式快照算法使用标记消息来记录跨进程的一致全局状态，而不会中断底层计算。标记消息的工作原理如下：
- 任何进程都可以通过记录自己的状态并在其每个传出通道上发送标记消息来启动快照。
- 当进程第一次收到标记消息时：
- 它记录其本地状态。
- 它将标记到达的传入通道的状态记录为空。
- 它向所有传出通道（标记到达的通道除外）发送标记消息。
- 如果进程在记录其状态之后但在接收所有传入通道上的标记之前接收到常规消息，它会将该消息记录为相应传入通道状态的一部分。
- 一旦进程在其所有传入通道上都收到标记，它就完成了记录其本地快照。
关键点是：
- 标记消息在系统中传播，导致进程记录其本地状态。
- 在通道上的标记之前收到的消息被记录为该通道快照状态的一部分。
- 在通道上的标记之后收到的消息不属于快照的一部分。
该算法保证记录的全局快照遵循一致的切割规则，不会干扰进程的正常执行。
如果在 Chandy-Lamport 分布式快照算法中标记消息延迟，则不会影响记录的全局快照的正确性。这是因为该算法依赖于进程间通信通道的 FIFO（先进先出）排序特性。
当标记消息延迟时会发生以下情况：
- 当一个进程启动快照算法时，它会记录其本地状态并在其所有传出通道上发送标记消息。
- 如果标记消息在通道上延迟，则常规应用程序消息可能会在延迟标记之前到达接收进程。
- 接收过程将记录延迟标记之前到达的所有应用程序消息作为快照传入通道状态的一部分。
- 一旦延迟标记最终到达，接收过程就会根据算法规则停止在该通道上记录消息。
- 延迟标记不会违反一致的全局快照属性，因为：
- 任何记录为已接收的消息都意味着其发送事件也被记录（由于 FIFO 排序）。
- 记录的任何发送事件都意味着该消息不能被记录为被其他人接收（由于 FIFO 排序）。
因此，虽然延迟标记可能会导致在特定通道的状态上记录更多消息，但它不会破坏全局快照的一致性规则。
FIFO 排序可确保尽管存在延迟，消息仍能以正确的顺序记录。关键点在于，得益于 FIFO 通道假设，Chandy-Lamport 算法可以容忍标记消息传播中的任意延迟，并且仍然可以捕获一致的全局快照。
实现此算法的系统
这些系统已经实现了分布式快照并在其操作中使用它。
Hazelcast Jet是一个分布式流处理器，它使用分布式快照来实现分布式计算的容错。
每隔一段时间，Jet就会升起一个全球标志，上面写着“是时候再拍一张快照了”。属于源顶点的所有处理器观察该标志，保存它们的状态，向下游处理器发出屏障项并恢复处理。
资料来源：官方文件，文件。
Apache Flink是一个流处理框架，它以两种方式使用分布式快照：
首先，它被用作全局状态的常规备份的检查点。当应用程序失败时，它用于恢复。其次，它用于死锁检测。当前程序在快照后继续运行。然后，分析快照以查看应用程序中是否存在死锁状态。如果是，将进行相应的处理。
在Flink中，在快照协议结束时，快照收集器（中央服务器）开始收集快照，以形成全局一致性快照。
TLA+规范
提供了 TLA+ 规范，用于正式建模和验证协议的正确性。
可以在GitHub上查看。
结论
在这篇文章中，我回顾了Alfrey-Lamport分布式快照协议论文，并介绍了我为它编写的TLA+规范。这篇论文概括了为解决特定实例（如终止检测）而编写的更具体的算法。稳定性属性概括了诸如“此计算是否已终止”或“此计算是否处于死锁状态”之类的属性。
在分布式系统中拍摄全局快照是很困难的，因为缺乏共享时钟，打个比方，这就像试图以一致的方式拼接天空的多张照片。
分布式快照是一种在分布式系统中记录程序全局状态的技术。它对于故障恢复、系统备份或检测稳定性属性等场景非常有用。Chandy-Lamport协议利用特殊的标记消息在没有全局共享时钟的分布式系统中实现快照，确保了快照的一致性。