License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DARTS.8.2.3
URN: urn:nbn:de:0030-drops-162018
URL: https://drops.dagstuhl.de/opus/volltexte/2022/16201/
Go back to Dagstuhl Artifacts Series


Liu, Shuyang ; Bender, John ; Palsberg, Jens

Compiling Volatile Correctly in Java (Artifact)

pdf-format:
DARTS-8-2-3.pdf (0.6 MB)
artifact-format:
DARTS-8-2-3-artifact-68b11fb27dbd97fbe5d9588b133d9658.zip (1 MB)

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.

BibTeX - Entry

@Article{liu_et_al:DARTS.8.2.3,
  author =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  title =	{{Compiling Volatile Correctly in Java (Artifact)}},
  pages =	{3:1--3:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2022},
  volume =	{8},
  number =	{2},
  editor =	{Liu, Shuyang and Bender, John and Palsberg, Jens},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16201},
  URN =		{urn:nbn:de:0030-drops-162018},
  doi =		{10.4230/DARTS.8.2.3},
  annote =	{Keywords: formal semantics, concurrency, compilation}
}

Keywords: formal semantics, concurrency, compilation
Collection: DARTS, Volume 8, Issue 2, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022)
Issue Date: 2022
Date of publication: 23.06.2022


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI