LIPIcs.ECOOP.2022.6.pdf
- Filesize: 1.24 MB
- 26 pages
Document
Compiling Volatile Correctly in Java
Authors
Shuyang Liu 
,
-
Part of:
Volume:
36th European Conference on Object-Oriented Programming (ECOOP 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: European Conference on Object-Oriented Programming (ECOOP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-06-23
File
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 AsGet 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
https://doi.org/10.4230/LIPIcs.ECOOP.2022.6
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.
-
ARM ARM. Architecture reference manual-armv8, for armv8-a architecture profile. ARM Limited, Dec, 2017.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
-
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.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.