问题描述
Java 语言规范提供了 criteria，用于确定（格式良好的）执行是否满足“Java 内存模型的因果关系要求”。让我们假设执行是有限的。我试图了解是否有多项式时间算法来证明或反驳这种情况。
真的，我不是在寻找详细的复杂性理论类型分析，这个问题可以更宽松地解释为： 这些因果关系要求是否真的提供了一个实用的定义，可以应用于实践中的程序执行——如果是，如何实现？
确实，the blue box 的措辞似乎暗示作者确实有一种实用的方法来筛选正式定义中要求的动作子集链的空间 - 我不明白：>
内存模型将给定的执行和程序作为输入，并确定该执行是否是程序的合法执行。它通过逐渐构建一组反映程序执行了哪些操作的“已提交”操作来实现这一点。通常，要提交的下一个操作将反映可以由顺序一致执行执行的下一个操作。但是，为了反映需要看到稍后写入的读取，我们允许某些操作比其他发生在它们之前的操作更早提交...
非正式地，如果我们知道可以在不假设发生某些数据竞争的情况下执行该操作，则我们允许提前提交该操作。”
如果有人可以将此草图应用到一个简单的示例中 - 那也会非常有帮助。
编辑： 有人指出，也许作者想到的是识别器，而不是决定器。我对两者都很好 - 整个复杂性角度只是询问是否/如何在实践中应用此定义的一种方式。
解决方法
我试图了解是否有多项式时间算法来证明或反驳这种情况。
我能找到的最接近的是 S. Polyakov 和 A. Schuster 在 Verification of the Java Causality Feature 中的算法。
该算法用于java程序执行跟踪（即程序完成后）。
如果跟踪为每个线程提供读取的提交顺序（这需要一些支持计算机架构的支持），则其复杂性是多项式的。
确实，the blue box 的措辞似乎暗示作者确实有一种实用的方法来筛选正式定义中要求的动作子集链的空间 - 我不明白
蓝色框包含 JMM 开发人员对 JMM 因果关系正式模型（位于蓝色框正上方的 JLS）背后的推理的非常精简版本。
如果您想查看更详细且易于理解的解释，那么我会推荐 creators of JMM 的论文和文章：Jeremy Manson、William Pugh、Sarita Adve 和 Doug Lea。
例如这些：
-
The Java Memory Model 作者：J. Manson、W. Pugh 和 S. Adve，2005 年。
一篇不错的短论文。 -
The Java Memory Model 作者：J. Manson，博士论文，2004.
这篇论文包含了最详细的解释。
论文包括关于模拟器的章节，这是用于 JMM 验证的内容。 -
Memory Models: A Case for Rethinking Parallel Languages and Hardware 作者：S. Adve 和 H. Boehm，2010 年。
这是一篇综述论文：- 它展示了 JMM 与其他内存模型（硬件和其他编程语言）的比较
- 它讨论了在使用 JMM 的 5 年中发现的强弱方面
- 它给出了未来记忆模型发展的一些潜在方向