Menu
▾
▴
[Javapathfinder-devel] javapathfinder/src/gov/nasa/jpf/tools IdleFilter.java,1.3,1.4
|
From: pcm <pcm...@us...> - 2005-09-09 04:55:47
|
Update of /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv12883/src/gov/nasa/jpf/tools Modified Files: IdleFilter.java Log Message: bad, bad back porter! half of the ChoiceGenerator interfacing was missing, the other half was wrong. Added some convenience array getters to Config, but those are not terribly efficient Index: IdleFilter.java =================================================================== RCS file: /cvsroot/javapathfinder/javapathfinder/src/gov/nasa/jpf/tools/IdleFilter.java,v retrieving revision 1.3 retrieving revision 1.4 diff -u -d -r1.3 -r1.4 --- IdleFilter.java 16 Aug 2005 22:27:33 -0000 1.3 +++ IdleFilter.java 9 Sep 2005 04:55:39 -0000 1.4 @@ -36,140 +36,147 @@ import java.util.logging.Logger; /** - * simple combined listener that checks if a thread seems to do idle loops that might starve - * other threads. The most classical case is a "busy wait" loop like + * simple combined listener that checks if a thread seems to do idle loops that + * might starve other threads. The most classical case is a "busy wait" loop + * like * - * for (long l=0; l<1000000; l++); + * for (long l=0; l<1000000; l++); * * which would give us a pretty long path. Even worse, things like - * - * while (true); * - * would never return if we don't break the partial order execution loop. - * Once IdleFilter determines a thread is not doing anything useful (no field access, no array - * element access, no method calls, huge number of back jumps), it breaks the POR loop and - * increases a counter. If it encounters the same thread doing this again consecutively, it - * marks the state as seen, which prunes the whole search tree underneath it + * while (true); + * + * would never return if we don't break the partial order execution loop. Once + * IdleFilter determines a thread is not doing anything useful (no field access, + * no array element access, no method calls, huge number of back jumps), it + * breaks the POR loop and increases a counter. If it encounters the same thread + * doing this again consecutively, it marks the state as seen, which prunes the + * whole search tree underneath it */ public class IdleFilter extends ListenerAdapter { - static Logger log = JPF.getLogger("gov.nasa.jpf.tools.IdleFilter"); + static Logger log = JPF.getLogger("gov.nasa.jpf.tools.IdleFilter"); - static class ThreadStat { - String tname; - int backJumps; - boolean isCleared = false; - int loopStartPc; - int loopEndPc; - int loopStackDepth; + static class ThreadStat { + String tname; - ThreadStat(String tname) { - this.tname = tname; - } - } + int backJumps; - DynamicObjectArray threadStats = new DynamicObjectArray(16); - ThreadStat ts; - int maxBackJumps; - boolean jumpPast; + boolean isCleared = false; - //----------------------------------------------------- SearchListener interface + int loopStartPc; - public IdleFilter(Config config) { - maxBackJumps = config.getInt("idle.max_backjumps", 500); - jumpPast = config.getBoolean("idle.jump", false); - } + int loopEndPc; - public void stateAdvanced(Search search) { - ts.backJumps = 0; - ts.isCleared = false; - ts.loopStackDepth = 0; - ts.loopStartPc = ts.loopEndPc = 0; - } + int loopStackDepth; - public void stateBacktracked(Search search) { - ts.backJumps = 0; - ts.isCleared = false; - ts.loopStackDepth = 0; - ts.loopStartPc = ts.loopEndPc = 0; - } + ThreadStat(String tname) { + this.tname = tname; + } + } - //----------------------------------------------------- VMListener interface - public void instructionExecuted(VM vm) { - JVM jvm = (JVM) vm; - Instruction insn = jvm.getLastInstruction(); - ThreadInfo ti = jvm.getLastThreadInfo(); + DynamicObjectArray threadStats = new DynamicObjectArray(16); - int tid = ti.getIndex(); - ts = (ThreadStat) threadStats.get(tid); - if (ts == null) { - ts = new ThreadStat(ti.getName()); - threadStats.set(tid, ts); - } + ThreadStat ts; - if (insn.isBackJump()) { - ts.backJumps++; + int maxBackJumps; - int loopStackDepth = ti.countStackFrames(); - int loopPc = jvm.getNextInstruction().getPosition(); + boolean jumpPast; - 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) { + // ----------------------------------------------------- SearchListener + // interface - ti.yield(); // this breaks the executePorStep loop - MethodInfo mi = insn.getMethod(); - ClassInfo ci = mi.getClassInfo(); - int line = mi.getLineNumber(insn); - String file = ci.getSourceFileName(); + public IdleFilter(Config config) { + maxBackJumps = config.getInt("idle.max_backjumps", 500); + jumpPast = config.getBoolean("idle.jump", false); + } - if (jumpPast) { - Instruction next = insn.getNext(); - ti.setPC(next); + public void stateAdvanced(Search search) { + ts.backJumps = 0; + ts.isCleared = false; + ts.loopStackDepth = 0; + ts.loopStartPc = ts.loopEndPc = 0; + } - 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 + ")"); - } - } - } - } + public void stateBacktracked(Search search) { + ts.backJumps = 0; + ts.isCleared = false; + ts.loopStackDepth = 0; + ts.loopStartPc = ts.loopEndPc = 0; + } - } 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(); + // ----------------------------------------------------- VMListener interface + public void instructionExecuted(VM vm) { + JVM jvm = (JVM) vm; + Instruction insn = jvm.getLastInstruction(); + ThreadInfo ti = jvm.getLastThreadInfo(); - if (stackDepth == ts.loopStackDepth) { - if ((pc >= ts.loopStartPc) && (pc < ts.loopEndPc)) { - ts.isCleared = true; - } - } - } - } - } + int tid = ti.getIndex(); + ts = (ThreadStat) threadStats.get(tid); + if (ts == null) { + ts = new ThreadStat(ti.getName()); + threadStats.set(tid, ts); + } + + if (insn.isBackJump()) { + ts.backJumps++; + + int loopStackDepth = ti.countStackFrames(); + int loopPc = jvm.getNextInstruction().getPosition(); + + 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) { + + ti.yield(); // this breaks the executePorStep loop + MethodInfo mi = insn.getMethod(); + ClassInfo ci = mi.getClassInfo(); + int line = mi.getLineNumber(insn); + String file = ci.getSourceFileName(); + + if (jumpPast) { + // pretty bold, we jump past the loop end and go on from there + + 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 off - 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 (!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; + } + } + } + } + } } |
