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.
Thu 23 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
Thu 23 Jun
Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:45 - 18:15 | |||
16:45 30mTalk | Vincent: Green Hot Methods in the JVMVCOOP 2022 Research Papers Kenan Liu SUNY Binghamton, Khaled Mahmoud SUNY Binghamton, USA, Joonhwan Yoo SUNY Binghamton, Yu David Liu SUNY Binghamton Pre-print | ||
17:15 30mTalk | Verified Compilation and Optimization of Floating-Point Programs in CakeML Research Papers Heiko Becker MPI-SWS, Robert Rabe TU Munich, Eva Darulova Uppsala University, Magnus O. Myreen Chalmers University of Technology, Zachary Tatlock University of Washington, Ramana Kumar DeepMind, Yong Kiam Tan Carnegie Mellon University, Anthony C. J. Fox Arm Limited | ||
17:45 30mTalk | Compiling Volatile Correctly in Java Research Papers Shuyang Liu UCLA, John Bender Sandia National Laboratories, Jens Palsberg University of California at Los Angeles | ||