Java语言规范提供了确定(良好形式的)执行是否满足"；Java内存模型的因果关系要求"；。让我们假设执行是有限的。我试图了解是否有多项式时间算法来证明或反驳这种情况。
实际上，我不是在寻找详细的复杂性理论类型分析，这个问题可以更松散地解释为：这些因果关系要求是否真的提供了一个实用的定义，可以应用于实践中的程序执行？如果是，如何
事实上，蓝框的措辞似乎意味着作者确实有一种实用的方法来筛选正式定义中要求的行动子集的链空间——我不理解：
内存模型将给定的执行和程序作为输入，并确定该执行是否是程序的合法执行。它通过逐渐建立一套"；承诺"；反映程序执行了哪些操作的操作。通常，要提交的下一个操作将反映可由顺序一致执行执行的下一操作。然而，为了反映需要看到后续写入的读取，我们允许某些操作比之前发生的其他操作更早提交
非正式地说，如果我们知道某个操作可以发生，而不假设发生了某些数据竞争，我们就允许提前提交该操作">
如果有人能把这个草图应用到一个简单的例子中，那也会很有帮助。
编辑：有人指出，也许作者心中有一个识别者，而不是决策者。我对这两者都很在行——整个复杂性角度只是询问这个定义是否/如何在实践中应用的一种方式。
我试图了解是否有多项式时间算法来证明或反驳这种情况
我能找到的最接近的东西是S.Polyakov和A.Schuster在《Java因果关系特征的验证》中的一个算法
该算法用于java程序执行跟踪(即程序完成后)
如果跟踪为每个线程提供Reads的承诺顺序(这需要一些支持计算机体系结构支持)，则其复杂性是多项式。
事实上，蓝框的措辞似乎意味着作者确实有一种实用的方法来筛选形式定义中要求的行动子集的链空间——我不理解
蓝框包含JMM开发人员在JMM因果关系的形式模型(位于蓝框正上方的JLS中)背后的推理的浓缩版本
如果你想看到更详细、更容易理解的解释，那么我推荐JMM的创作者Jeremy Manson、William Pugh、Sarita Adve和Doug Lea的论文和文章
例如：
- J.Manson、W.Pugh和S.Adve的《Java内存模型》，2005年。
一篇不错的短文 - J.Manson的Java内存模型，博士论文，2004。
本文包含了最详细的解释
本文包括关于模拟器的章节，这是用于JMM验证的模拟器 - 《内存模型：重新思考并行语言和硬件的案例》，S.Adve和H.Boehm著，2010。
这是一篇综述性论文：- 它展示了JMM与其他内存模型(在硬件和其他编程语言中)的比较
- 它讨论了JMM在使用的5年中发现了哪些优点和缺点
- 它给出了未来内存模型开发的一些潜在方向
为了补充上述答案，2008年的另一篇论文演示了Java因果关系特征验证提出的算法不能在多项式时间内完成的情况。
本文是Java中因果关系需求的验证Matko Botin、Paola Glavan和Davor Runje的《记忆模型是无法解释的》
论文结论：
验证JMM的问题任意Java程序的有限执行的因果关系要求是不可判定的。
简而言之，作者注意到原始论文隐含地假设所有用于证明的中间执行都是有限的和多项式有界的
但在现实中，这并不总是正确的，这已经通过例子证明了。
该示例可以简化为以下内容
程序：
Initially: y = 0, x = 0
Thread1 | Thread2
-----------------------------
y = x; | S;
| x = 1;
S是一个任意的顺序程序，它不访问x和y
我们需要验证的执行会产生结果y == 1
理由：
- 为了得到结果
y == 1，应该首先提交x = 1; - 只有当
S不无限执行时，才能提交x = 1;
来自JLS：执行可能导致线程被无限期阻塞，并且执行不会终止。在这种情况下，被阻止的线程生成的操作必须包括该线程在导致线程被阻止之前生成的所有操作(包括导致线程被阻塞的操作)，并且在该操作之后线程不会生成任何操作。
- 判断
S是否无限执行是不可判定的，因为这是一个停顿问题
是的，我认为这是可能的。
算法接受执行作为输入，如果执行有效(即满足因果关系要求)，则输出true，否则输出false
它通过提交由程序根据9条规则执行的逐步操作来工作
如果所有操作都可以提交，则执行有效。
就我个人而言，我会尝试向后实现该算法：它将从完全执行开始，然后不断删除操作，直到没有剩余的操作为止
我不是100%确定，但似乎在每一步都足以测试是否删除每个线程中的最后一个操作
这在多项式时间内应该是可能的。
在实践中，最常见的问题可能是：如何记录执行
例如，对于每次读取，执行都应存储相应的写入操作，写入读取返回的值
我不认为OpenJDK提供此功能
我的猜测是，像Java Pathfinder和Lincheck这样的Java模型检查工具可能能够做到这一点。
附言：这里是一个如何将算法应用于执行的示例。
您可能想看看Andreas Lochbihler在http://www.andreas-lochbihler.de/
特别是在他的博士论文中，你可以找到：
在本文中，我为Java源代码和字节码构建了一个名为JinjaThreads的Java并发性机器检查模型
与前代产品一样，JinjaThreads省略了Java中的一些顺序功能，以保持的易处理性