Specification of the JVM

In ACL2, machines are formalized by adopting an explicit representation of the states and then writing an interpreter for the machine language. Another way of putting it is this: to formalize a machine language, implement a simulator for it in functional Lisp. While this may seem to be a mere programming exercise, it is also a logic exercise if the simulator is written in an axiomatically described programming language like ACL2.

In our model of the JVM, a state consists of three components: the thread table, the heap, and the class table. We describe each in turn. When we use the word ``table'' here we generally mean a list of pairs in which ``keys'' (which might be thought of as constituting the left-hand column of the table) are paired with ``values'' (the right-hand column of the table). Such a table is a map from the keys to the corresponding values.

The thread table maps thread numbers to threads. Each thread consists of three components: a call stack, a flag indicating whether the thread is scheduled, and the heap address of an object of class Thread in the heap uniquely associated with this thread. We discuss the heap below.

The call stack is a list of frames treated as a stack (the first element of the list is the topmost frame). Each frame contains five components: a program counter and the bytecoded method body, a table associating variable names with values, a stack, and a synchronization flag indicating whether the method currently executing is synchronized. Unlike the JVM, the local variables of a method are referenced by symbolic names rather than positions.

The heap is a table associating heap addresses with instance objects. An instance object is a table. The keys of an instance object are the successive classes in the superclass chain of the object. The value of each such key is another table, mapping the immediate field names of the class to their values. The structure of heap addresses is unimportant but they can be distinguished from integers and other data types. In our model a heap address is a list of the form (REF $\mathit{i}$), where $\mathit{i}$ is a natural number. One point where our model differs from the JVM is that in our model the NEW instruction is completely responsible for the object's instantiation; all fields are initialized to 0. Classes in our model do not have separate constructors.

Finally, the class table is a table mapping class names to class descriptions. A class description contains a list of its superclass names, a list of its immediate fields, and a list of its methods. We do not model syntactic typing in our machine, though we could. Thus, our list of fields is just a simple list of field names (strings) rather than, say, a table mapping field names to signatures. A method is a list containing a method name, the names of the formal parameters of the method, a synchronization status flag, and a list of bytecoded instructions. Our model omits signatures and the access modes of methods.

Bytecoded instructions are represented abstractly as lists consisting of a symbolic opcode name followed by zero or more operands. For example, (LOAD X) is the instruction that pushes the value of local variable X onto the stack in the current frame. (ADD) pops two items off the stack in the current frame and pushes their sum. (IFEQ 12) pops an item off the stack and if it is 0, increments the program counter by 12; otherwise it increments it by 1. The similarity of these instructions to certain JVM instructions should be obvious, as should be the differences: we ignore the different types of LOAD (e.g., ILOAD, DLOAD, etc.) and ADDinstructions, we ignore the finite range of integer data, and we count program counter offsets in number of instructions rather than number of bytes. These and most of the other discrepancies between the current model and the JVM are matters of detail that would not change the basic structure of the model to fix and do not impact our ability to use the model to study proof techniques.

  

Table 1: execute-PUSH

(defun execute-PUSH (inst s th)
  (make-state
   (modify-tt th
              (push (make-frame (+ 1 (pc (top-frame s th)))
                                (locals (top-frame s th))
                                (push (arg1 inst)
                                      (stack (top-frame s th)))
                                (program (top-frame s th))
                                (sync-flg (top-frame s th)))
                    (pop (call-stack s th)))
              'SCHEDULED
              (thread-table s))
   (heap s)
   (class-table s)))

For those readers curious to see how we define the semantics of such operations in ACL2, see Table 1. It contains the definition of the function execute-PUSH which we use to give semantics to the PUSH instruction. The instruction (PUSH 3) is comparable to ICONST_3 or BIPUSH 3 on the JVM.

The function takes three arguments, named inst, s, and th. The first is the list expression denoting the instruction. The first element of inst will always be the symbol PUSH and the second is the constant that is to be pushed on the stack of the current frame. The second argument of execute-PUSH, s, is the JVM state, consisting of a thread table, a heap and a class table. The third argument, th, is the number of the thread that is to be ``stepped.'' Execute-PUSH returns the state obtained by executing the PUSH instruction in the given thread of s. It creates that state with the function make-state, which takes three arguments: the thread table, the heap and the class table of the state to be returned. The last two components of the new state above are the same as those in s. The thread table is modified by replacing the entry for th by another entry. That entry's call stack is obtained by replacing the topmost frame of the current call stack (notice we push a frame onto a stack obtained by popping one off). In the new frame, the program counter is advanced by 1, the locals remain unchanged, the constant (extracted from inst using the function arg1) is pushed on the stack, and the method program and synchronization flag are unchanged.

The most complicated instruction formalized in our model is INVOKEVIRTUAL. An example INVOKEVIRTUAL instruction on our machine is represented by the list structure (INVOKEVIRTUAL "ColoredPoint" "move" 2). Note that in place of the JVM's signature we provide only the number of parameters, since we consistently ignore type issues in this model. We paraphrase the definition of execute-INVOKEVIRTUAL by describing the state it creates from an instruction of the form below, a state $\mathit{s}$, and a thread number $\mathit{th}$.

