同步边的充分集为何唯一？如何构建该集合？

JLS定义引用 #

若同步边集合S是满足以下条件的最小集合：S与程序顺序的传递闭包可确定执行中的所有先行发生（happens-before）边，则该集合S是充分集，且该集合是唯一的。

1. 同步边充分集为何具有唯一性？ #

充分集的核心要求是最小性——不存在任何真子集能满足“和程序顺序传递闭包共同确定所有happens-before边”的条件。

假设存在两个不同的充分集S₁和S₂，那么必然存在元素e₁∈S₁但e₁∉S₂。因为S₂是充分集，说明仅靠S₂加程序顺序的传递闭包就能推导出所有happens-before关系，包括e₁对应的那组关系。这就意味着S₁去掉e₁之后，依然能满足充分集的条件，直接和S₁是“最小集合”的定义矛盾。同理，S₂也不可能存在这样的元素。因此，满足最小性要求的充分集只能有一个。

本质上，最小性的约束直接排除了存在多个不同充分集的可能——任何额外的、非必需的同步边都会让集合失去“最小”属性，而缺少必需边的集合又无法覆盖所有happens-before关系。

2. 如何判断同步边是否属于充分集？ #

判断的关键是看这条同步边是否是推导完整happens-before关系的必需项：如果移除这条边后，仅靠剩余同步边加程序顺序的传递闭包，无法推导出原本存在的某条happens-before关系，那么它就属于充分集；反之则是冗余边，不属于充分集。

具体步骤可以这样做：

• 先基于程序的所有同步边和程序顺序，推导出完整的happens-before关系图。
• 对每条同步边逐一测试：移除该边后，重新推导所有可能的happens-before关系。
  • 如果推导结果缺失了原关系图中的某条边，说明这条同步边是必需的，属于充分集。
  • 如果推导结果和原关系图完全一致，说明这条同步边是冗余的，不属于充分集。

举个实际场景：线程A释放锁L，线程B获取锁L，这条同步边是必需的——没有它，跨线程的A操作happens-before B操作的关系就无法通过程序顺序推导出来。但如果同时存在A释放L₁→B获取L₁、A释放L₂→B获取L₂两条同步边，且两者都能推导出A操作happens-before B操作，那么其中一条就是冗余的——移除后另一条依然能完成推导，所以这条冗余边不属于充分集。

内容的提问来源于stack exchange，提问作者cata