Check out the new USENIX Web site. next up previous
Next: Conclusion Up: An Executable Formal Java Previous: Specification of the JVM

Some Examples of Execution

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 $\mathit{s}_0$, 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 $\mathit{s}_0$ creates a new instance object of class Alpha and invokes its fact method after pushing 5. That is, it calls fact on 5.


  
Table 2: A State for Computing Factorial

(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 
       (MUL)                            ;  14 imul
       (XRETURN)))))))                  ;  15 ireturn

Call the state in Table 2 $\mathit{s}_0$. To run $\mathit{s}_0$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) $\mathit{s}_0$). Call that state $\mathit{s}_{58}$. Thus, $\mathit{s}_{58}$ is the result of stepping thread 0 fifty-eight times starting with $\mathit{s}_0$. 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 $\mathit{s}_0$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.


  
Table 3: The Result of Stepping the Factorial State 58 Times
(((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 $\mathit{s}_0$ 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).


  
Table 4: The Apprentice Class: Unbounded Parallelism
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


  
Table 5: Apprentice in Our Model
(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 $\leq$ 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].


next up previous
Next: Conclusion Up: An Executable Formal Java Previous: Specification of the JVM
J Strother Moore and George M. Porter
2001-02-20