Safra 终止检测

任何真实全局时刻都有

发送贡献+1，接收贡献−1。但令牌不是同时读取所有c[i]，它得到的是多个时刻的拼接。一条消息可能只计到接收的−1，却漏掉发送的+1，导致错误抵消。

黑色记录这种拼接需要重新检查。节点只要收到基本消息就染黑，不试图用猜测判断它是否危险；下一次交令牌时把黑色一起交出去。宁可多巡回一轮，也不把一个未经保证的零值当成全局信道为空。

零计数却仍有活动节点 ​

用A、B、C组成逻辑环，A为0。初始只有C活动，三处c=0且都白。固定以下执行：

若只检查每次转发者被动、最后s=0，就会误报。m的发送被C计入，接收发生在B本轮采样之后而未被计入；n恰好相反。两个不匹配项抵消成0，B却仍有工作。C接收n时染黑，打断了错误结论。

A启动第二轮。令牌到B后等待；B做完才转发，其尚未清掉的黑色又会让第二轮失败。第三轮没有新基本消息，三节点都白，累计计数总和0，A宣布。多一轮来自保守颜色，并不违反最终检测。

白色如何恢复一致切片 ​

每个节点在本轮交令牌时被采样，根在令牌返回时采样。由这些本地前缀形成一个候选切片。若它包含某条基本消息的接收却不包含发送，则该消息是在发送者本轮采样后发出、在接收者本轮采样前收到。

这次接收必发生在接收者上一轮采样之后：上一轮采样先于本轮发起，而这里的发送已经晚于本轮某次采样。第一轮可把初始化作为前一边界。于是接收者在本轮采样时必把黑色交给令牌；根上的接收则由black[0]直接检查。因此白色返回排除了所有这类因果倒置，得到一个一致切片公理库一致切片Consistent cut · Consistent global cut对事件因果前驱向下闭合、因而可解释为分布式全局状态的执行切片。。

在这个一致切片上，s等于“发送已在切片内、接收尚在切片外”的消息数，非负且不会出现漏发多收的抵消。所有被采样节点又都是passive，所以s=0证明切片满足终止谓词；利用稳定性，完成检查时也已终止。这个记账不变量公理库不变式与归纳不变式Invariant · Inductive invariant · Strengthened invariant区分所有可达状态上成立的性质与由初始性和一步闭包直接证明的归纳不变式。说明颜色不是装饰，计数也不能单独承担全部正确性。

最终检测与初始化 ​

基本计算终止后，各c[i]不再变化，和为0；所有节点都能转发令牌，黑色也不再产生。一次完整巡回会清掉各节点遗留的黑色，再下一次完整白色巡回即可宣布。这里按终止后开始的完整巡回计数，不能把终止时已在途的半圈算成覆盖全体的一圈。

初始A被动、c[A]=0也不能直接宣布：C可能从初始状态就活动，只是尚未发消息。代码要求先巡遍全环，正是为了覆盖分散的初始活动。

每轮令牌经过n条逻辑环边，控制开销为O(n)，每次基本消息只引起常数次本地计数和染色。若逻辑邻接由多跳路由实现，应按实际路径计包数；若基本算法长期运行，巡回次数没有只由n决定的上界。

计数必须容纳累计发送/接收数，不允许溢出回绕。M条基本消息下，单个计数绝对值至多M，令牌中间和可用 $O(\log (nM+1))$ 位表示。每个节点只需常数个计数/颜色字段，但位数并非常数。

本页不处理令牌丢失、节点崩溃或动态成员。Safra有优化和容错变体，可能改变染色时机、序号、检测节点与计数重置；移植其中一条规则前，应重新核对整套一致切片证明，不能按名称拼装。