计算机体系结构 24：内存一致性模型与 Store Buffering

核心问题

第 23 篇只处理同一个 cache line 的副本一致性。那套规则能阻止两个核心同时写同一地址，也能要求读 miss 找到脏 owner。但是程序通常同时操作多个地址。两个核心各自先写一个地址，再读对方写的地址时，单地址 coherence 没有直接回答“两个读能不能都看到旧值”。

本篇用 Store Buffering 这个 litmus case 切开 coherence 和 memory consistency 的边界：

1
2
3

初始: x = 0, y = 0
T0: x = 1; r0 = y
T1: y = 1; r1 = x

问题是结果 r0=0, r1=0 是否可能。顺序一致性模型下不可能；显式 store buffer 教学模型下可能。这个差异说明：每个地址最终都保持一致，并不推出所有地址上的操作都按程序顺序进入一个全局序列。

本文附件：

证据等级：功能执行。脚本枚举 SC 下所有保持线程内顺序的交错，并构造一个显式 store buffer 轨迹。它不是 RVWMO 完整解释器，也不是真实硬件测量。

边界

一致性教材把 coherence 和 consistency 分开：coherence 针对同一位置的读写值，consistency 定义所有内存操作之间允许出现的顺序关系。RISC-V RVWMO 规范也不是把硬件实现固定成某种队列，而是用全局内存顺序、load-value axiom、atomicity axiom、preserved program order 等规则描述允许行为；fence 和 acquire/release 等机制用于增加必要顺序。

本文只做两个模型：

SC 枚举器：把两个线程的四条操作交错成一个全局序列，同时保持每个线程内部的程序顺序。
Store buffer 机器：每个线程的 store 先进入本地 buffer，load 先查本线程 buffer 中同地址的项，没有同地址项时读共享内存；buffer 可以稍后 flush 到内存。

这两个模型足以展示“coherence 不推出跨地址 SC”。它们没有覆盖 RVWMO 的全部 preserved program order 条件、依赖顺序、AMO、地址翻译、I/O、取指或页表遍历。

顺序一致性下为什么不能得到 0/0

SC 要求结果等价于某个全局顺序，且每个线程内部顺序不能被打乱。对 Store Buffering，有四个操作：

A: T0 store x=1
B: T0 load y -> r0
C: T1 store y=1
D: T1 load x -> r1

线程内约束是 A < B 和 C < D。若 r0=0，则 B 必须在 C 之前发生，否则 B 会看到 y=1。若 r1=0，则 D 必须在 A 之前发生，否则 D 会看到 x=1。把四个不等式放在一起：

1	`A < B < C < D < A`

这形成环，无法成为一个线性全局顺序。因此 SC 禁止 r0=0,r1=0。

脚本枚举所有合法交错，输出文件记录的结果集合中没有这个结果：

{
  "model": "SC",
  "forbidden": "r0=0,r1=0"
}

复跑命令：

1	`python3 examples/computer-architecture/memory-model/src/run_cases.py`

本次输出：

1	`memory model cases: PASS`

Store buffer 怎样允许 0/0

显式 store buffer 轨迹如下：

T0: buffer x=1
T1: buffer y=1
T0: r0=load memory y->0
T1: r1=load memory x->0
T0: flush x=1
T1: flush y=1

两个 store 都已经在本线程“发出”，但还没有成为对另一个线程可见的共享内存更新。T0 读 y 时，本线程 buffer 中没有 y，于是读内存里的旧值 0。T1 读 x 时同理，也得到 0。之后两个 buffer flush，最终内存变成 x=1,y=1。

这个轨迹没有违反单地址 coherence。对地址 x 来说，只有一个写 x=1，最终所有核心都会承认这个写。对地址 y 也一样。问题在于两个地址之间没有一个强制顺序，能让“x=1 对别人可见”一定早于 “T0 读取 y”，也能让“y=1 对别人可见”一定早于 “T1 读取 x”。

因此，coherence 像是在每个地址上各自维护一条账本；memory consistency 决定不同账本上的条目怎样互相排序。程序需要跨地址消息传递、发布订阅或锁时，不能只依赖 coherence。

fence 与模型强度

RISC-V RVWMO 是弱内存模型。弱并不等于任意乱序；它仍然有 preserved program order、load-value、atomicity、progress 等约束。程序若需要更强顺序，要通过 FENCE、原子指令的 aq/rl 位、或更高层语言的同步原语表达。

对 Store Buffering，若两个线程都在 store 之后、load 之前加入足够强的 fence，含义就是要求本线程的前一组内存操作在后一组操作之前对外排序。教学 store buffer 机器中，这等价于 load 前先 flush 对应 store，因此 r0=0,r1=0 会被排除。真实 ISA 的结论必须回到该 ISA 的 fence 语义；本文只展示 fence 在这个简化模型里的作用方向。

验收结果

memory_model_summary.txt 记录：

1
2

memory model cases: PASS
SC forbids SB (0,0); explicit store buffers allow SB (0,0); release/acquire separates plain data-race and atomic-relaxed variants; LR/SC retry preserves one atomic increment after interference.

本文验收项对应为：

能从 A < B < C < D < A 的环说明 SC 禁止 r0=0,r1=0。
能读懂 store buffer 轨迹，说明两个读为何都能读到旧值。
能解释这个反例没有破坏每个地址自己的 coherence。
能说明脚本不是 RVWMO 完整判定器，不能把“脚本未枚举”写成“ISA 禁止”。

练习

练习 1

在 SC 下，r0=0,r1=1 是否可能？给出一个全局顺序。

答案线索：可能。一个顺序是 A: x=1，B: r0=y，C: y=1，D: r1=x。B 在 C 前，所以 r0=0；D 在 A 后，所以 r1=1。

练习 2

在本文 store buffer 模型中，如果 T0 在 x=1 后必须先 flush 才能执行 r0=y，但 T1 不加这个限制，r0=0,r1=0 还能出现吗？

答案线索：不能。T0 的 store 先 flush 后，x=1 已在共享内存中。T1 读取 x 时若本地没有更新 x 的 buffer 项，就会读到 1，因此 r1=0 不成立。