Verification of the Java Causality Requirements

摘要

The Java Memory Model (JMM) formalizes the behavior of shared memory accesses in a multithreaded Java program. Dependencies between memory accesses are acyclic, as defined by the JMM causality requirements. We study the problem of post-mortem verification of these requirements and prove that the task is NP-complete. We then argue that in some cases the task may be simplified either by considering a slightly stronger memory model or by tracing the actual execution order of Read actions in each thread. Our verification algorithm has two versions: a polynomial version, to be used when one of the aforementioned simplifications is possible, and a non-polynomial version - for short test sequences only - to be used in all other cases. Finally, we argue that the JMM causality requirements could benefit from some fine-tuning. Our examination of causality test case 6 (presented in the public discussion of the JMM) clearly shows that some useful compiler optimizations - which one would expect to be permissible - are in fact prohibited by the formal model.