The Apprentice Challenge

J Strother Moore
George Porter

We have an ACL2 model of the Java Virtual Machine and have used it to prove a theorem about a small Java application involving an unbounded number of threads and synchronization via monitors. The JVM model is named M5 and 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 javac 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.

Supporting Files