目录一致性与异步权限交接

三种等待，各自排除一种风险 ​

InvAck 回答“旧读者已经失效了吗”。等待集合最初是实际应撤销的缓存身份集合，每份确认只删除对应成员。只看收到了几条任意消息不够；消息的事务身份、发送者和种类都必须匹配。

Data 回答“最后一个写者留下的值在哪里”。旧 M 收到转发请求之前仍可本地写，所以 home 不能使用请求发出时的旧内存值。旧 owner 在处理 Fwd 的那一步捕获当时最新值，并同时失去写权；从这以后没有写者能再改掉正在交接的那份数据。

Installed 回答“下一次转发能否由新持有者处理”。即便 home 已经发出 Grant，网络仍可能把它延迟。等安装确认回来后再启动后继事务，就不会向一个尚为 I 的目标转发 owner 请求。这多一次确认的成本，换来更小的瞬态状态空间。

一次升级途中，又收到撤销 ​

A、B 都持有 S(0)，C 申请写10。home 先处理 C，于是向 A、B 发 Inv。A 随后也申请写20，它的 GetM 排在 C 后面。此时 A 不能因为“我已经申请升级”而拒绝 C 的撤销。

先让 Inv 到 A，再让 A 的 InvAck 回 home。A 变 I，但写20的 pending 还在；home 的等待集合只剩 B。此时 B 仍可本地读0，这完全合法，因为 C 尚未获得 M，也尚未完成写10。

当 B 也失效并确认后，C 才收到 GrantM，安装并写10。C 可以在 Installed 尚未回到 home 时再本地写11；home 仍不能开始 A 的请求。随后 A 的 GetM 被处理，FwdM 让 C 把11交回、变 I。A 收到11后获得 M，再完成自己的写20。

A 的旧 S 副本早已失效，所以这次授权必须有完整数据。实际写把整 word 改成20，容易掩盖一次错误的旧值传输；参考器额外在执行写之前检查授权数据确实是当前块，不能只看写后的最终值。

从0到20的完整账本 ​

先让 A、B 各读一次0，等待各自事务完全结束，得到两个 S(0)。每次读有 GetS、GrantS、Installed 三条消息。之后按上一节让 C 的 GetM 先抵达，再让 A 的 GetM 排队。B 失效之后也发 GetS，排在 A 后面。

第四行所有缓存都 I，内存却还不是最新值。这不是丢数据：最新11已经封在不可变的 Data 消息中。异步协议的数据不变量必须把在途载体包括进来，不能逐字沿用旧原子事务末尾的“无 M 就是内存最新”。

对有 $s$ 个其他共享者的 GetM，消息数为 $1+2s+2=2s+3$：一个请求、每个共享者的一次 Inv 与一次 InvAck、一次 Grant 和一次 Installed。当前 C 的事务 $s=2$，所以7条。向脏 owner 取数据的 GetS/GetM 都是请求、Fwd、Data、Grant、Installed，共5条。主例总计 $6+7+5+5=23$ 条；C 的第二次写与 B 未失效前的读都是零消息命中。

三种删掉步骤后的失败 ​

未收齐确认就授权。 在等待集合为 {B} 时，假装它已经为空，给 C 发 GrantM 并让 C 写10。此刻 C=M(10)、B=S(0)，权限已经矛盾；B 的下一次本地读还会返回旧0。这不是靠“最终消息都会到”能补救的，因为错误读取已经可以发生。

用旧内存替代脏数据。 A 持 M(11)，home 仍为0，B 申请读。A 降为 S 后若 home 丢弃返回的11，改以0授权 B，就会得到 A=S(11)、B=S(0)。M 的数量检查会通过，数据检查却失败；必须同时核对权限和内容。

发出 Grant 就提前处理下一项。 A 的写请求使 home 发出 GrantM，但该消息尚未到 A；此时提前开始 B 的读，向预定 owner A 发 FwdS。任意乱序网络可以先交付 FwdS，此时 A 还是 I，处理表没有合法的供数动作。增加别的等待状态可以设计另一种协议，本页选择用 Installed 握手排除这条轨迹。

