---

Monitor.java

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

import gov.nasa.arc.ase.util.Debug;
import gov.nasa.arc.ase.util.HashData;
import gov.nasa.arc.ase.jpf.InternalErrorException;
import java.io.*;
//#ifdef JDK11


//#else JDK11
import java.util.*;
//#endif JDK11
//#ifdef RACE

//#endif RACE

/**
 * Represents the monitor associate with classes and objects.
 */
public class Monitor { 
  /**
   * The identifier of the thread locking an object.
   */
  private int lockingThread;

  /**
   * The number of nested locks acquired.
   */
  private int lockCount;

  /**
   * The list of threads waiting to be notified.
   */
  private int[] waitingThreads;

  /**
   * Creates a new empty monitor.
   */
  public Monitor() {
    lockingThread = -1;
    lockCount = 0;
    waitingThreads = new int[0];
  }  
  /**
   * Returns true if it is possible to lock the monitor.
   */
  public boolean canLock(ThreadInfo th) {
    if (lockingThread == -1) return true;

    return (lockingThread == th.index);
  }  
  /**
   * Creates a clone of the monitor.
   */
  public Object clone() {
    Monitor m = new Monitor();

    m.lockingThread = lockingThread;
    m.lockCount = lockCount;
    m.waitingThreads = new int[waitingThreads.length];
    System.arraycopy(waitingThreads, 0, m.waitingThreads, 0, waitingThreads.length);

    return m; 
  }  
  /**
   * Compares to another object.
   */
  public boolean equals(Object o) {
    if(o == null) return false;
    if(!(o instanceof Monitor)) return false;

    Monitor m    = (Monitor)o;

    if (lockingThread != m.getLockingThread()) return false;
    if (lockCount != m.getLockCount()) return false;

    int[] w = m.waitingThreads;

    if (waitingThreads.length != w.length) return false;

    for(int i = 0; i < waitingThreads.length; i++)
      if(waitingThreads[i] != w[i]) return false;

    return true;
  }  
  /**
   * Returns the number of nested locks acquired.
   */
  public int getLockCount() {
    return lockCount;
  }  
  /**
   * Returns the identifier of the thread holding the lock.
   */
  public int getLockingThread() {
    return lockingThread;
  }  
  /**
   * Returns the list of waiting threads.
   */
  public int[] getWaitingThreads() {
    return waitingThreads;
  }  
  public void hash(HashData hd) {
    hd.add(lockingThread);
    hd.add(lockCount);

    for(int i = 0, l = waitingThreads.length; i < l; i++)
      hd.add(waitingThreads[i]);
  }  
  public int hashCode() {
    HashData hd = new HashData();

    hash(hd);

    return hd.getValue();
  }  
  /**
   * Interrupts one of the threads holding the lock.
   */
  public void interrupt(ThreadInfo th) {
    remove(th.index);
    th.setStatus(ThreadInfo.INTERRUPTED);
  }  
  /**
   * Acquires the lock for a given object or class.
   */
  public void lock(ThreadInfo th, Ref ref) {
    if(lockingThread == -1) {
      lockingThread = th.index;

//#ifdef RACE || LOCK_ORDER

//#endif LOCK_ORDER
    } else
      if(lockingThread != th.index)
    throw new InternalErrorException("lock operation failed");
    lockCount++;  
  }  
  /**
   * Tries to require the lock after being notified.
   */
  public void lockNotified(ThreadInfo th, Ref ref) {
    if (lockingThread != -1)
      throw new InternalErrorException("lock operation failed");

    lockingThread = th.index;
    lockCount = th.getLockCount();
    
    //** warning: should have been done when interrupted was set.   **//
    for(int i = 0; i < waitingThreads.length; i++)
      if(waitingThreads[i] == th.index) {
    remove(i);
    break;
      }

    th.setStatus(ThreadInfo.RUNNING);
    th.setLockCount(0);
  }  
  public void log() {
    Debug.println(Debug.MESSAGE, "    $lockingThread$: " + lockingThread);
    Debug.println(Debug.MESSAGE, "    $lockCount$: " + lockCount);
    Debug.print(Debug.MESSAGE, "    $waitingThreads$: { ");
    for(int i = 0, l = waitingThreads.length; i < l; i++) {
      if(i != 0) Debug.print(Debug.MESSAGE, ", ");
      Debug.print(Debug.MESSAGE, Integer.toString(waitingThreads[i]));
    }
    Debug.println(Debug.MESSAGE, " }");
  }  
  /**
   * Notifies one of the threads. The thread is chosen non deterministically.
   */
  public void notify(SystemState ss) {
    int length = waitingThreads.length;

    if(length == 0) return;

    int random = ss.random(length);

    ss.ks.tl.get(remove(random)).setStatus(ThreadInfo.NOTIFIED);
  }  
  /**
   * Notifies all waiting threads.
   */
  public void notifyAll(SystemState ss) {
    for(int i = 0, l = waitingThreads.length; i < l; i++) {
      ThreadInfo th = ss.ks.tl.get(waitingThreads[i]);
      th.setStatus(ThreadInfo.NOTIFIED);
    }

    waitingThreads = new int[0];
  }  
  private int remove(int index) {
    int r = waitingThreads[index];
    int length = waitingThreads.length;

    int[] n = new int[length - 1];
    System.arraycopy(waitingThreads, 0, n, 0, index);
    System.arraycopy(waitingThreads, index+1, n, index, length - index - 1);
    waitingThreads = n;

    return r;
  }  
  public String toString() {
    StringBuffer sb = new StringBuffer();

    sb.append("Monitor(");
    sb.append("lockingThread=");
    sb.append(lockingThread);
    sb.append(',');
    sb.append("lockCount=");
    sb.append(lockCount);
    sb.append(',');
    sb.append("waitingThreads=");
    sb.append('[');
    for(int i = 0; i < waitingThreads.length; i++) {
      if(i != 0)
    sb.append(',');
      sb.append(waitingThreads[i]);
    }
    sb.append(']');
    sb.append(')');

    return sb.toString();
  }  
  /**
   * Releases the lock. The lock can be still held by the thread
   * if it had been locked more than once.
   */
  public void unlock(ThreadInfo th, Ref ref) {
    lockCount--;

    if(lockCount < 0)
      throw new InternalErrorException("lock counter can't be negative");

    if (lockCount == 0) {
      lockingThread = -1;
//#ifdef RACE || LOCK_ORDER

//#endif RACE || LOCK_ORDER
    }
  }  
  /**
   * Waits to be notified. Releases the lock and waits.
   */
  public void wait(ThreadInfo th, Ref ref) {
    if(lockingThread != th.index)
      throw new InternalErrorException("wait on an unlocked monitor");

    th.setStatus(ThreadInfo.WAITING);
    th.setLockCount(lockCount);

    int length = waitingThreads.length;
    int[] n = new int[length + 1];
    System.arraycopy(waitingThreads, 0, n, 0, length);
    waitingThreads = n;
    waitingThreads[length] = th.index;

    lockingThread = -1;
    lockCount = 0;

//#ifdef RACE || LOCK_ORDER

//#endif RACE || LOCK_ORDER
  }  
}

---