Specifying multithreaded Java semantics for program verification

Most current work on multithreaded Java program verification assumes a model of execution that is based on interleaving of the operations of the individual threads. However, the Java language specification supports a weaker model of execution, called the Java Memory Model (JMM). The JMM allows certain reordering of operations within a thread and thus permits more behaviors than the interleaving based execution model. Therefore, programs verified by assuming interleaved thread execution may not behave correctly for certain Java multithreading implementations. The main difficulty with the JMM is that it is informally described in an abstract rule-based declarative style, which is unsuitable for formal verification. We develop an equivalent formal executable specification of the JMM. Our specification is operational and uses guarded commands. We then use this executable model to verify popular software construction idioms for multithreaded Java. Our prototype verifier tool detects a bug in the widely used "Double Checked Locking" idiom, which verifiers based on interleaving execution model cannot possibly detect.