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`

.

- the M4 version of the apprentice proof (95 KB gzipped postscript)
- a paper about the M4 model (71 KB gzipped postscript)
- Apprentice in Java (600 bytes!)
`the M4 model in ACL2 (4 KB)`

`the ACL2 proof script for M4 Apprentice (60 KB)`

```
```