分布式终止检测

“没看到工作”与“工作不存在”的差别，藏在发送和接收之间。发送者已经把任务移出自己的队列，接收者还没把它放入队列；这时两个本地队列都空，任务却仍在网络中。

终止谓词在上述模型中是稳定的。一旦所有进程被动且没有基本消息，就不存在能激活任何进程的下一步基本事件。控制协议还可继续传消息，但不会创造新任务。因此完成证明可以稍晚送达，结论不会在送达途中失效。

稳定性不是“进程从此完全不运行”。节点可能继续处理检测回执、返回统计结果，甚至开始另一个明确分隔的计算。被证明终止的是当前基本计算及其任务范围。

同样的两个空队列，两种不同结论 ​

A最初持有一个任务，准备把它交给B。按如下顺序执行：

第三行不是终止，第五行才是。若只保留两个进程的active/passive标记，两行完全相同；丢掉信道状态也就丢掉了区分答案所需的信息。

逐个询问“你现在空闲吗”还会遇到采样时间错位。观察者先问到B被动；随后A把任务发给B，B活动起来；观察者再问到A已经被动。两份报告都真实，却不对应一个全体被动且信道为空的可信全局状态。给每份报告加本地时钟，并不会自动修复这种拼接。

一致快照怎样成为检测器 ​

可以用一致切片公理库一致切片Consistent cut · Consistent global cut对事件因果前驱向下闭合、因而可解释为分布式全局状态的执行切片。同时表示进程状态与跨切片的在途消息，然后检查Term。若选用Chandy–Lamport快照公理库Chandy–Lamport 分布式快照Chandy-Lamport snapshot · Distributed snapshot algorithm在可靠 FIFO 通道上用 marker 并行记录一致进程状态与在途消息的分布式快照算法。，必须额外满足它的可靠FIFO等条件；本页不把这些条件加到所有终止检测方法上。

一份一致快照若满足Term，表示把独立事件作合法重排后，执行能到达这个终止配置。快照包含的本地前缀都已经发生，其后只剩尚未纳入的事件。稳定性保证这些后继事件不能重新制造基本工作，因此快照收集完成时可以宣布终止。反之，一份不满足Term的快照只说明这次记录没有证明完成，不能推出系统此刻仍有工作。

为保证最终检测，可在上一轮快照完成后继续启动新一轮，直到某轮满足Term。基本计算实际结束后，最终会有一次快照的全部记录发生在结束之后，得到全被动、基本信道空的结果。一次过早的快照没有这项保证。

模型改动会改变什么 ​

若允许用户在任意时刻注入新任务，Term就不再稳定。服务仍可检测“编号e这一批工作已结束”，但须把入口关闭、批次身份与消息归属纳入协议；不能把某一刻队列空称为永久完成。

若允许进程崩溃，未归还的任务可能永久消失，也可能在恢复后重新出现。仅用等待时间无法在纯异步网络中分辨迟到与丢失，必须重新规定故障下“完成”的含义及可用故障信息。控制消息同样不能悄悄假设为比基本消息更可靠。

不同检测器用不同的摘要替代全局快照。Dijkstra–Scholten公理库Dijkstra–Scholten 终止检测Dijkstra–Scholten algorithm · Diffusing computation termination为单源扩散计算维护未清回执与动态父树，使根的被动和零欠账同时排除活动后代与在途任务。把未完成工作挂在动态父树与未清回执上；信用分配公理库信用分配终止检测Credit distribution termination detection · Weight-throwing termination detection让每份活动工作与在途消息携带正信用，以精确总量守恒判定何时全部责任已归还根。保持总量守恒；Safra公理库Safra 终止检测Safra termination detection · Safra token algorithm用累计消息差额、接收染黑与被动转发构造可信令牌巡回，避免把不同时刻的零计数误当成终止。用令牌累计消息差额，并检查采样是否受到重新激活干扰。

在本页无故障、可靠恰好一次交付且任务入口关闭的范围内，三者分别给出检测实现，但还各有输入条件：Dijkstra–Scholten 要求单根激活、反向 ACK 路径与完整的发送欠账；信用分配要求单根初始信用、精确守恒和通往根的归还路径；这里的 Safra 版本允许多个初始活动节点，但要求固定成员、覆盖全体的逻辑环及配套计数染色。它们检测的是已经声明的基本工作，不能替应用决定哪些回调或外部请求算作工作。

这些机制适合搜索、工作池、分布式不动点计算等任务。应用时先规定什么事件算发出任务、什么状态算真正被动，再选择检测控制层。如果某节点的异步回调仍可能派生任务，却提前被标为passive，再正确的控制算法也只能证明一个错误抽象。

单元终点将任务发送、在途记录、回执与最终宣布放入同一张账表；验收首先检查是否有任何未纳入模型的工作来源。