SC、TSO 与 XC：用形式化语义判断内存重排
两个核心各自按程序写入、读取共享变量时，某个读取究竟能得到什么值？回答这个问题需要两类规则：操作进入全局内存顺序的约束，以及加载从哪次存储取值的约束。本书第 3～5 章依次用 SC、TSO 和教学用的 XC 展示了规则如何放宽。这里讨论的是书中以物理地址上的加载、存储为对象的模型；XC 是示例模型，不应直接当成某个处理器的完整规范。
先把程序顺序与内存顺序分开
用 L(a)、S(a) 表示对地址 a 的加载和存储。<p 是同一核心的程序顺序，<m 是所有核心的全局内存顺序，两者在本书的三个模型中都是总顺序。例如，S(x) <p L(y) 只说程序先写 x 再读 y；能否推出 S(x) <m L(y)，取决于模型。下面的 X、Y 都指动态内存操作，a、b 可以相同也可以不同。
三个模型还要求原子读改写（RMW）的读和写作为不可分割的操作；下文的重排表也列出 RMW。普通加载的取值规则则要单独看：允许一次加载越过较早的存储，不等于允许它读到自己刚写过的地址的旧值。
SC：每个核心的程序顺序都进入全局顺序
SC（sequential consistency，顺序一致性）要求同一核心任意两次内存操作满足
若 X <p Y，则 X <m Y。具体展开，就是 L→L、L→S、S→S、S→L 四种组合全部保序，不论地址是否相同。每次加载读取全局顺序中排在它之前、对同地址的最后一次存储：
Value(L(a)) = Value(MAX_<m { S(a) | S(a) <m L(a) })初始值可视作最初的存储。原子 RMW 的读和写在 <m 中逻辑上相邻，不能插入其他内存操作。下面是原书表 3.4：SC ordering rules 的转录。行是程序顺序中较早的操作 1，列是较晚的操作 2；X 表示必须按程序顺序进入 <m。
| 操作 1 ＼ 操作 2 | Load | Store | RMW |
|---|---|---|---|
| Load | X | X | X |
| Store | X | X | X |
| RMW | X | X | X |
用原书表 3.1的消息传递程序检验这两条规则（初始 data=0，flag≠SET）：
Core C1 Core C2
S1: data = NEW; L1: r1 = flag;
S2: flag = SET; B1: if (r1 != SET) goto L1;
L2: r2 = data;当某次 L1 读到 SET，取值规则要求 S2 <m L1。程序顺序又给出 S1 <m S2 和 L1 <m L2，因此 S1 <m S2 <m L1 <m L2，r2 只能是 NEW。这里是对读到 SET 并继续执行的情形作判断，不保证自旋一定结束。
TSO：只放松 Store→Load，同时要求本地旁路
TSO（total store order）继续要求任意地址上的 L→L、L→S、S→S 保序；它不再普遍要求 S(a) <p L(b) 推出 S(a) <m L(b)。这允许核心把存储暂留在 FIFO 写缓冲区，后面的加载先进入全局顺序。不过，加载必须能看到本核心程序顺序中较早、写往同一地址的存储：
Value(L(a)) = Value(MAX_<m {
S(a) | S(a) <m L(a) 或 S(a) <p L(a)
})这个集合同时考虑已经进入全局顺序的存储，以及本核心较早但可能仍在缓冲区中的存储。后一种情况通过旁路得到值。若较早的存储来自同一核心、且尚未进入全局顺序，它在 <m 中位于加载之后，因此会优先于加载之前的旧存储。TSO 的 FENCE 与同核心前后的加载、存储、RMW 和 FENCE 都保序；尤其 S <p FENCE <p L 会推出 S <m L。
下面是原书表 4.4：TSO ordering rules 的转录。B 表示 Store→Load 不要求按程序顺序进入 <m，但同地址时必须旁路取值。X 的含义与上表相同。
| 操作 1 ＼ 操作 2 | Load | Store | RMW | FENCE |
|---|---|---|---|---|
| Load | X | X | X | X |
| Store | B | X | X | X |
| RMW | X | X | X | X |
| FENCE | X | X | X | X |
**原书表 3.3（亦为表 4.1）**给出经典的 Store Buffering 程序，初始 x=y=0：
Core C1 Core C2
S1: x = NEW; S2: y = NEW;
L1: r1 = y; L2: r2 = x;在 SC 下，r1=r2=0 会要求 S1 <m L1 <m S2 <m L2 <m S1，形成环，所以不可能。在 TSO 下，两次加载都可先于各自尚未排出的存储进入 <m，于是 (r1,r2)=(0,0) 可能出现。若在两个核心的 S→L 之间各放一条 FENCE，这个结果再次被禁止。前一节的消息传递仍保证读到 SET 后读到 NEW，因为它只用到了 TSO 保留的 S→S、L→L 顺序。
原书表 4.3进一步检查旁路规则，初始 x=y=0，并假定 r2=r4=0：
Core C1 Core C2
S1: x = NEW; S2: y = NEW;
L1: r1 = x; L3: r3 = y;
L2: r2 = y; L4: r4 = x;虽然两个核心都还没看到对方的写入，L1 和 L3 仍须从本核心较早的存储取值，所以 r1=r3=NEW。B 不能被误读为“同地址的 Store→Load 可以读旧值”。
XC：只保留同地址顺序，并让 FENCE 显式建立跨地址顺序
XC 是书中用于教学的宽松模型。它仍假设一个全局总顺序 <m，但不同地址上的普通加载与存储默认不保序。其正式规则分三组：
- FENCE 保序：对同一核心，
L(a) <p FENCE、S(a) <p FENCE、FENCE <p FENCE、FENCE <p L(a)、FENCE <p S(a)，分别推出相应的<m顺序。因此，FENCE 前的操作都排在它后面的操作之前。 - 同地址保序：
L(a) <p L′(a)、L(a) <p S(a)、S(a) <p S′(a)分别推出对应的<m顺序。不同地址没有这三条保证。 - 加载取值：沿用 TSO 的旁路公式，即
Value(L(a)) = Value(MAX_<m { S(a) | S(a) <m L(a) 或 S(a) <p L(a) })。
特别留意：同地址的 S→L 仍没有 <m 保序要求，而是靠取值规则保证读到本核心较早的写入。RMW 作为原子读改写操作出现在下表中；它与同地址操作的顺序按表中的 A 处理。原书表 5.5：XC ordering rules 转录如下。A 表示仅同地址强制保序；B 和 X 沿用前表定义。FENCE 行列的 X 与地址无关。
| 操作 1 ＼ 操作 2 | Load | Store | RMW | FENCE |
|---|---|---|---|---|
| Load | A | A | A | X |
| Store | B | A | A | X |
| RMW | A | A | A | X |
| FENCE | X | X | X | X |
于是，XC 单靠普通操作不能保证前述消息传递。下面摘录原书表 5.3为表 5.1 程序补上的两条 FENCE；初始 data1=data2=0，flag≠SET：
Core C1 Core C2
S1: data1 = NEW; L1: r1 = flag;
S2: data2 = NEW; B1: if (r1 != SET) goto L1;
F1: FENCE; F2: FENCE;
S3: flag = SET; L2: r2 = data1;
L3: r3 = data2;当 L1 读到 SET 时，F1 保证 S1,S2 <m S3，F2 保证 L1 <m L2,L3；加载取值规则把读到 SET 的 L1 接在 S3 之后。因此 r2=r3=NEW。但 S1 与 S2、L2 与 L3 仍可各自重排：程序的正确性并不依赖这些额外顺序。删去 F2，L2 就可能在看到标志之前读取旧的 data1。书中表 5.4 还把同一思路用于锁：临界区操作与释放之间、获取与临界区操作之间用 FENCE 建立交接顺序。
把三张表用于判断执行结果
读程序时，先按表把必须保留的 <p 边写成 <m 边，再根据每次加载的值补充“它读到了哪次存储”的约束。如果边形成环，这个结果不可能；若没有环，还要用对应模型的取值规则检查同地址旁路。只看表中的空白或 B，不足以判断加载可以读到任何值。
对书中的两个问题，可以这样自测：消息传递中，观察到 flag=SET 后读取数据，SC 和 TSO 均能推出 NEW，XC 需要适当的 FENCE；Store Buffering 中两次交叉读取都为 0，SC 禁止，TSO 允许，XC 也允许。这个差别正是三种形式化语义逐步放宽的结果。
本笔记讨论的是一致性模型给核心操作施加的约束。缓存如何用请求取得读写权限，属于另一层机制，可接着读 aigc/什么是连贯性请求。