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

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

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

Modified Files:
	RaceDetector.java 
Log Message:
Ok, since I claimed it would be easy to check for cycles, I've just added this. It's still a bit over-simplified, since we don't check for identical call stacks in each access thread, but again I claim that's easy enough (hashing ThreadInfo call stacks could probably be quite handy for other things too, so I will add it there). In fact, RaceDetector changes would be minor (the FieldAccess ctor and equal()), and it now can deal with sync by signals 

Index: RaceDetector.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/RaceDetector.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- RaceDetector.java	25 Aug 2005 17:02:16 -0000	1.1
+++ RaceDetector.java	25 Aug 2005 18:22:57 -0000	1.2
@@ -62,6 +62,8 @@
       this.ti = ti;
       this.finsn = finsn;
       this.locksHeld = ti.getLockedObjects().toArray();
+      
+      // <2do> we should also hash the threads callstack here
     }
   
     Object[] intersect (Object[] a, Object[] b) {
@@ -104,11 +106,23 @@
       return null; // no potential conflict found
     }
     
+    public boolean equals (Object other) {
+      if (other instanceof FieldAccess) {
+        FieldAccess fa = (FieldAccess)other;
+        if (ti != fa.ti) return false;
+        if (finsn != fa.finsn) return false;
+        // <2do> we should also check for same callstack, but that's a detail we leave out for now
+        
+        return true;
+      }
+      return false;
+    }
+    
     String describe () {
       String s = isWriteAccess() ? "write" : "read"; 
       s += " from thread: \"";
       s += ti.getName();
-      s += "\", locking {";
+      s += "\", holding locks {";
       for (int i=0; i<locksHeld.length; i++) {
         if (i>0) s += ',';
         s += locksHeld[i];
@@ -145,11 +159,18 @@
   
   Stack transitions = new Stack();   // the stack of FieldStateChanges
   ArrayList pendingChanges;          // changed FieldStates during the last transition
+  FieldAccess access1, access2;      // our race candidates (race if encountered in reverse order)
   FieldAccessSequence raceField;     // if this becomes non-null, we have a race and terminate
+  
   String[] watchFields;              // list of regular expressions to match class/field names
+  boolean terminate;                 // terminate search when we found a (potential) race
+  boolean verifyCycle;               // don't report potentials, go on until encountering
+                                     // the suspicious insns in both orders
   
   public RaceDetector (Config config) {
     watchFields = config.getStringArray("race.fields");
+    terminate = config.getBoolean("race.terminate", true);
+    verifyCycle = config.getBoolean("race.verify_cycle", false);
   }
     
   boolean isWatchedField (FieldInstruction finsn) {
@@ -239,11 +260,29 @@
           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());
+              if (verifyCycle) {
+                if (access1 != null) {
+                  if (fa.equals(access2) && conflict.equals(access1)) {
+                    if (terminate) {
+                      raceField = fs;
+                    }
+                    System.err.println("race detected (access occurred in both orders): " + fs.id);
+                    System.err.println("\t" + fa.describe());
+                    System.err.println("\t" + conflict.describe());                    
+                  }
+                } else {
+                  access1 = fa;
+                  access2 = conflict;
+                }
+              } else {
+                if (terminate) {
+                  raceField = fs;
+                }
+                System.err.println("potential race detected: " + fs.id);
+                System.err.println("\t" + fa.describe());
+                System.err.println("\t" + conflict.describe());
+              }              
             }
           }
         }