Bib::mp02
J S. Moore and G. Porter, “The
Apprentice Challenge”, ACM TOPLAS, 24(3), pp. 1-24,
May, 2002.
Relevance: M5 and mutual-exclusion via monitors: an
unbounded number of JVM threads competing for access to a shared resource
———
Abstract
We describe a mechanically checked proof of a property of a small system
of Java programs involving an unbounded number of threads and synchronization
via monitors. We adopt the output of the javac compiler as the
semantics and verify the system at the bytecode level under an operational
semantics for the JVM. We assume a sequentially consistent memory model and
atomicity at the bytecode level. Our operational semantics is expressed in
ACL2, a Lisp-based logic of recursive functions. 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
abstract machine, (ii) the dependencies between Java threads, heap objects,
and synchronization, (iii) the bytecode-level interleaving, (iv) the
unbounded number of threads, (v) the presence in the heap of incompletely
initialized threads and other objects, and (vi) the proof engineering
permitting automatic mechanical verification of code-level theorems. We
discuss these issues. The problem posed here is also put forth as a
benchmark against which to measure other approaches to formally proving
properties of multi-threaded Java programs.
