A JVM Thread Model in ACL2

J Strother Moore
George Porter

We present a formal operational semantics for a machine very similar to the Java Virtual Machine. The model is called M4 and supports the ``bytecode'' operands PUSH, POP, LOAD, STORE, ADD, SUB, MUL, GOTO, IFEQ, IFLT, IFGT, INVOKEVIRTUAL, RETURN, XRETURN, NEW, GETFIELD, PUTFIELD, MONITORENTER, and MONITOREXIT. Most of these instructions represent entire families of actual JVM instructions of similar names. Arithmetic on M4 is unbounded. Our M4 provides an interleaved semantics for thread execution, with individual bytecodes being atomic. We assume a sequentially consistent memory model. It was in this paper that we introduced the so-called ``Apprentice problem''. As presented here, the Apprentice class spawns an an unbounded number of threads in contention for a single unbounded counter. Using the M4 model and ACL2 we proved that the counter increases monotonically, e.g., that mutual exclusion is achieved between the competing threads. This paper describes Apprentice but not the proof.

Since the presentation of this paper at JVM'01 in Monterey, CA (April, 2001), we have elaborated the model to M5 which supports true JVM bounded arithemtic and 138 actual bytecode opcodes. This M4 paper is a good introduction to the M5 model because it describes how we go about defining operational models of this sort and how we prove theorems about them. But the M4 is much less similar to the JVM than the M5 is. The M5 work includes an a realistic treatment of the Apprentice problem, by proving that the int counter wraps appropriately. The bytecode verified is that produced by javac on the Java source for Apprentice.

Supporting Files