无数据竞争保证与 SC-for-DRF

形式陈述 ​

SC-for-DRF 不是脱离语言后仍成立的一条无条件定理，而是一族由内存模型公理库内存一致性模型Memory consistency model · Memory model规定并发程序的内存操作可以产生哪些可观察执行的契约。参数化的保证。设模型 $M$ 规定普通访问、原子访问、同步操作及 happens-before 的生成规则。常见的 DRF${}_0$ 形式先把程序 $P$ 称为无数据竞争：$P$ 的每个顺序一致公理库顺序一致性Sequential consistency共享内存中的读写操作可排成保持各线程程序顺序并解释所有读值的单一全序。执行中，所有相互冲突的普通访问都由 $M$ 认可的同步关系排序。随后模型承诺

$$P\in {\mathrm{DRF}}_M⟹{\mathrm{Beh}}_M(P)\subseteq {\mathrm{Beh}}_{\mathrm{SC}}(P),$$

或承诺一个针对普通访问、同步操作和外部可观察结果的相应 SC 投影。左侧的 DRF 判据与右侧的行为等价范围必须成对给出：有的模型在所有 SC 执行上定义 race-free，有的直接约束语言允许执行中的数据竞争公理库数据竞争Data race · 数据竞态不同线程对同一内存位置的冲突访问既未按模型同步排序、也未通过原子操作协调的情形。；有的保证完整 SC 行为，有的只保证正确同步部分可按交错语义解释。

以下 C++ 陈述固定到 WG21 工作草案 N5009（2025-03-15）。其中 [intro.races] 把数据竞争定义为两个潜在并发的冲突动作，其中至少一个不是原子动作，且二者没有 happens-before 排序；程序执行包含数据竞争便产生未定义行为。同一节还给出一条范围更窄的语言级说明：程序若正确使用 mutex 与顺序一致原子来排除全部数据竞争，并且不使用其他同步操作，其可观察行为仿佛各线程操作被简单交错。[atomics.order] 另行规定顺序一致原子操作的单一全序；混入较弱内存序后，不能继续套用这段简化说明。

这些都是 C++ 抽象机对程序允许行为与未定义行为的合同，不是“处理器实际按全序执行”的硬件定理。编译器和处理器仍可重排或并行执行，只要没有引入草案禁止的可观察行为。Java 内存模型也以“正确同步程序”给出顺序一致语义，但其冲突、同步序与初始化规则属于 Java 自身，不能把 C++ 的未定义行为结论直接移过去。

证明骨架通常先由同步操作建立顺序边，再证明每一对普通冲突访问都被这些边定向。对所得偏序取保持线程程序顺序和同步顺序的线性扩展，若模型的读值、同步和编译变换规则允许，就可构造产生同样观察的 SC 执行。最后这一步高度依赖模型：relaxed 原子、consume 依赖、混合大小访问和编译器映射都可能改变可构造的全序，因此不存在一份可替代具体语言证明的“万能 SC-for-DRF 证明”。

直觉 ​

弱内存允许处理器和编译器在没有可观察约束时重排工作；正确同步程序则主动在真正冲突的位置架起顺序边。SC-for-DRF 的交换条件是：程序员用模型规定的同步方式消除普通数据竞争，语言与实现便把复杂重排隐藏在一个可由线程交错解释的表象之后。

这不是说硬件真的逐条执行，也不是说每次运行只有一个结果。它只说允许行为可以找到某个合法 SC 交错作为解释。两把锁的竞争顺序、线程谁先入队或原子操作读到哪个合法值仍可能不同，因而 race-free 与确定性是两回事。

例子与边界 ​

线程 A 在 mutex 保护下写入普通对象 payload 并令 ready = true；线程 B 取得同一把锁后读取 ready，为真才读取 payload。释放与后继获取按语言规则同步，普通写读由 happens-before 排序。即使底层硬件使用写缓冲并执行重排，程序层观察仍可解释为 A 的临界区在 B 的临界区之前，或者 B 先执行并看到 ready == false；不会出现“已经看到 ready 为真，却从普通 payload 读到同步前状态”的任意组合。

把字段都换成 relaxed 原子则给出重要边界。初值 $x=y=0$，线程 P 执行 relaxed x.store(1); r1=y.load()，线程 Q 对称执行 y.store(1); r2=x.load()。所有访问都是原子的，因此没有普通对象 data race；弱模型仍可能允许 $r1=r2=0$，而这个结果无法由保持两线程程序顺序的单一 SC 交错产生。“没有非原子竞争”不足以让所有 relaxed 原子行为自动升级为顺序一致。

动态竞争检测器一次没有报警也不能证明 $P\in {\mathrm{DRF}}_M$。DRF 定义通常量化所有相关执行，罕见调度中的冲突可能从未被测试触发；反过来，基于抽象解释公理库抽象解释Abstract interpretation · Theory of sound static approximation以具体与抽象语义、可靠转移和不动点逼近统一组织静态程序分析的数学框架。的静态分析会用可计算的别名与并发状态近似覆盖执行，其无竞争结论只在抽象域、库摘要和目标模型假设成立时有效。SC-for-DRF 是语义定理，不是一次运行的经验规律。

推论与应用 ​

SC-for-DRF 为并发编程提供模块化契约：大部分业务状态可继续使用普通对象，只在锁、原子和线程生命周期边界上建立模型认可的同步。验证者可以先证明无数据竞争，再在定理覆盖的行为范围内使用熟悉的交错推理；实现者则可在不改变这些观察的前提下优化。

基于 SMT 的软件验证公理库基于 SMT 的软件验证SMT-based software verification · SMT-aided program verification将路径条件、验证条件和理论约束交给 SMT 求解器，以模型或不可满足证明支持软件正确性判断。可核对路径条件、锁纪律和冲突访问的逻辑义务，但必须把别名、线程交错及内存模型规则编码完整。分析工具帮助证明定理前件，不会取代 SC-for-DRF 这一语义蕴涵本身。

使用该出口时必须在结论旁写明语言版本、同步操作集合和原子内存序。本页 C++ 例子只按 N5009 的上述条款解释；未来草案若改变 happens-before 或原子顺序规则，应重新核对而非沿用版本无关的简称。互斥锁公理库互斥锁Mutex · Mutex lock · 互斥量以所有权和阻塞语义封装临界区互斥的同步对象。保护的普通数据常落在经典保证内，手写 relaxed 协议、无锁结构与混合原子/非原子访问则需要直接按模型证明。把“DRF 程序容易推理”扩张为“弱内存程序默认 SC”，恰好抹掉了定理的前提。

参考资料

• ISO/IEC JTC1/SC22/WG21, Working Draft, Programming Languages — C++, N5009, 2025-03-15，[intro.races] 与 [atomics.order]。
• Sarita V. Adve and Mark D. Hill, “Weak Ordering—A New Definition,” ISCA 1990, pp. 2–14。
• Jeremy Manson, William Pugh, and Sarita V. Adve, “The Java Memory Model,” POPL 2005, pp. 378–391。