“若要检查同一块的副本谁能写、旧脏副本怎样提供最新值，可在MSI教学协议里逐事务核对权限和数据不变量。它回答单块副本如何保持正确；本页的内存模型另回答跨地址观察怎样组合，两层契约不能互相替代。”
形式陈述
MSI用每块的I（Invalid）、S（Shared）、M（Modified）状态实现缓存一致性契约。本文明确选用教学变体：所有总线事务串行且原子完成，不存在未完成请求交错；S副本与内存一致，M是唯一有效读写副本、可能比内存新。每个原子事务结束后才观察稳定状态。
请求有BusRd（申请读副本）、BusRdX（取得数据及独占权限）、BusUpgr（已有S副本，申请独占权限）。BusRdX遇旧M时，旧主既供最新数据也更新内存，然后失效；这是本文的显式选择，其他实现可以有不同的数据转发方式。
本核心事件
| 旧状态 | 读 | 写 | 逐出 |
|---|---|---|---|
| I | BusRd取最新块，转S再读 | BusRdX取块并使他方失效，转M再写 | 保持I |
| S | 本地读，保持S | BusUpgr使他方S失效，转M再写 | 静默转I |
| M | 本地读，保持M | 本地写，保持M | 最新整块写回，转I |
监听其他核心事务
| 旧状态 | 他方BusRd | 他方BusRdX | 他方BusUpgr |
|---|---|---|---|
| I | 不动作 | 不动作 | 不动作 |
| S | 保持S | 失效为I | 失效为I |
| M | 供最新数据并更新内存，转S | 供最新数据并更新内存，转I | 合法稳定状态中不应发生 |
M与他方S不能共存，而BusUpgr只能由S发起，所以最后一个组合不可达。它应当被断言检查，而不是随意补一条掩盖协议错误的正常转移。
直觉
S可以让多个人读，M把写权收拢到一个人，I禁止使用残留旧值。从S升级只需收回别人的权限；从I写入还要取得完整数据，以保留本次没覆盖的字节。
三状态图只描述本文事务完成后的观察点。若把请求发送、仲裁、数据返回和失效确认拆成独立消息，就必须增加等待与竞争状态；不能用这张图直接声称分裂总线已经无竞态。
例子与边界
三个核心转交一个word
内存初值0，P/Q/R均I。下面每行是一个完整事件之后的状态；括号内为有效副本的值。
| 操作 | P | Q | R | 内存 | 总线动作 |
|---|---|---|---|---|---|
| P读 | S(0) | I | I | 0 | BusRd |
| Q读 | S(0) | S(0) | I | 0 | BusRd |
| P写1 | M(1) | I | I | 0 | BusUpgr |
| R读 | S(1) | I | S(1) | 1 | BusRd；P供数据并写回 |
| Q写2 | I | M(2) | I | 1 | BusRdX；P/R失效 |
| Q逐出 | I | I | I | 2 | 脏回写 |
第四步R不能从尚为0的内存直接读旧值；必须由M的最新数据修正此次响应。第五步Q取得完整块后再改目标word，保留块内其他字节。
两个最短错误轨迹
省略第三步的失效：P成M(1)，Q仍S(0)，Q下一次本地读就得到旧0，且读写权限同时存在。省略第四步的M供数：状态表可以写成两个S，但R读到0、P保留1，数据不变量仍被破坏。只检查M数量不超过一，抓不到第二种错误。
推论与应用
把按已完成写操作更新的最新抽象块记为
I读若遇M，原M把
这份证明依赖事务原子完成的观察边界，有限状态穷举只能补充检查实现是否忠于规则。总线最终是否服务每个请求还需要公平调度假设，安全不变量本身不保证进展。
本页不提供跨地址排序或持久化保证。内存模型和掉电恢复仍有各自的契约；把状态名换成MESI也不会自动补齐这些保证。
参考资料
- Vijay Nagarajan et al., A Primer on Memory Consistency and Cache Coherence, 2nd ed., 2020，Ch. 7，监听式协议与原子请求/事务假设。本文把事务折叠成稳定状态的一步，并明确选取BusUpgr与M响应写内存规则。
- James R. Goodman, “Using Cache Memory to Reduce Processor-Memory Traffic”, ISCA, 1983, pp. 124–131；历史背景，不作为本文三状态表的逐项规范。