Happens-before 关系

Happens-before 记录可证明的信息流。程序顺序让同一线程的前一步影响后一步，消息接收携带发送之前的知识，同步操作把一个线程先前的写入交给另一个线程。传递闭包再把这些局部证据串成跨线程、跨节点的因果链。

它不是物理时间轴。两个事件即使在测量上先后相隔很久，只要模型没有程序、通信或同步路径，仍可能不可比；反过来，某些语言允许编译器重排机器指令，却仍要求抽象执行保持规定的 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 不能跨语言模型自行补边。

语言模型还可能规定单个原子位置的 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。偏序约简还要求动作独立与交换，不能仅从两个事件无因果路径就推出交换执行保持所有观察。