为何顺序一致执行无数据竞态即可保证所有执行无数据竞态？

根据Java内存模型（JMM）的定义：

当且仅当所有顺序一致执行均无数据竞态时，程序是正确同步的。
若程序正确同步，则程序的所有执行都会表现为顺序一致（§17.4.3）。

我无法理解为何所有顺序一致（SC）执行无数据竞态就能保证所有执行都无数据竞态（即所有执行均为SC），是否存在相关证明？

我找到的资料 #

• JMM设计者的博客内容：作者是JMM的设计者之一Jeremy Manson，以下段落似乎表明该保证由因果性提供，但我无法理解其原理：

  这就是该模型背后的直觉。当你要证明某读取操作返回某写入操作的值时，若满足以下条件即可：
  a) 该写入操作先行发生于读取操作，或
  b) 你已经证明了该写入操作的合理性。
  模型的工作方式是：从所有操作均由属性a)证明合理性的执行开始，逐步迭代证明操作的合理性。比如在上文的第二个示例中，你会生成一系列执行，依次证明0、2、3、4、1的合理性。
  该定义具备相当直观且能保证无数据竞态（DRF）程序符合顺序一致性（SC）的优良特性。

• 《C++并发内存模型基础》报告内容：这篇文章介绍了与JMM相似的C内存模型，第8节针对C给出了类似保证的证明：

  定理8.1. 若程序在某一致执行中存在2类数据竞态，则存在一个顺序一致执行，其中包含两个冲突操作，且二者均不先行发生于对方。⁸
  实际上，我们只需查看顺序一致执行，即可判断某一致执行中是否存在数据竞态。
  [...]
  ⁸后者本质上是[25]中定义Java“正确同步”所使用的条件。

  但我不确定该证明是否适用于JMM，因为以下推论在JMM中不成立：

  考虑*_T的最长无数据竞态前缀P*。注意P中的每个加载操作必须看到同步顺序或先行发生顺序中位于其之前的存储操作。

  在我看来，上述推论在JMM中不成立，因为因果性允许读取操作返回后续存储操作的值。

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