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. © Springer-Verlag Berlin Heidelberg 2006.
CITATION STYLE
Polyakov, S., & Schuster, A. (2006). Verification of the java causality requirements. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3875 LNCS, pp. 224–246). https://doi.org/10.1007/11678779_16
Mendeley helps you to discover research relevant for your work.