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.

- the paper (255 KB postscript)
- the M5 model (100 KB)
- Apprentice in Java (600 bytes!)
`the ACL2 for the initial state (4.5 KB)`

`the ACL2 proof script (96 KB)`

```
```