内存一致性模型

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

判断一个读值时，应先选出它的来源写，再检查该选择是否与其他关系共同满足模型。单个读到旧值可能合法，但把两个这样的选择拼在一起可能形成禁止的环；故合法性不是逐个事件独立判断。

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

指定模型后重算 store buffering ​

以下采用 Sewell 等人 2010 年的 x86-TSO 程序员模型，限制在普通 write-back 内存及模型支持的对齐访问片段；不涉及混合宽度、非临时访问或页表变化。这个抽象机的共享内存记为 $M$，每个硬件线程拥有独立 FIFO 写缓冲 $B_P$。对下面没有锁定指令的程序，只需四条规则：写把地址和值追加到本线程缓冲；读先取本线程缓冲中该地址的最新写，否则读共享内存；缓冲的最老写可排出并更新共享内存；MFENCE 只有在本线程缓冲已空时才能完成。这是可观察行为的模型，不是缓存电路的内部结构图。

初始 $M[x]=M[y]=0$，两个缓冲为空。store-buffering（SB）测试为：

线程 P: W(x,1); R(y) -> r1
线程 Q: W(y,1); R(x) -> r2

一条产生双零的合法执行可以逐步核查：

同一观察在顺序一致性公理库顺序一致性Sequential consistency并发对象操作可重排为保持各线程观察的合法顺序历史；寄存器情形要求每次读取得相应最近写值。下被禁止。程序顺序要求 $W(x)<R(y)$ 与 $W(y)<R(x)$，读到初值又要求 $R(y)<W(y)$ 与 $R(x)<W(x)$，合起来形成

因此，障碍是不存在同时解释两个地址的全序，并非某次读到初值本身不合理。其余三种结果都有 SC 见证：先完整运行 P 再 Q 得 $(0,1)$，先 Q 再 P 得 $(1,0)$，先完成两写再做两读得 $(1,1)$；令每次写随即排空缓冲，这些也都是 x86-TSO 执行。

现在在两个线程各自的写与读之间插入 MFENCE。设写 x、写 y 排入共享内存的事件分别为 $D_x,D_y$。栅栏保证 $D_x<R(y)$、$D_y<R(x)$。若仍双零，则还需 $R(y)<D_y$、$R(x)<D_x$，从而得到 $D_x<R(y)<D_y<R(x)<D_x$，不可能。因此两道指定位置的 MFENCE 排除了双零。“有一道屏障”不足以代替这四个关系；若只给 P 加栅栏，Q 可以先缓冲 y、读到 x=0，随后 P 排出 x 并读到尚未排出的 y=0。

C++ 源码须另选语言内存序 ​

硬件事件不能直接当成普通 C++ 变量访问。对 std::atomic<int> x{0}, y{0}，让 P 执行 x.store(1, order); r1=y.load(order)，Q 对称执行；这里 order 是占位说明，实际 store/load 必须分别选用合法内存序。假设初始化在线程启动前完成，结果在线程结束后汇总，且没有其他访问：

若把 x、y 换成无同步的普通 int，冲突的非原子访问产生数据竞争公理库数据竞争Data race · 数据竞态不同线程对同一内存位置的冲突访问既未按模型同步排序、也未通过原子操作协调的情形。，C++ 行为未定义；不能把其结果表写成“允许四种读值”。volatile 也不是修复这项语言问题的同步协议。上述表是源语言契约；某编译器如何用机器指令实现它，需要另证编译映射，不能把 C++ 的 seq_cst 直接定义成某一条硬件栅栏。

发布数据是另一种测试。P 先普通写 d=42，再对原子标志 ready 作 release 写 1；Q 用 acquire 读 ready，仅当读到该 release 写的 1 时才普通读 d。假设 d 的初始化和这次发布写之外没有其他写入，发布写、同步边和线程内顺序串成happens-before公理库Happens-before 关系Happens-before · Causal order由程序顺序及模型规定的通信或同步边生成的事件因果严格偏序。，该读得到 42。读到 0 的分支不能无条件访问 d；将 acquire 改为 relaxed 也可能失去这条保护，造成普通 d 上的数据竞争，后果不只是“偶尔读到旧值”。

缓存一致协议即使保证所有核心按同一顺序观察地址 $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给定系统模型与形式规格，判定所有指定初始行为是否满足公式，并交付证明结果或诊断见证。可以把有限程序、候选内存模型和违例条件联合编码，搜索某个允许轨迹是否产生禁用观察。得到反例说明该模型仍容许该行为；未在给定界内找到反例，只是验证算法在当前状态空间上的结论，不会把弱内存模型改写为顺序一致。