数据竞争

Data race 检查的是一对具体访问：它们是否碰到同一位置、是否冲突、是否至少一方非原子，以及模型能否证明顺序。线程数很多、结果偶尔变化或 CPU 同时运行，都不是定义条件。

锁与 release/acquire 向历史加入 happens-before 边，原子类型则改变访问本身的冲突规则。二者都能让特定访问对不再是 data race，却通过不同机制工作；把字段换成 atomic 不会自动把由多次访问组成的事务变成单一步骤。

从普通整数 x = 0 开始，两个线程都执行 x = x + 1。若两边先读到 $0$，再各写 $1$，冲突读写之间没有 happens-before，构成 data race。$x=1$ 只是源码级丢失更新的一种图像；在 C/C++ 中不能据此断言结果只可能是 $1$ 或 $2$，因为程序已越过语言定义行为的边界。

若两段更新都在同一互斥锁下，线程 $P$ 的普通写先于 unlock，该解锁 synchronizes-with 线程 $Q$ 随后的成功 lock，而锁又先于 $Q$ 的访问。传递性给出 $P$ 的访问 happens-before $Q$ 的访问，因此不存在这对 data race。证明依赖的是锁语义生成边，不是临界区“看起来不会同时运行”。

若线程 A 只写 array[0]，线程 B 只写 array[1]，两个元素在语言对象模型中是不同内存位置，则并发写本身不构成 data race。仍可能出现 false sharing，引发缓存行抖动和性能下降；性能共享单元与语言定义的冲突位置是两个层次，不能因为硬件缓存行相同就把访问改判为数据竞争。

再看全原子的检查—行动逻辑：两个线程各自原子读取 balance >= 100，若为真再原子扣除 $100$。每个单次访问都合法原子，因此没有普通对象 data race；两者却可能同时通过检查，使余额越过业务下界。这是 race condition：复合操作缺少整体线性化。CAS 循环、锁或事务要解决的是这一更高层问题。

动态 race detector 依据一次运行观察到的访问与同步关系报告冲突；未报告只说明这条执行未命中。静态类型、所有权系统与分离逻辑公理库分离逻辑Separation logic以分离合取表达互不重叠资源并局部推理堆内存的程序逻辑。能在各自假设下覆盖所有执行，但还需证明其抽象与目标语言内存模型对应。

无数据竞争程序在某些语言中获得接近顺序一致性公理库顺序一致性Sequential consistency共享内存中的读写操作可排成保持各线程程序顺序并解释所有读值的单一全序。的语义，是额外的 SC-for-DRF 定理，其前提、原子操作范围和保证随模型变化。数据竞争定义页只负责刻画冲突；它不把模型特定的定理偷渡成无条件结论，也不把“race-free”夸大为程序结果唯一。