This paper is a first step at developing an executable abstract formal model of threading in the JVM. We have explained how such a model can be built, we have shown that the model can be executed on concrete data to test the behavior of methods and threads under various scheduling regimes, and we have illustrated that it is possible to prove theorems about all possible behaviors. These proofs can be checked mechanically by ACL2, a general-purpose theorem proving engine. This engine was not designed with JVM proofs in mind; indeed, all the engine ``knows'' about the model is its formal definition. Our proofs of the theorems cited were straightforward applications of general techniques understood well by the ACL2 community. Further investigation of such theorems would undoubtedly lead to the codification of JVM-specific proof techniques and formal metatheorems, such as that syntactically non-interfering threads can be analyzed separately.
The prover is sufficiently powerful to be of use in verifying microprocessor architectures and floating-point implementations. While our JVM model is currently quite simple compared to the implemented JVM, past experience with ACL2 supports the hope that ACL2 will be capable of handling significantly more realistic models of the JVM.
If our past experience is any guide, the formalization of proof techniques for a realistic model of the JVM will make it easier to reason formally about the JVM and Java. In addition, such an undertaking will most likely expose oversights or ambiguities in existing informal understandings of how to write correct and reliable Java programs.