SC 的严格定义
Lamport 的开关比喻，穷举法可以精确判定哪些结果合法
CS152 · 第 22 课
第 21 课解决了"单个地址的读该返回什么值"；这一课处理更难的问题——"多个地址的读写顺序，对不同处理器而言应该看起来是什么样"。答案不是唯一的：从最严格的顺序相合性到宽松得多的模型，都是真实处理器做出的不同权衡。
内存相合性模型（Memory Consistency Model, MCM）描述"跨多个硬件线程，load 指令可以返回哪些值"。在这个语境下重新定义：一致性（coherence）描述单个内存地址应该返回哪些合法值；相合性（consistency）描述跨越所有内存地址的属性。
一个具体的生产者-消费者例子：生产者写数据、设置 flag=1；消费者自旋等待 flag 变为 1，再读取数据。这段代码能否正确工作，完全取决于底层相合性模型是否保证"生产者写数据一定先于写 flag 被消费者观察到"。
Lamport 给出的经典定义（原文引用）："一个系统是顺序相合的，如果任意一次执行的结果，都等同于把所有处理器的操作按某个顺序串行执行的结果，且每个处理器自己的操作在这个顺序里保持程序指定的顺序。"直观的"开关"比喻：所有处理器按程序顺序发出 load/store；内存随机选择一个处理器，把它的一次内存操作执行完，再切换到另一个处理器，如此往复。
具体的判定实例（重新逐一枚举验证）：初始 M[X]=M[Y]=0；P1 执行 (1)M[X]=1 然后 (2)读 x2=M[Y]；P2 执行 (3)M[Y]=1 然后 (4)读 x2=M[X]。在 SC 下，四步操作必须能排成一个尊重"1 先于 2、3 先于 4"的全局顺序。枚举全部 6 种满足这个约束的排列（1234、1324、1342、3124、3142、3412），逐一推演每种排列下 (P1.x2, P2.x2) 的结果，得到的可达结果集合恰好是 {(0,1), (1,1), (1,0)}——(0,0) 在任何合法的 SC 全序下都无法达到。这与幻灯片给出的判定表完全一致：(0,0)→N；(0,1)/(1,0)/(1,1)→Y。
幻灯片明确指出：大多数真实机器并不是 SC 的——原因是 SC 的强顺序保证会严重限制硬件优化空间（例如禁止 store 缓冲这类常见优化）。真实实现 SC 的例子：MIPS R10K——用硬件推测执行 load/store，一旦跨核检测到顺序违反就撤销重来。
TSO（Total Store Order）允许处理器把自己的 store 暂存在本地的 Store Buffer 里："处理器可以比其他处理器更早看到自己的写入"。优化规则：更晚的 load 如果访问不同地址，可以越过缓冲中尚未真正写出的 store；更晚的 load 如果访问同一地址，可以直接从缓冲中的 store 里"旁路"取值。幻灯片指出：TSO 是目前常见处理器里最强的相合性模型。
TSO 允许 (0,0)：一个经典的"Store 缓冲违反 SC"实例（重新验证）。同样的程序，TSO 下的判定表变成全部四行都是 Y，即 (0,0) 现在也合法了。原因：P1 把 M[X]=1 暂存进自己的 Store Buffer（还没真正写入共享内存），随后就去读 M[Y]；P2 同理把 M[Y]=1 暂存在自己的 Store Buffer 里，随后去读 M[X]。只要两次读操作都发生在各自缓冲的 store 真正"排空"到共享内存之前，P1 就会读到 Y=0（陈旧值），P2 也会读到 X=0（陈旧值）——即使从每个处理器自己的视角看，"我的写入已经发生了"。这正是内存模型文献中著名的"Dekker 式检测实例"，专门用来暴露 Store 缓冲对 SC 的破坏。
从强到弱的相合性模型谱系（附真实 ISA 例子）：
| 模型 | 真实 ISA 例子 |
|---|---|
| SC（最强） | —（IBM 370、x86、ARM、RISC-V 均不是 SC） |
| TSO | IBM-370 TSO、x86 TSO、SPARC TSO（默认）、RISC-V RVTSO（可选） |
| 弱、多副本原子 | 修订版 ARM v8、RISC-V RVWMO（RISC-V 基线弱内存模型） |
| 弱、非多副本原子（最弱） | ARM v7、原始 ARM v8、IBM POWER、Digital Alpha（"极弱"） |
多副本原子性（multi-copy atomicity）："每个硬件线程必须按程序顺序看待自己的内存操作，可以在本地缓冲、围绕缓冲重排访存顺序；但一旦某个本地 store 对系统中任何一个其他硬件线程变得可见，它就必须同时对所有其他硬件线程可见"——这正是"原子"一词的含义：可见性要么对所有人同时发生，要么都还没发生，不存在"对 A 可见、对 B 不可见"的中间状态。非多副本原子模型放弃了这个保证：不同处理器可能以不同的顺序看到另一个处理器的写入序列（例如通过分层的共享缓冲区结构，共享同一中间缓冲的处理器之间同步得更快）。幻灯片明确指出："近期业界共识认为，非多副本原子模型对通用处理器而言过于弱了"——这也是为什么 ARM 在 v8 修订版里收紧到了多副本原子模型。
在弱内存模型下，软件需要显式的 fence（栅栏）指令来指定必须保证的顺序——例如 fence w,w（写-写栅栏）、fence r,r（读-读栅栏）。回到生产者-消费者例子：生产者需要在写数据和写 flag 之间插入 fence w,w，消费者需要在读到 flag 和读数据之间插入 fence r,r，才能在弱内存模型下依然保证正确的先后关系——这正是硬件把"排序保证"这份责任转移给软件的具体代价。此外，编译器本身也会重排指令（不仅仅是硬件），所以语言级别的内存模型（如 C11/C++11 的 atomic 类型）同样需要明确定义，并最终映射到具体 ISA 的 fence 指令上。
(0,0) 这样的结果在 TSO 下变得合法，而这在 SC 下是不可能出现的——这正是并发程序里许多微妙 bug 的根源，也是 fence 指令存在的原因。问题 1：初始 M[X]=M[Y]=0，P1 执行"写X=1，读Y"，P2 执行"写Y=1，读X"。在严格的顺序相合性（SC）下，(P1读到的Y, P2读到的X) 能否等于 (0, 0)？
问题 2：为什么同样的程序，在 TSO 下 (P1.x2, P2.x2)=(0,0) 是合法的，而在 SC 下不合法？
问题 3："多副本原子性（multi-copy atomicity）"具体保证了什么？
Lamport 的开关比喻，穷举法可以精确判定哪些结果合法
允许本地提前看到自己的写入，打开了 SC 不允许的结果空间
可见性要么对所有人同时发生，要么都还没发生
软件显式指定顺序，把排序责任从硬件转移给程序员/编译器
sp23/lecture_slides/L22_Memory_Consistency.pdf（UC Berkeley CS152/CS252A, Spring 2023, Sophia Shao）