---

Monitor.java

package gov.nasa.arc.ase.jpf.jvm;

import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.HashData;
import java.io.*;
import java.util.*;
// ifdef RACE
import gov.nasa.arc.ase.jpf.jvm.runtime.*;
//#endif RACE

public class Monitor implements Cloneable { 
  int   locking_thread  = -1;
  int   lock_count  = 0;
  List  waiting_threads = new ArrayList();

  public Monitor() {
  }  
  public Monitor(int lt, int lc, List wt) {
    locking_thread = lt;
    lock_count = lc;
    waiting_threads = wt;
  }  
// ifdef RACE
  private void ANALYZE_lock(ThreadInfo th, Ref ref) {
    if (Analyze.on()) {
      th.getLockSet().addLock(ref);
      if (Analyze.debug_on()) {
    Analyze.println("--- LOCK ------------");
    Analyze.println("Thread " + th.getThreadReference() 
        + " locks object [" + ref + "]");      
    th.getLockSet().print();
      }
    }
  }  
  private void ANALYZE_unlock(ThreadInfo th, Ref ref) {
    if (Analyze.on()) {
      th.getLockSet().deleteLock(ref);      
      if (Analyze.debug_on()) {
    Analyze.println("--- UNLOCK ----------");
    Analyze.println("Thread " + th.getThreadReference() 
        + " releases object [" + ref + "]"); 
    th.getLockSet().print();
      }
    }    
  }  
  private void ANALYZE_wait(ThreadInfo th, Ref ref) {
    if (Analyze.on()) {
      th.getLockSet().deleteLock(ref);
      if (Analyze.debug_on()) {
    Analyze.println("--- WAIT ------------");
    Analyze.println("Thread " + th.getThreadReference() 
        + " waits on object [" + ref + "]");
    th.getLockSet().print();
      }    
    }
  }  
  public boolean checkLock(ThreadInfo th) {
    if (locking_thread == -1) 
      return true;
    return (locking_thread == th.getThreadReference());
  }  
  public boolean checkLockAfterNotified(ThreadInfo th) {
    return checkLock(th);
  }  
//#endif RACE

  public Object clone() {
    try {
      Monitor m = (Monitor)super.clone();
      m.locking_thread = locking_thread;
      m.lock_count = lock_count;
      m.waiting_threads = new ArrayList();
      for(int i = 0; i < waiting_threads.size(); i++)
    m.waiting_threads.add(waiting_threads.get(i));
      return m; 
    } catch(CloneNotSupportedException e) {
      throw new InternalError(e.toString());
    }  
  }  
  public boolean equals(Object obj) {
    Monitor m    = (Monitor)obj;

    if (locking_thread != m.getLockingThread()) return false;
    if (lock_count != m.getLockCount()) return false;

    List waiting = m.waiting_threads;

    if (waiting_threads.size() != waiting.size()) return false;

    for(int i = 0; i < waiting_threads.size(); i++)
      if (((Integer)waiting_threads.get(i)).compareTo(waiting.get(i)) != 0) return false;

    return true;
  }  
  public int getLockCount() {
    return lock_count;
  }  
  public int getLockingThread() {
    return locking_thread;
  }  
  public List getWaitingThreads() {
    return waiting_threads;
  }  
  public void hash(HashData hd) {
    hd.add(lock_count);

    for(int i = 0, l = waiting_threads.size(); i < l; i++)
      hd.add(((Integer)waiting_threads.get(i)).intValue());
  }  
  public int hashCode() {
    HashData hd = new HashData();

    hd.add(lock_count);

    for(int i = 0, l = waiting_threads.size(); i < l; i++)
      hd.add(((Integer)waiting_threads.get(i)).intValue());

    return hd.getValue();
  }  
  public boolean lock(ThreadInfo th, Ref ref) {
    if (locking_thread == -1) { 
      locking_thread = th.getThreadReference();
// ifdef RACE
      ANALYZE_lock(th,ref);
      LOCKORDER_lock(th,ref);
//#endif RACE
    }
    if (locking_thread == th.getThreadReference()) {
      lock_count++;  
// ifdef DEBUG

//#endif DEBUG
      return true;
    } else {
// ifdef DEBUG


//#endif DEBUG
      return false;
    }
  }  
  public boolean lockAfterNotified(ThreadInfo th, Ref ref) {
    if (lock(th,ref)) {
      th.setStatus(STATUS.RUNNING);
      lock_count = th.getLockCount();
      return true;
    }
    else
      return false;
  }  
  private void LOCKORDER_lock(ThreadInfo th, Ref ref) {
    if (LockOrder.on()) {
      VirtualMachine vm = (VirtualMachine)Engine.vm;
      KernelState ks = (KernelState)vm.getKernelState();
      String className;
      if(ref.isClass)
    className = ks.static_area.getClass(ref.reference).getClassName();
      else
    className = ks.dynamic_area.getClass(ref.reference).getClassName();
      th.getLockTree().lock(LockPool.get(new Lock(ref,className)));
    }
  }  
  private void LOCKORDER_unlock(ThreadInfo th) {
    if (LockOrder.on()) {
      th.getLockTree().unlock();
    }
  }  
  private void LOCKORDER_wait(ThreadInfo th) {
    if (LockOrder.on()) {
      th.getLockTree().unlock();
    }
  }  
  public void notify(KernelState ks, Scheduler sch) {
    int notify_index = sch.getCurrentNotify();

    if (notify_index < waiting_threads.size()) {
      if ((notify_index + 1) < waiting_threads.size()) {
// ifdef DEBUG


//#endif DEBUG
    TransitionResult.setNotified();
      }
      else {
// ifdef DEBUG

//#endif DEBUG
    TransitionResult.clearNotified();
      }
      int thread_index = 
    ((Integer)waiting_threads.remove(notify_index)).intValue();
      ThreadInfo th = (ThreadInfo)ks.getThreadInfo(thread_index);
      th.setStatus(STATUS.NOTIFIED);
    }
  }  
  public void notifyAll(KernelState ks) {
    while (!waiting_threads.isEmpty()) {
      int thread_index = ((Integer)waiting_threads.remove(0)).intValue();
      ThreadInfo th = (ThreadInfo)ks.getThreadInfo(thread_index);
      th.setStatus(STATUS.NOTIFIED);
    }
  }  
  public void unlock(ThreadInfo th, Ref ref) {
// ifdef DEBUG

//#endif DEBUG
    lock_count--;
    if (lock_count < 0) {
      Debug.println(Debug.WARNING,"Illegal Monitor Operation");
    }
    if (lock_count == 0) {
      locking_thread = -1;
// ifdef RACE
      ANALYZE_unlock(th,ref);
      LOCKORDER_unlock(th);
//#endif RACE
    }
  }  
  public void wait(ThreadInfo th, Ref ref) {
    th.setStatus(STATUS.WAITING);
    th.setLockCount(lock_count); // be aware: perhaps lock_count - 1.
    waiting_threads.add(new Integer(th.getThreadReference()));
    locking_thread = -1;
    lock_count = 0;
// ifdef RACE
    ANALYZE_wait(th,ref);
    LOCKORDER_wait(th);
//#endif RACE
  }  
}

---