[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools IdleFilter.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-serv29755/src/gov/nasa/jpf/tools

Modified Files:
	IdleFilter.java 
Log Message:
tried to refine the IdleFilter heuristics a bit:

(1) we now store the loop bounds/stackdepth, and only shortcut the test if we
have array or invoke insns inside the last loop. This should take care of the
case where we have such insns BEFORE we enter the critical loop, thus cutting it off before it really starts to do it's magic

(2) we now even have an option to jump past the end of the loop, and continue
from there. Sounds dangerous, but hey - we give a warning

(3) added log warnings for both search pruning and jump around

(4) changed the ThreadStat store from a slow HashMap to a thread index based
DynamicObjectArray. Should make things a bit faster

(5) using the ts.IsCleared shortcut in the non-GOTO branch (which is the 
vast majority) should also accelerate things a bit

Index: IdleFilter.java
===================================================================
RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.java,v
retrieving revision 1.1
retrieving revision 1.2
diff -u -d -r1.1 -r1.2
--- IdleFilter.java	10 May 2005 06:46:54 -0000	1.1
+++ IdleFilter.java	16 Aug 2005 06:50:21 -0000	1.2
@@ -19,16 +19,21 @@
 package gov.nasa.jpf.tools;
 
 import gov.nasa.jpf.Config;
+import gov.nasa.jpf.JPF;
 import gov.nasa.jpf.Search;
 import gov.nasa.jpf.ListenerAdapter;
 import gov.nasa.jpf.VM;
+import gov.nasa.jpf.jvm.ClassInfo;
 import gov.nasa.jpf.jvm.JVM;
+import gov.nasa.jpf.jvm.MethodInfo;
 import gov.nasa.jpf.jvm.ThreadInfo;
 import gov.nasa.jpf.jvm.bytecode.ArrayStoreInstruction;
 import gov.nasa.jpf.jvm.bytecode.Instruction;
 import gov.nasa.jpf.jvm.bytecode.InvokeInstruction;
+import gov.nasa.jpf.util.DynamicObjectArray;
 
 import java.util.HashMap;
+import java.util.logging.Logger;
 
 /**
  * simple combined listener that checks if a thread seems to do idle loops that might starve
@@ -48,40 +53,51 @@
  */
 public class IdleFilter extends ListenerAdapter {
     
+  static Logger log = JPF.getLogger("gov.nasa.jpf.tools.IdleFilter");
+  
   static class ThreadStat {
     String tname;
     int strikes;
     int backJumps;
     boolean isCleared = false;
     
+    int loopStartPc;
+    int loopEndPc;
+    int loopStackDepth;
+    
     ThreadStat (String tname) {
       this.tname = tname;
     }
   }
   
-  HashMap threadStats = new HashMap();
-  
+  DynamicObjectArray threadStats = new DynamicObjectArray(16);  
   ThreadStat ts;
   
   int maxStrikes;
   int maxBackJumps;
+  boolean jumpPast;
   
   //----------------------------------------------------- SearchListener interface
 
   public IdleFilter (Config config) {
     maxBackJumps = config.getInt("idle.max_backjumps", 500);
     maxStrikes = config.getInt("idle.max_strikes", 1);
+    jumpPast = config.getBoolean("idle.jump", false);
   }
   
   public void stateAdvanced(Search search) {
     ts.backJumps = 0;
     ts.isCleared = false;
+    ts.loopStackDepth = 0;
+    ts.loopStartPc = ts.loopEndPc = 0;
   }
 
   public void stateBacktracked(Search search) {
     ts.strikes = 0;
     ts.backJumps = 0;
     ts.isCleared = false;
+    ts.loopStackDepth = 0;
+    ts.loopStartPc = ts.loopEndPc = 0;
   }
   
   //----------------------------------------------------- VMListener interface
@@ -90,31 +106,74 @@
     Instruction insn = jvm.getLastInstruction();
     ThreadInfo ti = jvm.getLastThreadInfo();
 
-    String tid = ti.getName(); // not ideal, but still better than boxing int's
+    int tid = ti.getIndex();
     ts = (ThreadStat)threadStats.get(tid);
     if (ts == null) {
-      ts = new ThreadStat(tid);
-      threadStats.put(tid, ts);
+      ts = new ThreadStat(ti.getName());
+      threadStats.set(tid,ts);
     }
     
-    if (insn.isBackJump() && !ts.isCleared ) {
+    if (insn.isBackJump()) {
       ts.backJumps++;
+    
+      int loopStackDepth = ti.countStackFrames();
+      int loopPc = jvm.getNextInstruction().getPosition();
       
-      if (ts.backJumps > maxBackJumps) {
-        ti.yield();
-        ts.strikes++;
+      if ((loopStackDepth != ts.loopStackDepth) || (loopPc != ts.loopStartPc)) {
+        // new loop, reset
+        ts.isCleared = false;
+        ts.loopStackDepth = loopStackDepth;
+        ts.loopStartPc = loopPc;
+        ts.loopEndPc = insn.getPosition();
+        ts.backJumps = 0;
+      } else {
+        if (!ts.isCleared) {
+          if (ts.backJumps > maxBackJumps) {
         
-        if (ts.strikes > maxStrikes) {
-          // cut this sucker of - we declare this a visited state
-          // <2do> - we should probably issue a warning message here
-          jvm.setIgnoreState(true);
+            ti.yield();  // this breaks the executePorStep loop
+            ts.strikes++;
+            
+            if (ts.strikes > maxStrikes) {
+
+              MethodInfo mi = insn.getMethod();
+              ClassInfo ci = mi.getClassInfo();
+              int line = mi.getLineNumber(insn);
+              String file = ci.getSourceFileName();
+
+              if (jumpPast) {
+                Instruction next = insn.getNext();
+                ti.setPC(next);
+
+                log.warning("WARNING: IdleFilter jumped past loop in: " + ti.getName() + 
+                            "\n\tat " + ci.getName() + "." + mi.getName() +
+                            "(" + file + ":" + line + ")");
+              } else {
+                // cut this sucker of - we declare this a visited state
+                jvm.setIgnoreState(true);
+                            
+                log.warning("WARNING: IdleFilter pruned thread: " + ti.getName() + 
+                            "\n\tat " + ci.getName() + "." + mi.getName() +
+                            "(" + file + ":" + line + ")");
+              }
+            }
+          }          
         }
       }
-    } else if (insn instanceof InvokeInstruction) {
-      ts.isCleared=true; // shut it off for this forward
-    } else if (insn instanceof ArrayStoreInstruction) {
-      ts.isCleared=true;
-    }
+      
+    } else if (!ts.isCleared) {
+      // if we call methods or set array elements inside the loop in question, we
+      // assume this is not an idle loop and terminate the checks
+      if ((insn instanceof InvokeInstruction) || (insn instanceof ArrayStoreInstruction)) {
+        int stackDepth = ti.countStackFrames();
+        int pc = insn.getPosition();
+
+        if (stackDepth == ts.loopStackDepth) {
+          if ((pc >= ts.loopStartPc) && (pc < ts.loopEndPc)) {
+            ts.isCleared = true;
+          }
+        }
+      }
+    }      
   }
   
 }