java - 决定 Java 内存模型的因果关系要求是否容易处理？

Question

Java 语言规范提供了criteria用于确定(格式良好的)执行是否满足“Java 内存模型的因果关系要求”。让我们假设执行是有限的。我试图了解是否存在多项式时间算法来证明或反驳这种情况。

真的，我不是在寻找详细的复杂性理论类型分析，这个问题可以更宽松地解释为:这些因果关系要求实际上是否提供了可应用于实际程序执行的实用定义 - 如果是，如何应用？

的确，the blue box的写法似乎暗示作者确实有一种实用的方法来筛选正式定义中要求的 Action 子集链的空间——我不明白:

The memory model takes as input a given execution, and a program, and determines whether that execution is a legal execution of the program. It does this by gradually building a set of "committed" actions that reflect which actions were executed by the program. Usually, the next action to be committed will reflect the next action that can be performed by a sequentially consistent execution. However, to reflect reads that need to see later writes, we allow some actions to be committed earlier than other actions that happen-before them...
Informally, we allow an action to be committed early if we know that the action can occur without assuming some data race occurs."

如果有人可以将此草图应用到一个简单的示例中 - 那也会非常有帮助。

编辑:有人指出，也许作者想到的是识别器，而不是决策器。我对任何一个都很好 - 整个复杂性角度只是一种询问这个定义是否/如何在实践中应用的方式。

Answer 1

I'm trying to understand if there's a polynomial-time algorithm for proving or disproving that this is the case.

我能找到的最接近的算法是 Verification of the Java Causality Feature作者:S. Polyakov 和 A. Schuster。
该算法用于 java 程序执行跟踪(即程序完成后)。
如果跟踪为每个线程提供读取的提交顺序(这需要一些支持的计算机体系结构支持)，则其复杂度是多项式的。

Indeed, the wording of the blue box seems to imply that the authors did have a practical way of sifting through the space of chains of subsets of actions called for in the formal definition - which I do not understand

蓝框包含 JMM 开发人员在 JMM 因果关系正式模型(位于蓝框正上方的 JLS 中)背后推理的非常浓缩版本。
如果想看更详细通俗易懂的解释，推荐creators of JMM的论文和文章。 : Jeremy Manson、William Pugh、Sarita Adve 和 Doug Lea。
例如这些:

1. The Java Memory Model作者:J. Manson、W. Pugh 和 S. Adve，2005 年。
   一篇不错的短文作为开始。
2. The Java Memory Model作者:J. Manson，博士论文, 2004.
   本文包含最详细的解释。
   论文包括模拟器章节，这是用于JMM验证的。
3. Memory Models: A Case for Rethinking Parallel Languages and Hardware作者:S. Adve 和 H. Boehm，2010 年。
   这是一篇概述论文:
   • 它展示了 JMM 与其他内存模型(在硬件和其他编程语言中)的比较
   • 它讨论了在 5 年的使用过程中发现了 JMM 的优点和缺点
   • 给出了 future 内存模型发展的一些潜在方向