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

Added Files:
	IdleFilter.java 
Log Message:
moved the idle loop detection out of the core and into gov.nasa.jpf.tools.IdleFilter listener, which
is also a bit more sophisticated. It checks not just for back jump threshold, but abandons the test if it
detects ArrayStoreInstructions or InvokeInstructions, assuming both are doing stuff that shouldn't be
ignored. The thing can be made vastly more sophisticated, but it nicely shows what can be done
with listeners. It passes the

  int[] a = new int[500]; // init loop  -> pass
  for (int i=0; i<a.length; i++) a[i] = i; 

   for (long l=0; l<1000000; l++); // bad idle loop  -> filter

test. To ease creation of listeners like this, I've also added a ListenerAdapter, which dummy implements
both VMListener and SearchListener, so that tools only have to override their relevant notificatiion
methods

--- NEW FILE: IdleFilter.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 gov.nasa.jpf.Config;
import gov.nasa.jpf.Search;
import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.VM;
import gov.nasa.jpf.jvm.JVM;
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 java.util.HashMap;

/**
 * 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++);
 * 
 * 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
 */
public class IdleFilter extends ListenerAdapter {
    
  static class ThreadStat {
    String tname;
    int strikes;
    int backJumps;
    boolean isCleared = false;
    
    ThreadStat (String tname) {
      this.tname = tname;
    }
  }
  
  HashMap threadStats = new HashMap();
  
  ThreadStat ts;
  
  int maxStrikes;
  int maxBackJumps;
  
  //----------------------------------------------------- SearchListener interface

  public IdleFilter (Config config) {
    maxBackJumps = config.getInt("idle.max_backjumps", 500);
    maxStrikes = config.getInt("idle.max_strikes", 1);
  }
  
  public void stateAdvanced(Search search) {
    ts.backJumps = 0;
    ts.isCleared = false;
  }

  public void stateBacktracked(Search search) {
    ts.strikes = 0;
    ts.backJumps = 0;
    ts.isCleared = false;
  }
  
  //----------------------------------------------------- VMListener interface
  public void instructionExecuted(VM vm) {
    JVM jvm = (JVM)vm;
    Instruction insn = jvm.getLastInstruction();
    ThreadInfo ti = jvm.getLastThreadInfo();

    String tid = ti.getName(); // not ideal, but still better than boxing int's
    ts = (ThreadStat)threadStats.get(tid);
    if (ts == null) {
      ts = new ThreadStat(tid);
      threadStats.put(tid, ts);
    }
    
    if (insn.isBackJump() && !ts.isCleared ) {
      ts.backJumps++;
      
      if (ts.backJumps > maxBackJumps) {
        ti.yield();
        ts.strikes++;
        
        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);
        }
      }
    } else if (insn instanceof InvokeInstruction) {
      ts.isCleared=true; // shut it off for this forward
    } else if (insn instanceof ArrayStoreInstruction) {
      ts.isCleared=true;
    }
  }
  
}