Folklore is often saying "The Java memory model is broken." Therefore, several approaches have proposed repairs, only to find new programs exhibiting unexpected, unintuitive behavior or the model forbidding standard compiler optimizations. The complexity of defining a memory model for concurrent Java lies in the fact that it requires a multi-execution model. Multi-execution models need to inspect the many potential executions of a program in order to find the valid ones. Tools automatically validating novel proposals of Java memory models are, however, largely lacking. To alleviate this problem, we introduce jMT, a novel tool for constructing multi-execution semantics for concurrent Java programs. jMT relies on single-execution models defining well-formed execution graphs, based on which it builds valid multi-execution semantics via causality checking. Thereby, jMT supports evaluating new proposals of Java memory models (JMMs) on a per-program basis. jMT can furthermore be employed for testing the conformance of JMMs to existing compilation schemes and compilers. Our evaluation of jMT on 169 litmus tests reveals a number of interesting insights into existing JMMs.

翻译：民间常言“Java内存模型存在缺陷”，因此已有多种修复方案被提出，但这些方案要么导致新程序出现非预期且反直觉的行为，要么禁止标准编译器优化。并发Java内存模型的定义复杂性源于其需要多执行模型（multi-execution model），这类模型需检查程序的多重潜在执行序列以识别有效执行路径。然而，目前严重缺乏能自动验证新型Java内存模型提案的工具。为解决这一问题，我们提出jMT——一种为并发Java程序构建多执行语义的新工具。jMT基于定义良好执行图的单执行模型，通过因果性检查构建有效的多执行语义。由此，jMT支持在逐程序基础上评估Java内存模型（JMM）的新提案，并可用于测试JMM与现有编译方案及编译器的符合性。通过对169个litmus测试的评估，jMT揭示了现有JMM中若干有趣的洞见。