DARTS.8.2.3.pdf
- Filesize: 0.56 MB
- 2 pages
Document
Compiling Volatile Correctly in Java (Artifact)
Authors
Shuyang Liu 
,
-
Part of:
Issue:
Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Volume: DARTS, Volume 8 (ECOOP 2022)
Conference: European Conference on Object-Oriented Programming (ECOOP)
Journal: Dagstuhl Artifacts Series (DARTS) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-06-23
Artifact Description
Document Identifiers
Author Details
Acknowledgements
We thank Doug Lea for the helpful insights on the Java language semantics and compilers; we thank Jade Alglave for her precious and detailed help on implementing Java architecture for Herd; we thank Ori Lahav, Anton Podkopaev and Viktor Vafeiadis for initially pointing out the issue of the Java Access Modes model; we thank all the reviewers of ECOOP'22 for their insightful feedback.
Cite As Get BibTex
Shuyang Liu, John Bender, and Jens Palsberg. Compiling Volatile Correctly in Java (Artifact). In Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022). Dagstuhl Artifacts Series (DARTS), Volume 8, Issue 2, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/DARTS.8.2.3
Artifact
DARTS-8-2-3-artifact-68b11fb27dbd97fbe5d9588b133d9658.zip
(Filesize: 1.4 MB)
MD5 Sum:
68b11fb27dbd97fbe5d9588b133d9658
(Get MD5 Sum)
Artifact Evaluation Policy
The artifact has been evaluated as described in the ECOOP 2022 Call for Artifacts and the ACM Artifact Review and Badging Policy
Abstract
The compilation scheme for Volatile accesses in the OpenJDK 9 HotSpot Java Virtual Machine has a major problem that persists despite a recent bug report and a long discussion. One of the suggested fixes is to let Java compile Volatile accesses in the same way as C/C++11. However, we show that this approach is invalid for Java. Indeed, we show a set of optimizations that is valid for C/C++11 but invalid for Java, while the compilation scheme is similar. We prove the correctness of the compilation scheme to Power and x86 and a suite of valid optimizations in Java. Our proofs are based on a language model that we validate by proving key properties such as the DRF-SC theorem and by running litmus tests via our implementation of Java in Herd7.
Subject Classification
ACM Subject Classification
- Software and its engineering → Semantics
Keywords
- formal semantics
- concurrency
- compilation
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Jade Alglave, Luc Maranget, and Michael Tautschnig. Herding cats: Modelling, simulation, testing, and data mining for weak memory. ACM Trans. Program. Lang. Syst., 36(2), July 2014. URL: https://doi.org/10.1145/2627752.