内存一致性模型

处理器会把写暂存在 store buffer，编译器会移动互不依赖的操作，缓存协议会让传播分阶段完成；逐条等待全局可见会牺牲性能。程序证明却需要知道哪些观察绝不会出现。内存模型把优化自由与推理义务同时写成约束：同步原语买回哪些顺序，普通访问在缺少同步时还剩什么语义。

因此模型不是“处理器实际按什么顺序执行”的录像，而是对所有允许观察的公理化包络。一个实现可以内部乱序，只要对外执行仍落在集合内；一次测试从未观察到某结果，也不能证明模型禁止它。

store-buffering 测试从 $x=y=0$ 开始，两个线程分别执行：

线程 P: x = 1; r1 = y
线程 Q: y = 1; r2 = x

若两次写先停留在各自 store buffer，随后的读可在对方写尚未传播时取得初值，于是出现 $r1=r2=0$。该结果不能由保持两条程序顺序的单一全序解释，却被一些硬件模型允许。只有加入目标模型认可的栅栏，或给原子操作选择足以建立顺序的内存序，才能排除它；把变量仅声明为 atomic 而使用过弱顺序，未必得到 SC 结果。

另一条消息发布执行为：线程 $P$ 先写普通数据 $d=42$，再 release 写标志 $f=1$；线程 $Q$ 的 acquire 读若从该写取得 $1$，随后普通读 $d$ 必须看到受 happens-before 保护的发布结果。把 acquire 改成 relaxed 后，这条跨线程顺序可能消失。两段代码表面只差一个内存序参数，允许执行集合却不同。

缓存一致协议即使保证所有核心按同一顺序观察地址 $x$ 的写，也未必约束 $x,y$ 之间的相对观察。happens-before公理库Happens-before 关系Happens-before · Causal order由程序顺序及模型规定的通信或同步边生成的事件因果严格偏序。同样只提供模型中的顺序骨架；还需 $\mathrm{rf}$ 合法性、原子位置写序、数据竞争语义和禁止循环等公理，才能决定一次候选执行是否合法。

语言模型、处理器 ISA 模型和分布式副本一致性可能共享“弱”“因果”“顺序”等词，却有不同操作粒度与故障假设。跨层正确性需要证明编译器映射把每个目标执行精化为源模型允许的执行；名称相似不能代替这项映射。某些模型还专门限制 out-of-thin-air 值，单靠局部读写顺序无法排除这种全局循环。

弱内存算法的证明通常分两步：先证明语言层 happens-before、原子写序与读值满足不变量，再验证编译器和 ISA 映射保持这些边。互斥锁、release/acquire、顺序一致原子与栅栏只是构造约束的不同工具，不应统一替换成模糊的“加一道屏障”。

无数据竞争程序在特定语言模型下可能获得 SC-for-DRF 保证，但其“race-free”定义、原子操作范围与结论各不相同。这是一条模型定理，不是所有共享内存系统的默认事实。

设计并发算法时，必须把证明依赖的顺序关系映射到目标语言和处理器提供的原语。仅在某台机器上重复测试未见异常不能替代模型证明，因为被允许但罕见的执行仍可能在不同编译、核心或负载下出现。

模型检查公理库模型检查问题Model checking problem · Model checking给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。可以把有限程序、候选内存模型和违例条件联合编码，搜索某个允许轨迹是否产生禁用观察。得到反例说明该模型仍容许该行为；未在给定界内找到反例，只是验证算法在当前状态空间上的结论，不会把弱内存模型改写为顺序一致。