[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools RaceDetector.java,NONE,1.1

[pcm <pcm...@us...>]

Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv2066/src/gov/nasa/jpf/tools

Added Files:
	RaceDetector.java 
Log Message:
simple lockset based race detector listener. We don't check for cycles yet (i.e. if the potentially conflicting operations really could occur in reverse order), but that should be easy to add 

--- NEW FILE: RaceDetector.java ---
//
// Copyright (C) 2005 United States Government as represented by the
// Administrator of the National Aeronautics and Space Administration
// (NASA).  All Rights Reserved.
// 
// This software is distributed under the NASA Open Source Agreement
// (NOSA), version 1.3.  The NOSA has been approved by the Open Source
// Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
// directory tree for the complete NOSA document.
// 
// THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
// KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
// LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
// SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
// A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
// THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
// DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
//

package gov.nasa.jpf.tools;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.Iterator;
import java.util.Stack;

import gov.nasa.jpf.PropertyListenerAdapter;
import gov.nasa.jpf.Search;
import gov.nasa.jpf.VM;
import gov.nasa.jpf.Config;
import gov.nasa.jpf.jvm.ElementInfo;
import gov.nasa.jpf.jvm.JVM;
import gov.nasa.jpf.jvm.ThreadInfo;
import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
import gov.nasa.jpf.jvm.bytecode.InstanceFieldInstruction;
import gov.nasa.jpf.jvm.bytecode.Instruction;
import gov.nasa.jpf.jvm.bytecode.PUTFIELD;
import gov.nasa.jpf.jvm.bytecode.PUTSTATIC;
import gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction;

/**
 * Simple field access race detector example
 * 
 * This implemenation so far doesn't deal with synchronization via signals, it
 * only checks if the lockset intersections of reads and writes from different
 * threads get empty. A more sophisticated version would check if the two
 * suspicious access operations (one read, one write) will also happen in reverse
 * order (that's the beauty of using this inside a model checker)
 */
public class RaceDetector extends PropertyListenerAdapter {
  
  /*** helper classes ***************************************************************/
  static class FieldAccess {
    ThreadInfo ti;
    Object[] locksHeld;          // the ones we have during this operation (not really required)
    Object[] lockCandidates;     // the intersection for all prev operations
    FieldInstruction finsn;
    
    FieldAccess prev;
    
    FieldAccess (ThreadInfo ti, FieldInstruction finsn) {
      this.ti = ti;
      this.finsn = finsn;
      this.locksHeld = ti.getLockedObjects().toArray();
    }
  
    Object[] intersect (Object[] a, Object[] b) {
      ArrayList list = new ArrayList(a.length);
      for (int i=0; i<a.length; i++) {
        for (int j=0; j<b.length; j++) {
          if (a[i].equals(b[j])) {
            list.add(a[i]);
            break;
          }
        }
      }
      return (list.size() == a.length) ? a : list.toArray();
    }
    
    void updateLockCandidates () {
      if (prev == null) {
        lockCandidates = locksHeld;
      } else {
        lockCandidates = intersect(locksHeld, prev.lockCandidates);
      }
    }
    
    boolean hasLockCandidates () {
      return (lockCandidates.length > 0);
    }
    
    boolean isWriteAccess () {
      return ((finsn instanceof PUTFIELD) || (finsn instanceof PUTSTATIC));
    }
    
    FieldAccess getConflict () {
      boolean isWrite = isWriteAccess();
      
      for (FieldAccess c = prev; c != null; c = c.prev) {
        if ((c.ti != ti) && (isWrite != c.isWriteAccess())) {
          return c;
        }
      }
      return null; // no potential conflict found
    }
    
    String describe () {
      String s = isWriteAccess() ? "write" : "read"; 
      s += " from thread: \"";
      s += ti.getName();
      s += "\", locking {";
      for (int i=0; i<locksHeld.length; i++) {
        if (i>0) s += ',';
        s += locksHeld[i];
      }
      s += "} in ";
      s += finsn.getSourceLocation();
      return s;
    }
  }
  
  static class FieldAccessSequence {
    String id;
    FieldAccess lastAccess;
    
    FieldAccessSequence (String id) {
      this.id = id;
    }
      
    void addAccess (FieldAccess fa) {
      fa.prev = lastAccess;
      lastAccess = fa;
      fa.updateLockCandidates();
    }
    
    void purgeLastAccess () {
      lastAccess = lastAccess.prev;
    }
    
  }
    

  /*** private fields and methods ****************************************/
  HashMap fields = new HashMap();
  
  Stack transitions = new Stack();   // the stack of FieldStateChanges
  ArrayList pendingChanges;          // changed FieldStates during the last transition
  FieldAccessSequence raceField;     // if this becomes non-null, we have a race and terminate
  String[] watchFields;              // list of regular expressions to match class/field names
  
  public RaceDetector (Config config) {
    watchFields = config.getStringArray("race.fields");
  }
    
  boolean isWatchedField (FieldInstruction finsn) {
    if (watchFields == null) {
      return true;
    }
    
    String fname = finsn.getVariableId();
    
    for (int i = 0; i<watchFields.length; i++) {
      if (fname.matches(watchFields[i])){
        return true;
      }
    }
    
    return false;
  }
    
  
  /*** GenericProperty **************************************************/
  
  public boolean check(VM vm, Object arg) {
    return (raceField == null);
  }
  
  public String getErrorMessage () {
    return ("potential field race: " + raceField.id);
  }
  
  /*** SearchListener ****************************************************/
  
  public void stateAdvanced(Search search) {
    transitions.push(pendingChanges);
    pendingChanges = null;
  }

  public void stateBacktracked(Search search) {
    ArrayList fops = (ArrayList) transitions.pop();
    if (fops != null) {
      for (Iterator it=fops.iterator(); it.hasNext(); ) {
        FieldAccessSequence fs = (FieldAccessSequence) it.next();
        fs.purgeLastAccess();
      }      
    }
  }
  
  /*** VMListener *******************************************************/
  
  public void instructionExecuted(VM vm) {
    JVM jvm = (JVM)vm;
    Instruction insn = jvm.getLastInstruction();
    
    if (insn instanceof FieldInstruction) {
      ThreadInfo ti = jvm.getLastThreadInfo();
      FieldInstruction finsn = (FieldInstruction)insn;
      String id = null;

      if (raceField != null) { // we only report the first one
        return;
      }
      
      if (ti.hasOtherRunnables() && isWatchedField(finsn)) {
        if (insn instanceof StaticFieldInstruction) { // that's shared per se
          id = finsn.getVariableId();
        } else { // instance field, check if the object is shared
          ElementInfo ei = ((InstanceFieldInstruction)insn).getLastElementInfo();
          if (ei.isShared()) {
            id = finsn.getId(ei); 
          }
        }
        
        if (id != null) {
          FieldAccessSequence fs = (FieldAccessSequence) fields.get(id);
          if (fs == null) { // first time
            fs = new FieldAccessSequence(id);
            fields.put(id, fs);
          }
          
          FieldAccess fa = new FieldAccess(ti, finsn);
          fs.addAccess(fa);
     
          if (pendingChanges == null) {
            pendingChanges = new ArrayList(5);
          }
          pendingChanges.add(fs);
          
          if (!fa.hasLockCandidates()) {
            FieldAccess conflict = fa.getConflict();            
            if (conflict != null) {
              raceField = fs;
              
              System.err.println("potential race detected: " + fs.id);
              System.err.println("\t" + fa.describe());
              System.err.println("\t" + conflict.describe());
            }
          }
        }
      }
    }
  }  
}