(INVOKEVIRTUAL $\mathit{c}$ $\mathit{name}$ $\mathit{n}$): Let $\mathit{ref}$ be the item $\mathit{n}$ deep in the stack. This is expected to be a heap reference to an instance object, $\mathit{obj}$. Let $\mathit{class}$ be the class of this object (the first key in the table, i.e., the name of the most specific class in the object's class hierarchy). Use the function lookup-method to determine from the class-table of $\mathit{s}$ the closest method with name $\mathit{name}$ in $\mathit{class}$ or its superclass chain. Let $\mathit{formals}$ and $\mathit{body}$ be the formal parameters and bytecoded body of the closest method. Let $\mathit{formals'}$ be $\mathit{formals}$ with the new symbol THISadded to the front.

Create a new call stack, $\mathit{cs'}$, from the call stack of thread $\mathit{th}$ in $\mathit{s}$ by replacing the topmost frame by a new frame in which the program counter has been incremented by one and $\mathit{n}+1$ items have been popped off the stack. Create another call stack, $\mathit{cs''}$, by pushing a new frame onto $\mathit{cs'}$. This new frame should have a program counter of 0 and an empty stack. The locals of the new frame should bind $\mathit{formals'}$ to the topmost $\mathit{n}+1$ items removed from the stack in $\mathit{s}$ (above), the deepest of which is bound to THIS. The bytecoded body of the frame should be $\mathit{body}$. We will use $\mathit{cs'}$ and $\mathit{cs''}$ in various cases below and we will not be interested in $\mathit{cs''}$ unless the closest method is non-native. Consider the following cases.

• The closest method is native: We support only two native methods, "start" and "stop" from the "Object" class. We describe only the first here. In this case, $\mathit{obj}$ should include the class "Thread" in its superclass chain. The new state constructed by the "start" method has the same heap and class table as $\mathit{s}$. The thread table is changed in two ways. First, the call stack of $\mathit{th}$ is replaced by $\mathit{cs'}$ above (stepping over the INVOKEVIRTUAL). Second, the thread $\mathit{th'}$ uniquely associated with $\mathit{obj}$ is changed so that its scheduled flag is SCHEDULED.

• The closest method is a synchronized method: Fetch the contents of the "monitor" and "mcount" fields in the "Object" class of $\mathit{obj}$. If the mcount is 0 or the mcount is non-0 but the monitor is $\mathit{th}$, then we say $\mathit{obj}$ is ``available'' to $\mathit{th}$. If $\mathit{obj}$ is available to $\mathit{th}$, then the new state is obtained from $\mathit{s}$ by replacing the call stack with $\mathit{cs''}$ after setting the sync-flg component of the top frame to LOCKED, and by replacing the heap of $\mathit{s}$ with a heap in which the "mcount" field of the object at $\mathit{ref}$ has been incremented by one and the "monitor" field has been set to $\mathit{th}$. If, on the other hand, $\mathit{obj}$is unavailable, then the ``new'' state is $\mathit{s}$ itself. Thus, the thread hangs at the INVOKEVIRTUAL instruction until $\mathit{obj}$ becomes available. We do not specify the scheduler; instead, our model allows all possible interleavings of thread executions and some thread states (as the one just described) make no change if stepped before progress is possible.

• Otherwise, the new state is obtained from $\mathit{s}$ by replacing the call stack with $\mathit{cs''}$ after setting the sync-flg component of the top frame to UNLOCKED.

Given execute-PUSH, the reader can presumably imagine how this description is coded in ACL2.

We formalize a variety of instructions in this style, including POP, LOAD, STORE, ADD, MUL, GOTO, IFEQ, IFGT, RETURN, XRETURN, NEW, GETFIELD, PUTFIELD, MONITORENTER, and MONITOREXIT. For each such opcode $\mathit{op}$ we define an ACL2 function execute- $\mathit{op}$ that takes the instruction, current state, and thread number and returns the next state.

We then define step to be the function that takes a state and a thread number and executes the next instruction in the given thread, provided that thread exists and is SCHEDULED. Step is essentially a ``big switch'' on the opcode of the instruction indicated by the program counter and method body in the top frame of the call stack of the given thread.

Finally we define run to take a ``schedule'' and a state and return the result of stepping the state according to the given schedule. A schedule is just a list of numbers, indicating which thread is to be stepped next. That is, our model puts no constraints on the JVM thread scheduler; however stepping a non-existent, UNSCHEDULED, or otherwise blocked thread is a no-op. We find it convenient also to define (runn n schedule s) to run the first n steps of schedule starting in state s.

The complete ACL2 source text for our machine is available from https://www.cs.utexas.edu/users/moore/publications/m4/index.html.

Our model omits many features of the JVM. Among the more glaring omissions are accurate support for the JVM primitive data types like ints, doubles, arrays, etc., support for syntactic typing both in the naming convention in the instruction set (e.g., IADD versus DADD) and field and method signatures, class loading and initialization, INVOKESTATIC (with the concomitant requirement that classes have representative instance objects in the heap upon which synchronization can be arranged), exception handling, and errors. Experience with other commercial microprocessor models leads us to believe that these features could be added to our model without fundamentally changing its basic structure. There is no doubt that they greatly complicate the model and would complicate proofs about programs that use the features in question. That is one of the reasons we left them out. Our model is adequate however as a vehicle for studying basic mechanized proof techniques for dealing with Java programs, including multi-threaded applications.