jMT: Testing Correctness of Java Memory Models (Extended Version)

TL;DR

jMT is a new tool for constructing and testing multi-execution semantics of Java memory models, helping validate and compare different JMM proposals and their conformance.

Contribution

It introduces jMT, a novel tool that builds multi-execution semantics from single-execution models to evaluate Java memory models on individual programs.

Findings

Evaluation on 169 litmus tests revealed insights into existing JMMs.

jMT supports testing new JMM proposals and their conformance.

The tool aids in validating and comparing Java memory models.

Abstract

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.