Compiling Volatile Correctly in Java (Artifact)

Authors Shuyang Liu , John Bender, Jens Palsberg



PDF
Thumbnail PDF

Artifact Description

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

Document Identifiers

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

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 AsGet 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

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

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