M5and the Java application is called Apprentice. The Apprentice problem is also put forth as a benchmark against which to measure other approaches to formally proving properties of multi-threaded Java programs.
To prove Apprentice correct, we adopt the output of the
compiler as the semantics of Java and verify the system at the bytecode level
under the M5 operational semantics for the JVM. We assume a sequentially
consistent memory model and atomicity at the bytecode level.
Our proofs are checked with the ACL2 theorem prover. The proof involves
reasoning about arithmetic, infinite loops, the creation and modification of
instance objects in the heap, including threads, the inheritance of fields
from superclasses, pointer chasing and smashing, the invocation of instance
methods (and the concomitant dynamic method resolution), use of the
start method on thread objects, the use of monitors to attain
synchronization between threads, and consideration of all possible
interleavings (at the bytecode level) over an unbounded number of threads.
Readers familiar with monitor-based proofs of mutual exclusion, will recognize our proof as fairly classical. The novelty here comes from (i) the complexity of the individual operations on the machine, (ii) the dependencies between Java threads, heap objects, and synchronization, (iii) bytecode-level interleaving, (iv) the unbounded number of threads, and (v) and proof engineering permitting ``automatic'' mechanical verification. We discuss these issues.