Document Open Access Logo

Compiling Volatile Correctly in Java

Authors Shuyang Liu , John Bender, Jens Palsberg

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2022.6.pdf
  • Filesize: 1.24 MB
  • 26 pages

Document Identifiers

Related Versions

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. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 6:1-6:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ECOOP.2022.6

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.

Supplementary Materials

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.
  2. ARM ARM. Architecture reference manual-armv8, for armv8-a architecture profile. ARM Limited, Dec, 2017. Google Scholar
  3. John Bender and Jens Palsberg. A formalization of java’s concurrent access modes. Proc. ACM Program. Lang., 3(OOPSLA), October 2019. URL: https://doi.org/10.1145/3360568.
  4. Peter Sewell Jaroslav Sevcik. C/C++11 mappings to processors. Technical report, University of Cambridge, October 2016. URL: https://www.cl.cam.ac.uk/~pes20/cpp/cpp0xmappings.html.
  5. Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, and Viktor Vafeiadis. Making weak memory models fair. Proc. ACM Program. Lang., 5(OOPSLA), October 2021. URL: https://doi.org/10.1145/3485475.
  6. Ori Lahav, Viktor Vafeiadis, Jeehoon Kang, Chung-Kil Hur, and Derek Dreyer. Repairing sequential consistency in C/C++11. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2017, pages 618-632, New York, NY, USA, 2017. Association for Computing Machinery. URL: https://doi.org/10.1145/3062341.3062352.
  7. L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Trans. Comput., 28(9):690-691, September 1979. URL: https://doi.org/10.1109/TC.1979.1675439.
  8. Doug Lea. The jsr-133 cookbook for compiler writers. http://gee.cs.oswego.edu/dl/jmm/cookbook.html, 2011. Last modified: Tue Mar 22 07:11:36 2011.
  9. Doug Lea. Using jdk 9 memory order modes. http://gee.cs.oswego.edu/dl/html/j9mm.html, 2018. Last Updated: Fri Nov 16 08:46:48 2018.
  10. Lun Liu, Todd Millstein, and Madanlal Musuvathi. A volatile-by-default jvm for server applications. Proc. ACM Program. Lang., 1(OOPSLA), October 2017. URL: https://doi.org/10.1145/3133873.
  11. Yatin A Manerkar, Caroline Trippel, Daniel Lustig, Michael Pellauer, and Margaret Martonosi. Counterexamples and proof loophole for the c/c++ to power and armv7 trailing-sync compiler mappings. arXiv preprint arXiv:1611.01507, 2016. Google Scholar
  12. Jeremy Manson, William Pugh, and Sarita V. Adve. The java memory model. SIGPLAN Not., 40(1):378-391, January 2005. URL: https://doi.org/10.1145/1047659.1040336.
  13. Christopher Pulte, Shaked Flur, Will Deacon, Jon French, Susmit Sarkar, and Peter Sewell. Simplifying arm concurrency: Multicopy-atomic axiomatic and operational models for armv8. Proc. ACM Program. Lang., 2(POPL), December 2017. URL: https://doi.org/10.1145/3158107.
  14. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding power multiprocessors. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, pages 175-186, New York, NY, USA, 2011. Association for Computing Machinery. URL: https://doi.org/10.1145/1993498.1993520.
  15. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. X86-tso: A rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7):89-97, July 2010. URL: https://doi.org/10.1145/1785414.1785443.
  16. Aleksey Shipilev. jcstress - the java concurrency stress tests. https://wiki.openjdk.java.net/display/CodeTools/jcstress, 2017. Last Updated: Wed Dec 05 13:55 2018.
  17. Aleksey Shipilev. [JDK-8262877] PPC sequential consistency problem: volatile stores are too weak. Technical report, OpenJDK Bug System, March 2021. URL: https://bugs.openjdk.java.net/browse/JDK-8262877.
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