Document Open Access Logo

Compiling Volatile Correctly in Java (Artifact)

Authors Shuyang Liu , John Bender, Jens Palsberg

PDF

Artifact Description

Thumbnail PDF
PDF
DARTS.8.2.3.pdf
  • Filesize: 0.56 MB
  • 2 pages

Document Identifiers

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)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

Shuyang Liu
  • University of California, Los Angeles, CA, USA
John Bender
  • Sandia National Laboratories, Albuquerque, NM, USA
Jens Palsberg
  • University of California, Los Angeles, CA, USA

Funding

This material is based upon work supported by the National Science Foundation under Grant No. 1815496.

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.

Artifact

  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

Related Article

  • Shuyang Liu, John Bender, and Jens Palsberg, "Compiling Volatile Correctly in Java", in 36th European Conference on Object-Oriented Programming (ECOOP 2022), LIPIcs, Vol. 222, pp. 6:1-6:26, 2022. https://doi.org/10.4230/LIPIcs.ECOOP.2022.6

References

  1. 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.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact