Description: Writings on computer stuff.
More posts can be found in the archive .
This is a somewhat narrow introduction to formal methods I presented at UCLA in March of 2022 with the goal of describing some of my research at Sandia.
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 P