改变竞争次序，结果也会改变 ​

若先让 A 的 GetM 抵达 home，再让 C 的 GetM 抵达，A 的20会先完成，C 随后完成10。两者结束后让 B 读，答案是10，不是原轨迹的20。网络排序改变了允许的执行次序；协议保证每次读与实际完成的写一致，并不保证由发请求的墙钟时间决定胜者。

$N=1$ 时，读缺失仍有三条消息，S 升 M 的撤销集合为空，也只需三条。不能把“没有其他共享者”解释成不需要取到授权。消息若可以永远不交付，等待可以无限长；安全不变量不提供毫秒级完成期限。

按每条消息保持权限与数据 ​

令 $V$ 为最近一次完成的应用写的值，初始取内存初值。它是证明中的抽象量，不是协议可以向外查询的额外服务。归纳保持：至多一个 M；存在 M 时其他缓存全 I；所有有效缓存的值均为 $V$。若没有 M，内存为 $V$，或者活动事务正等待旧 owner 已经发出的 Data，且该消息携带 $V$。

初态各缓存 I，内存为 $V$。本地读不改变权限和数据；M 本地写只改变唯一有效副本并同时更新 $V$。Get 请求入队只增待办，不赋权。

在共享阶段，Inv 只减少读权限，InvAck 在失效以后才发出。home 只有逐一删完等待集合才发 GrantM，此时除请求者可能仍有 S 外，其他缓存均 I；请求者安装 M 并写入只会留下一个有效副本。GrantS 仅在没有 M 且内存已经最新时发出，不会制造读写并存。

在脏交接阶段，旧 M 可以在 Fwd 到达前继续写；处理 Fwd 时捕获的正是那时的 $V$。同一步撤回 M，因此 Data 在途时没有其他写者；后续 Data 接收与 Grant 不会把旧值越过更新值。GetS 让旧 owner 保留 S，GetM 让其变 I，两者都保持有效副本一致。

最后，Installed 只能由已经安装权限的请求者发出。home 收到它以后才启动下一项，所以下一次所列 owner 或共享者都已真实可处理控制消息。等待升级的缓存仍接受 Inv，消除了“握着旧 S 等新 M，同时拒绝别人撤销”的循环。以上覆盖本地操作和全部消息种类，故不变量按事件数保持。

进展与真实执行成本 ​

再加公平交付、公平处理和有限个应用操作，每个活动事务只等有限组 InvAck、一次 Data 或一次 Installed。这些响应都不依赖另一个应用操作完成，控制消息也不会被 pending 阻塞。每个活动事务因此结束；FIFO 队列中有限个前驱依次结束，每个已到达请求最终被处理。有限缓冲可能引入额外资源等待，本证明没有覆盖；可靠也不等于存在固定网络延迟上界。

协议本体保存 $O(1+N)$ 个缓存/目录状态和在途控制记录。每个缓存只有一个应用 pending，即使它在旧 Installed 回程时发出新请求，也只多出当前事务的有限确认；不会在固定 $N$ 下无界堆积未完成请求。一次共享撤销要枚举 $s$ 个目标，消息数为 $2s+3$；脏交接是5条。这是消息账，不能直接等同于程序运行时间。

完整参考器用 deque 实现 home 队列，但为任意选取交付顺序，把网络保存为列表。删除列表中间一项最坏 $O(1+N)$；每个事件还开启全缓存与在途载体检查，最坏同阶。因此实际参考器的单事件最坏为 $O(1+N)$，有 $s$ 个撤销者的完整远程事务为 $O((s+1)(N+1))$。日志另占已完成操作数 $E$ 的 $O(E)$ 空间；可见状态快照复制整个日志，另花 $O(1+N+E)$。这里按固定大小数据和身份记操作，任意精度整数需另计位成本。

程序的 $V$ 字段、完整日志和故意破坏步骤的测试都用于核验，不参与授权对象、数据来源或消息路由的选择。小规模穷举与随机调度提供具体证据；一般正确性仍来自上述状态不变量和明确的网络条件。