Because our model, run, is an ACL2 program, it can be executed on
concrete data to produce concrete results. To run our bytecode we create a
state, say
,
containing the thread table, heap, and class table we have
in mind. An expression constructing such a state is shown in Table 2.
The class Alphacontains a single instance method factwhich is just a recursive factorial program written in our bytecode.1
The bytecode is similar to that produced by compiling
public int fact(int n) {
if (n<=0) return 1;
else return n*fact(n-1);
}
except our arithmetic is not bounded. We show the JVM bytecode
for this fact in Table 2, in line-by-line correspondence with ours.
The main program of the only thread in the thread table of
creates a new
instance object of class Alpha and invokes its fact method after
pushing 5. That is, it calls fact on 5.
(make-state
(make-tt ; Thread table
(push ; call stack of thread 0
(make-frame 0 ; frame: pc
nil ; locals
nil ; stack
'((NEW "Alpha") ; method body
(STORE OBJ)
(LOAD OBJ)
(PUSH 5)
(INVOKEVIRTUAL "Alpha" "fact" 1)
(HALT))
'UNLOCKED) sync status
nil))
nil ; Heap
(make-class-def ; Class Table
(list
(make-class-decl
"Alpha" ; class name
'("Object") ; superclasses
NIL ; fields
'(("fact" (N) NIL ; Method int fact(int)
(LOAD N) ; 0 iload\_1
(IFGT 3) ; 1 ifgt 6
(PUSH 1) ; 4 iconst\_1
(XRETURN) ; 5 ireturn
(LOAD N) ; 6 iload\_1
(LOAD THIS) ; 7 aload\_0
(LOAD N) ; 8 iload\_1
(PUSH 1) ; 9 iconst\_1
(SUB) ; 10 isub
(INVOKEVIRTUAL "Alpha" "fact" 1) ; 11 invokevirtual \#8
|
Call the state in Table 2
.
To run
we must provide a schedule. Since the main program is in thread 0(the only thread) and creates no other threads, a suitable schedule is
just a list of 0's.
The list constant shown in Table 3 is the state
created by evaluating (run (repeat 58 0)
). Call that state
.
Thus,
is the result of stepping thread 0 fifty-eight times
starting with
.
The code elided away is just the definition of our
fact method. Inspection of thread 0 reveals that the program counter of the
top frame is pointing to the last instruction, the (XRETURN), and that
120 is on the top of the stack. Stepping once would pop the top frame
and push the 120 onto the empty stack of the frame below. The new top
frame is poised to execute the (HALT) instruction. So stepping
sixty times halts the machine with 120 on top of the stack in the main
frame. Since 120 is 5!, the fact method seems to have worked.
(((0 ; Thread 0
((11 ; call stack, top frame: pc
((THIS . (REF 0)) (N . 5)) ; locals
(120) ; stack (120 on top)
((LOAD N) ; method body
(IFGT 3)
(PUSH 1)
(XRETURN)
(LOAD N)
(LOAD THIS)
(LOAD N)
(PUSH 1)
(SUB)
(INVOKEVIRTUAL "Alpha" "fact" 1)
(MUL)
(XRETURN)) ; (pc points here)
UNLOCKED) ; sync status
(5 ; next frame: pc
((OBJ . (REF 0))) ; locals
() ; stack (empty)
((NEW "Alpha") ; method body
(STORE OBJ)
(LOAD OBJ)
(PUSH 5)
(INVOKEVIRTUAL "Alpha" "fact" 1)
(HALT)) ; (pc points here)
UNLOCKED)) ; sync status
SCHEDULED NIL))
((0 ; Heap address 0:
("Alpha") ; Alpha fields: none
("Object" ; Object fields:
("monitor" . 0)
("mcount" . 0)
("wait-set" . 0))))
; Class table
(("Object" ; Object class
() ; superclasses
("monitor" ; fields
"mcount"
"wait-set")
(("start" () NIL NIL) ; methods
("stop" () NIL NIL)))
("Thread" ; Thread class
("Object") ; superclasses
() ; fields (none)
(("run" () NIL (RETURN)))) ; methods
("Alpha" ; Alpha class
("Object") ; superclasses
() ; fields (none)
(("fact" (N) NIL (LOAD N) ... (XRETURN)))))) ; methods
|
Also evident in Table 3 is the representation of the instance object at heap address 0, an object of class Alpha(which has no fields) with superclass "Object" (which has fields "monitor", "mcount" and "wait-set"). Note also the class table, which, in addition to our Alpha class, contains two built in classes, Object and Thread. In our model, the Object class has only the three fields listed, and the Thread class has only two (native) methods, "start" and "stop" whose semantics are built into INVOKEVIRTUAL.
There are of course many schedules that run thread 0 in
for sixty
instructions. Any schedule containing sixty 0's would work, no matter
how many other thread numbers are interspersed between them.
Because our model is expressed in a formal mathematical logic, it is possible
to reason about it formally, using the ACL2 mechanical theorem prover.
Rather than just test that the fact method works for 5 and a few
other numbers, we can prove a theorem stating that the fact method
computes the factorial of its argument.
Theorem. fact is correct.
(implies (and (poised-to-invoke-fact s th n)
(natp n))
(equal (top
(stack
(top-frame
(run (fact-sched n th) s)
th)))
(factorial n)))
The hypotheses of the theorem assume that s is a state poised (in
thread th) to invoke our fact method on the natural number
n. Because fact is an instance method, this requires inspecting
the top two objects on the stack to make sure that the topmost is a natural
number and that the resolution of the name "fact" in the class of the
next item is our fact method. The conclusion is an equality stating
that a certain expression is equal to (factorial n). Here,
factorial is the mathematical function of that name, defined in ACL2.
The expression in question describes the top item on the stack in the top
frame of thread th in the state obtained by executing state s a
certain number of steps, as given by (fact-sched n th). Thus, this
theorem establishes that by running thread th a certain number of
steps, it computes the factorial function.2
The proof of the factorial theorem can be constructed interactively with the ACL2 theorem prover and the theorem prover is entirely responsible for the correctness of the proof. In this case, the user provides an inductive argument and the machine carries out that argument, expanding definitions, applying axioms and basic theorems about the machine. For a discussion of such theorems see [15]. The proof that fact computes factorial takes about 30 seconds (on a 700 MHz machine).
class Container {
public int counter;
}
class Job extends Thread {
Container objref;
Object x;
public Job incr () {
synchronized(objref) {
objref.counter = objref.counter + 1;
}
return this;
}
public void setref(Container o) {
objref = o;
}
public void run() {
for (;;) {
incr();
}
}
}
class Apprentice {
public static void main(String[] args){
Container container = new Container();
for (;;) {
Job job = new Job();
job.setref(container);
job.start();
}
}
}
|
In Table 5 we show a more interesting state, modeled after the Java Apprentice code shown in Table 4. In this state the main program creates an object of class Container and then loops forever creating and starting Thread objects of class Job. Each Job is in an infinite loop using the method incr to read, increment, and write into the counter field of the Containerobject. The critical section of the incr method is protected by MONITORENTER and MONITOREXIT.3
(make-state
(make-tt ; Thread Table
(push (make-frame 0 ; call stack, top frame: pc
'((CONTAINER . NIL) (JOB . NIL)) ; locals (uninitialized)
() ; stack (empty)
'((NEW "Container") ; main method
(STORE CONTAINER)
(NEW "Job")
(STORE JOB)
(LOAD JOB)
(LOAD CONTAINER)
(INVOKEVIRTUAL "Job" "setref" 1)
(LOAD JOB)
(INVOKEVIRTUAL "Job" "start" 0)
(GOTO -7))
'UNLOCKED)
nil))
nil ; Heap
(make-class-def ; Class Table
(list (make-class-decl "Container" ; Container class
'("Object") ; superclasses
'("counter") ; fields
'()) ; methods (none)
(make-class-decl "Job" ; Job class
'("Thread" "Object"); superclasses
'("x" "objref") ; fields
'(("incr" () nil ; methods
(LOAD THIS)
(GETFIELD "Job" "objref")
(STORE TEMP)
(LOAD TEMP)
(MONITORENTER)
(LOAD THIS)
(GETFIELD "Job" "objref")
(LOAD THIS)
(GETFIELD "Job" "objref")
(GETFIELD "Container" "counter")
(PUSH 1)
(ADD)
(PUTFIELD "Container" "counter")
(LOAD TEMP)
(MONITOREXIT)
(LOAD THIS)
(XRETURN))
("run" (N) nil
(LOAD THIS)
(INVOKEVIRTUAL "Job" "incr" 0)
(GOTO -1))
("setref" (R) nil
(LOAD THIS)
(LOAD R)
(PUTFIELD "Job" "objref")
(RETURN))
)))))
|
If we remove the MONITORENTER and MONITOREXIT (and the corresponding LOAD) instructions from the bytecode (i.e., remove the synchronization from the Java method) we can exhibit a schedule that makes the counter decrease: run the main thread until it has started two jobs, then run the first thread until it pushes the value of the counter (which at this point will be 0) onto its local stack, then run the other thread many cycles to increment the counter several times, and finally run the first job again so that it increments its 0 and writes a 1 into the counter field.
The ability to deal with schedules and states abstractly makes it easier to explore such issues. This illustrates the value of an executable abstract model.
However, there is no schedule that makes the state in Table 5 decrease the counter. This cannot be demonstrated by testing. It can, however, be proved by analyzing our model. Here is a theorem proved with the ACL2 theorem prover about the state shown in Table 5, here called *a0*.
Theorem. Apprentice Monotonicity
(implies (and (natp n)
(natp m)
(<= n m))
(<= (counter
(runn n any-schedule *a0*))
(counter
(runn m any-schedule *a0*))))
The theorem compares the values of the counter in two states, one obtained by
running *a0* n steps and the other obtained by running msteps, both according to the same completely unconstrained schedule. If
n 
m, the counter in the former state is less than or equal
to that in the latter state. This theorem is a statement about an unbounded
number of parallel threads using the JVM synchronization primitives. The
proof requires careful (and rather global) analysis of what is happening in
the heap. (For example, all threads writing to the Containerrespect the monitor and no thread changes the objref field of
a running thread.)
See, for example, Praxis 56 in [10], where Haggar writes
``Do not reassign the object reference of a locked object.'' For details of
our proof see [16].