---

LockStatus.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 LockStatus extends LockSet{
// ifdef RACE
  private static final int VIRGIN          = 0;
  private static final int EXCLUSIVE       = 1;
  private static final int SHARED          = 2;
  private static final int SHARED_MODIFIED = 3;
  private static final int FAILED          = 4;

  private int state = VIRGIN;
  private AccessList accesses = new AccessList();

  private ThreadInfo first_thread;

//#endif RACE
  public void checkRead(ThreadInfo thread,String className,String fieldName){
    if (!isSafe(thread,false)){
      Runner.race_conditions++;
      printExplanation(className,fieldName);    
      RaceWindow.addRace(this);
    }
  }  
  public void checkReadArray(ThreadInfo thread,int index){
    if (!isSafe(thread,false)){
      Runner.race_conditions++;
      printArrayExplanation(index);    
      RaceWindow.addRace(this);
    }
  }  
  public void checkWrite(ThreadInfo thread,String className,String fieldName){
    if (!isSafe(thread,true)){
      Runner.race_conditions++;
      printExplanation(className,fieldName);
      RaceWindow.addRace(this);
    }
  }  
  public void checkWriteArray(ThreadInfo thread,int index){
    if (!isSafe(thread,true)){
      Runner.race_conditions++;
      printArrayExplanation(index);
      RaceWindow.addRace(this);
    }
  }  
  public AccessList getAccessList(){
    return accesses;
  }  
  private boolean isSafe(ThreadInfo thread,boolean isWrite){
    switch (state){
      case VIRGIN : 
        accesses.addInit(thread);
        first_thread = thread;
        state = EXCLUSIVE;
        return true;
      case EXCLUSIVE :
        if (thread == first_thread)
          return true;
    else{
          if (isWrite){
            accesses.addWrite(thread);
            refineFirst(thread);
            if (isEmpty()){
              state = FAILED;
              return false;
        }
            else{
              state = SHARED_MODIFIED;
              return true;
            }
      }
          else{ 
            accesses.addRead(thread);
            refineFirst(thread);
            state = SHARED;
            return true;
      }
    }
      case SHARED :  
        if (isWrite){
          accesses.addWrite(thread);
          refine(thread);
          if (isEmpty()){
            state = FAILED;
            return false;
          }
          else{
            state = SHARED_MODIFIED;
            return true;
          }
        } 
        else{
          if (refine(thread))
            accesses.addRead(thread);
          return true;
        };
      case SHARED_MODIFIED :
        if (refine(thread)){
          if (isWrite)
            accesses.addWrite(thread);
          else
            accesses.addRead(thread);
        };
        if (isEmpty()){
          state = FAILED;
          return false;
        }
        else{
          return true;
        }
      case FAILED :
        return true;
      default :
        Debug.println(Debug.ERROR, "*** LockStatus state undefined : " + state);
        System.exit(0);
        return false; // Java compiler requires this statement
    };
  }  
  public void print(){
    Analyze.print("Variable state = ");
    switch(state){
      case VIRGIN          : Analyze.println("VIRGIN");break;
      case EXCLUSIVE       : Analyze.println("EXCLUSIVE");break;
      case SHARED          : Analyze.println("SHARED");break;
      case SHARED_MODIFIED : Analyze.println("SHARED_MODIFIED");break;
      case FAILED          : Analyze.println("FAILED");break;
    };
    Analyze.print("Lock set = ");
    printSet();
  }  
  private void printArrayExplanation(int index){
    String descr = "Array (in index " + index + ")";
    printExplanationPlus(descr);
  }  
  private void printExplanation(String className, String fieldName){
    String descr = "Variable " + fieldName + " in class " + className;
    printExplanationPlus(descr);
  }  
  private void printExplanationPlus(String descr){
    Analyze.println("\n\n");
    Analyze.println("******************************");
    Analyze.println("Race condition!");
    Analyze.println("------------------------------");
    Analyze.println(descr);
    Analyze.println("is accessed unprotected.");
    Analyze.println("******************************");
    Analyze.println("");
    Analyze.println("=============================");
    Analyze.println(" *** Access description: *** ");
    Analyze.println("=============================");
    accesses.print();
    Analyze.println("=============================");
  }  
  private boolean refine(ThreadInfo thread){
    int cardinality_before = cardinality();
    intersect(thread.getLockSet());
    return (cardinality() < cardinality_before);
  }  
  private void refineFirst(ThreadInfo thread){
    union(thread.getLockSet());
  }  
}

---