---

Depend.java

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

import gov.nasa.arc.ase.jpf.*;
import gov.nasa.arc.ase.jpf.jvm.*;
import java.util.*;
import gov.nasa.arc.ase.util.Debug;

public class Depend {
// ifdef RACE
  private static HashMap map = new HashMap(); // map ThreadUnit to DependInfo

//#endif RACE
  public static void addFork(ThreadInfo father,ThreadInfo son) {
    Unit fatherUnit = mkThreadUnit(father);
    Unit sonUnit = mkThreadUnit(son);
    DependInfo info = new DependInfo(fatherUnit);
    map.put(sonUnit,info);
  }  
  public static void addMain(ThreadInfo th) {
    Unit threadUnit = mkThreadUnit(th);
    map.put(threadUnit,new DependInfo());
  }  
  public static void addRead(ThreadInfo th,Ref ref) {
    Unit threadUnit = mkThreadUnit(th);
    Unit objectUnit = mkObjectUnit(ref);
    getInfo(threadUnit).addRead(objectUnit);
  }  
  public static void addWrite(ThreadInfo th,Ref ref) {
    Unit threadUnit = mkThreadUnit(th);
    Unit objectUnit = mkObjectUnit(ref);    
    getInfo(threadUnit).addWrite(objectUnit);
  }  
  public static eHashSet/*String*/ createWindow(eHashSet/*ThreadInfo*/ threads) {
    eHashSet/*String*/ threadNames = new eHashSet();
    if (on()) {
      eHashSet/*Unit*/ window = new eHashSet();
      Iterator threads_it = threads.iterator();
      ThreadInfo thread;
      while(threads_it.hasNext()) {
        thread = (ThreadInfo)threads_it.next();
        window.add(mkThreadUnit(thread));
      };
      eHashSet eWindow = extendWindow(window);
      Iterator eWindow_it = eWindow.iterator();
      Unit threadUnit;
      while(eWindow_it.hasNext()) {
        threadUnit = (Unit)eWindow_it.next();
        threadNames.add(threadUnit.getClassName());
      };
    }
    else {
      Iterator threads_it = threads.iterator();
      ThreadInfo thread;
      while(threads_it.hasNext()) {
        thread = (ThreadInfo)threads_it.next();
        threadNames.add(thread.getClassInfo().getClassName());
      };
    };
    return threadNames;
  }  
  public static boolean debug_on() {
    return Debug.getDebugLevel(Debug.DEPEND) > 0;
  }  
  private static eHashSet/*Unit*/ extendWindow(eHashSet/*Unit*/ window) {
    eHashSet/*Unit*/ passedThreads = new eHashSet();
    eHashSet/*Unit*/ waitingThreads = (eHashSet)window.clone();
    Unit thread;
    DependInfo info;
    Unit ancestor;
    while(!waitingThreads.isEmpty()) {
      thread = (Unit)waitingThreads.choose();
      if (!passedThreads.contains(thread)) {
        passedThreads.add(thread);
        info = getInfo(thread);
        ancestor = info.getThread();
        if (ancestor != null) waitingThreads.add(ancestor);
        waitingThreads.union(writingThreads(info.getReads()));
      };
    };
    return passedThreads;
  }  
  public static DependInfo getInfo(Unit thread) {
    return (DependInfo)map.get(thread);
  }  
  private static Unit mkObjectUnit(Ref ref) {
    VirtualMachine vm = (VirtualMachine)Engine.vm;
    KernelState    ks = (KernelState)vm.getKernelState();
    String className;

    if(ref.isClass()) {
      StaticArea sa = ks.static_area;
      className = sa.getClass(ref.getReference()).getClassName();
    } else {
      DynamicArea da = ks.dynamic_area;
      className = da.getClass(ref.getReference()).getClassName();
    }

    return UnitPool.get(new Unit(ref,className));
  }  
  private static Unit mkThreadUnit(ThreadInfo th) {
    Ref ref = th.getReference();
    String className = th.getClassInfo().getClassName();
    return UnitPool.get(new Unit(ref, className));
  }  
  public static boolean on() {  
    return VirtualMachine.options.depend;
  }  
  public static void print() {
    Unit thread;
    DependInfo info;
    Set keys = map.keySet();
    Iterator keys_it = keys.iterator();
    Debug.println(Debug.ERROR, "");
    Debug.println(Debug.ERROR, "#################");
    Debug.println(Debug.ERROR, "# Dependencies: #");
    Debug.println(Debug.ERROR, "#################");
    while (keys_it.hasNext()) {
      thread = (Unit)keys_it.next();
      info = getInfo(thread);
      Debug.println(Debug.ERROR, "");
      Debug.println(Debug.ERROR, "================");
      thread.print();
      Debug.println(Debug.ERROR, ":");
      Debug.println(Debug.ERROR, "================");
      info.print();
    }
  }  
  private static eHashSet writingThreads(eHashSet/*Unit*/ objs) {
    Iterator keys_it = map.keySet().iterator();
    eHashSet/*Unit*/ writing = new eHashSet();
    Unit thread;
    while (keys_it.hasNext()) {
      thread = (Unit)keys_it.next();
      if (objs.overlaps(getInfo(thread).getWrites()))
        writing.add(thread);
    };
    return writing;
  }  
}

---