Happens-before 关系

Happens-before 记录模型允许的信息影响路径。程序顺序让同一线程的前一步有机会影响后一步，消息接收携带发送之前的信息，同步操作把一个线程先前的写入交给另一个线程。传递闭包再把这些局部证据串成跨线程、跨节点的因果链。存在路径不要求后一个事件真的在业务上使用了前一个结果；即使接收者丢弃消息，发送—接收边仍存在。

判断关系时可先画基本边，再沿箭头寻找路径；找得到从 $a$ 到 $b$ 的路径就有 $a{<}_{\mathrm{hb}}b$，两个方向都找不到才叫并发。只检查二者之间是否有一条直接消息会漏掉经第三个进程中转的传递依赖。

它不是物理时间轴。两个事件即使在测量上先后相隔很久，只要模型没有程序、通信或同步路径，仍可能不可比；反过来，某些语言允许编译器重排机器指令，却仍要求抽象执行保持规定的 happens-before。分析必须始终说明关系属于哪一层。

消息执行中，进程 $P$ 先执行 $a$，再发送 $m$；进程 $Q$ 接收 $m$ 后执行 $b$，于是

故 $a{<}_{\mathrm{hb}}b$。若进程 $R$ 独立执行 $c$，且没有消息链把 $c$ 与 $b$ 相连，则 $b,c$ 不可比；日志系统可以选择先显示任一个，但不应把所选顺序冒充因果事实。

共享内存中，线程 $P$ 先普通写 data = 42，再以 release 语义写 ready = true；线程 $Q$ 的 acquire 读若从这次 ready 写取得 true，便有

所以数据写 happens-before 数据读。若 acquire 读没有观察该 release 写，或 ready 只是普通变量，所需 synchronizes-with 边可能不存在；仅凭读到了数值 true 不能跨语言模型自行补边。

发布例还要求 ready 是模型认可的原子同步对象，且载荷读写没有其他未排序的冲突访问。如果另一个线程在发布后继续无同步改写 data，上面的四条边并不会顺便排序这次新写；一次发布只保障对应的既有信息，不会永久冻结对象。

若发布的是替代旧配置的新指针，发布正确还不足以立即释放旧配置。RCU公理库Read-Copy UpdateRCU · Read-copy update先发布完整新版本，再等待相关旧读侧区间结束，以分离共享更新和旧对象回收。把发布与回收分成两步：先使后续读者能取得新版本，再等覆盖原有读区间的宽限期结束。仍持有旧指针的读者何时退出，是与新版本可见性不同的证明义务。

语言模型还可能规定单个原子位置的 modification order、Java 同步动作的 synchronization order，或所有顺序一致原子的某个总序。这些附加次序不等于 happens-before 本身；只有规范指定的边才参与生成 ${<}_{\mathrm{hb}}$。同样，给日志任意选择一个全序只是偏序的线性扩张，不会把原本并发的事件变成因果相关。

Lamport 时钟公理库逻辑时钟Logical clock · Lamport clock为事件赋整数时间戳并保证因果先后蕴含时间戳递增。保证 $a{<}_{\mathrm{hb}}b$ 时标量时间递增，但逆命题不成立；向量时钟公理库向量时钟Vector clock用每进程计数向量在标准消息传递模型中精确刻画事件因果偏序。在固定成员、可靠事件传播等标准假设下可精确判定偏序。一致切片公理库一致切片Consistent cut · Consistent global cut对事件因果前驱向下闭合、因而可解释为分布式全局状态的执行切片。取 happens-before 的向下闭集，因果广播公理库因果广播Causal broadcast保证所有进程按因果先后顺序交付消息的广播抽象。则让交付顺序保持消息因果。

数据竞争公理库数据竞争Data race · 数据竞态不同线程对同一内存位置的冲突访问既未按模型同步排序、也未通过原子操作协调的情形。用模型特定的 happens-before 判断冲突普通访问是否未排序；不可比的只读访问却不会因此成为 race。偏序约简还要求动作独立与交换，不能仅从两个事件无因果路径就推出交换执行保持所有观察。