内存一致性模型

形式陈述 ​

内存一致性模型是共享内存系统公理库共享内存系统Shared-memory system进程通过读写共享对象交互的并发模型。对程序、编译器与硬件之间可观察行为的规格。给定一次共享内存执行中的读、写、原子操作、线程内程序顺序与 reads-from 候选关系，模型约束哪些重排可见、每次读可从哪次写取得值，以及是否存在满足这些约束的全局或局部次序。等价地，一个模型规定读写事件所组成的允许执行集合；实现只能产生集合内的执行，程序若想跨实现推理，则必须只依赖该集合共同保证的性质。并发对象历史公理库并发对象历史Concurrent object history · Invocation-response history按线程记录对象操作调用与匹配返回的有限或无限事件序列。记录调用与返回，用于对象正确性；它可以由某些内存执行投影得到，却不是本页定义读值与重排规则所需的共同前置。

几个相邻概念的约束层级不同。coherence 通常逐地址要求对写入形成一致次序，并让读取遵守该地址的写序；顺序一致性公理库顺序一致性Sequential consistency共享内存中的读写操作可排成保持各线程程序顺序并解释所有读值的单一全序。要求所有线程的内存操作可排成一个保持各线程程序顺序的单一全序；线性一致性公理库线性一致性Linearizability每次操作可放置在调用与返回之间的单点，使历史等价于满足实时顺序的顺序规范。针对并发对象操作，还要求该顺序保持不重叠操作的真实时间先后。单地址 coherence 不能推出跨地址的顺序一致性，顺序一致性也不自动具有线性一致性的实时条件。

直觉 ​

处理器和编译器希望重排指令、缓冲写入并并行执行，因为严格逐条等待会浪费大量性能；程序员又需要某些观察始终不可能发生，才能证明并发代码正确。内存模型划定双方的合同边界：优化可以越过表面源代码顺序到什么程度，锁、原子变量和栅栏又能恢复哪些顺序。

把模型看成“允许执行集合”比把它看成一句强弱标签更可靠。更弱的模型允许更多历史，为实现留出更大优化空间，也要求程序通过同步操作排除不希望的历史；更强的模型减少可能行为，推理简单，却可能限制硬件与编译器。所谓一致性不是缓存最终会不会收敛，而是每个读值与各类次序能否共同得到一个被规格接受的解释。

例子与边界 ​

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

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

若每个线程的写先停留在本地 store buffer，随后的读可在对方写尚未对本核可见时读到旧值，于是出现 $r1=r2=0$。这一结果不符合顺序一致性：任何保持两个线程程序顺序的全序，都无法同时把两次读放在各自应观察的写之前；但一些弱硬件模型允许它。加入模型规定的内存栅栏或使用具有足够强顺序的原子操作，才可排除该结果。

缓存一致协议即使保证所有核心按同一顺序观察对地址 $x$ 的写，也未必约束 $x$ 与 $y$ 两个地址之间的相对观察次序，因此不能自动提供顺序一致性。语言或硬件文献中的happens-before公理库Happens-before 关系Happens-before · Causal order由进程内顺序与消息传递生成的事件因果严格偏序。由程序顺序、同步、原子或模型规定的边生成，却不是一份完整内存模型：仍需规定哪些读取可见、数据竞争时行为如何，以及编译器可执行哪些变换。Lamport 分布式因果关系则从进程内顺序与消息发送—接收生成事件偏序，不含共享内存读值和编译器变换规则。二者共享因果先后的数学图像，但跨领域引用时必须回到各自定义。

本页讨论共享内存中的程序可观察行为，不把语言内存模型、处理器 ISA 模型和分布式副本一致性压成同一对象。三者可能借用相似词汇，但操作粒度、故障假设与实时语义不同；跨层论证必须说明编译器映射和硬件指令是否保持上层保证。把允许执行表示为轨迹集合公理库轨迹与路径语义Trace semantics · Path semantics · Execution traces以状态路径和可观察动作轨迹描述有限、无限与最大行为，并说明投影和隐藏会遗忘什么。有助于比较模型，但投影时必须保留读值来源、同步与可观察事件，不能只留下一个无类型事件序列。

推论与应用 ​

顺序一致性提供接近指令交错的基准心智模型，线性一致性则适合说明锁、队列、寄存器等对象操作仿佛在调用区间内瞬间生效。弱内存下，互斥锁、release/acquire、顺序一致原子与栅栏通过建立必要顺序，缩小程序实际可达的历史集合。无数据竞争程序在特定语言模型下可能获得近似顺序一致的保证，但这是一条需精确陈述前提的语言定理，不是所有系统的默认事实。

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

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