Verification of the java causality requirements

2Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free