src/main/gov/nasa/jpf/listener/IdleFilter.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   6  * The Java Pathfinder core (jpf-core) platform is licensed under the
   7  * Apache License, Version 2.0 (the "License"); you may not use this file except
   8  * in compliance with the License. You may obtain a copy of the License at
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  12  * Unless required by applicable law or agreed to in writing, software
  13  * distributed under the License is distributed on an "AS IS" BASIS,
  14  * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  15  * See the License for the specific language governing permissions and
  16  * limitations under the License.
  17  */
  18 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22 import gov.nasa.jpf.JPFConfigException;
  23 import gov.nasa.jpf.PropertyListenerAdapter;
  24 import gov.nasa.jpf.jvm.bytecode.ArrayStoreInstruction;
  25 import gov.nasa.jpf.jvm.bytecode.JVMInvokeInstruction;
  26 import gov.nasa.jpf.search.Search;
  27 import gov.nasa.jpf.util.DynamicObjectArray;
  28 import gov.nasa.jpf.vm.ClassInfo;
  29 import gov.nasa.jpf.vm.Instruction;
  30 import gov.nasa.jpf.vm.VM;
  31 import gov.nasa.jpf.vm.MethodInfo;
  32 import gov.nasa.jpf.vm.ThreadInfo;
  33
  34 import java.util.logging.Logger;
  35
  36 /**
  37  * simple combined listener that checks if a thread seems to do idle loops that
  38  * might starve other threads or JPF. The most classical case is a "busy wait" loop
  39  * like
  40  *
  41  *   for (long l=0; l<1000000; l++);
  42  *
  43  * which would give us a pretty long path. Even worse, things like
  44  *
  45  *   while (true);
  46  *
  47  * would (just like in a normal VM) never terminate in JPF, even though people
  48  * familiar with model checking would expect state matching. Only that without
  49  * a transition break, JPF has no reason to match states, so we have to
  50  * automatically add a break on the backjump. We shouldn't add one on every
  51  * backjump though because that might cause a lot of overhead in programs that
  52  * do terminate.
  53  *
  54  * IdleFilter has two options:
  55  *   idle.max_backjumps : sets the number of backjumps after which we break
  56  *   idle.action : what to do if max_backjumps are exceeded in the same thread
  57  *                 on the same location and stackframe
  58  *     warn : only print warning for backjumps exceeding the max_backjumps
  59  *     break : break the transition to allow state matching
  60  *     prune : unconditionally prune the search
  61  *     jump : jump past the backjump (this is dangerous if the loop has side effects)
  62  */
  63 public class IdleFilter extends PropertyListenerAdapter {
  64
  65   static Logger log = JPF.getLogger("gov.nasa.jpf.listener.IdleFilter");
  66
  67   static class ThreadStat {
  68     String tname;
  69
  70     int backJumps;
  71
  72     boolean isCleared = false;
  73
  74     int loopStartPc;
  75
  76     int loopEndPc;
  77
  78     int loopStackDepth;
  79
  80     ThreadStat(String tname) {
  81       this.tname = tname;
  82     }
  83   }
  84
  85   static enum Action { JUMP, PRUNE, BREAK, YIELD, WARN }
  86
  87   DynamicObjectArray<ThreadStat> threadStats = new DynamicObjectArray<ThreadStat>(4,16);
  88
  89   ThreadStat ts;
  90
  91   // we use this to remember that we just broke the transition
  92   boolean brokeTransition;
  93
  94   int maxBackJumps;
  95   Action action;
  96
  97
  98   // ----------------------------------------------------- SearchListener
  99   // interface
 100
 101   public IdleFilter(Config config) {
 102     maxBackJumps = config.getInt("idle.max_backjumps", 500);
 103
 104     String act = config.getString("idle.action", "break");
 105     if ("warn".equalsIgnoreCase(act)){
 106       action = Action.WARN;
 107     } else if ("break".equalsIgnoreCase(act)){
 108       action = Action.BREAK;
 109     } else if ("yield".equalsIgnoreCase(act)){
 110       action = Action.YIELD;
 111     } else if ("prune".equalsIgnoreCase(act)){
 112       action = Action.PRUNE;
 113     } else if ("jump".equalsIgnoreCase(act)){
 114       action = Action.JUMP;
 115     } else {
 116       throw new JPFConfigException("unknown IdleFilter action: " +act);
 117     }
 118
 119   }
 120
 121   @Override
 122   public void stateAdvanced(Search search) {
 123     ts.backJumps = 0;
 124     ts.isCleared = false;
 125     ts.loopStackDepth = 0;
 126     ts.loopStartPc = ts.loopEndPc = 0;
 127
 128     brokeTransition = false;
 129   }
 130
 131   @Override
 132   public void stateBacktracked(Search search) {
 133     ts.backJumps = 0;
 134     ts.isCleared = false;
 135     ts.loopStackDepth = 0;
 136     ts.loopStartPc = ts.loopEndPc = 0;
 137   }
 138
 139   // ----------------------------------------------------- VMListener interface
 140   @Override
 141   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 142
 143     int tid = ti.getId();
 144     ts = threadStats.get(tid);
 145     if (ts == null) {
 146       ts = new ThreadStat(ti.getName());
 147       threadStats.set(tid, ts);
 148     }
 149
 150     if (executedInsn.isBackJump()) {
 151       ts.backJumps++;
 152
 153       int loopStackDepth = ti.getStackDepth();
 154       int loopPc = nextInsn.getPosition();
 155
 156       if ((loopStackDepth != ts.loopStackDepth) || (loopPc != ts.loopStartPc)) {
 157         // new loop, reset
 158         ts.isCleared = false;
 159         ts.loopStackDepth = loopStackDepth;
 160         ts.loopStartPc = loopPc;
 161         ts.loopEndPc = executedInsn.getPosition();
 162         ts.backJumps = 0;
 163
 164       } else {
 165         if (!ts.isCleared) {
 166           if (ts.backJumps > maxBackJumps) {
 167
 168             ti.reschedule("idleFilter"); // this breaks the executePorStep loop
 169             MethodInfo mi = executedInsn.getMethodInfo();
 170             ClassInfo ci = mi.getClassInfo();
 171             int line = mi.getLineNumber(executedInsn);
 172             String file = ci.getSourceFileName();
 173
 174             switch (action) {
 175               case JUMP:
 176                 // pretty bold, we jump past the loop end and go on from there
 177
 178                 Instruction next = executedInsn.getNext();
 179                 ti.setNextPC(next);
 180
 181                 log.warning("jumped past loop in: " + ti.getName() +
 182                         "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
 183                 break;
 184
 185               case PRUNE:
 186                 // cut this sucker off - we declare this a visited state
 187                 vm.ignoreState();
 188                 log.warning("pruned thread: " + ti.getName() +
 189                         "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
 190                 break;
 191
 192               case BREAK:
 193                 // just break the transition and let the state matching take over
 194                 brokeTransition = true;
 195                 ti.breakTransition("breakIdleLoop");
 196
 197                 log.warning("breaks transition on suspicious loop in thread: " + ti.getName() +
 198                         "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
 199
 200                 break;
 201
 202               case YIELD:
 203                 // give other threads a chance to run
 204                 brokeTransition = true;
 205                 ti.reschedule("rescheduleIdleLoop");
 206
 207                 log.warning("yield on suspicious loop in thread: " + ti.getName() +
 208                         "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
 209
 210                 break;
 211
 212               case WARN:
 213                 log.warning("detected suspicious loop in thread: " + ti.getName() +
 214                         "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
 215                 break;
 216
 217             }
 218           }
 219         }
 220       }
 221
 222     } else if (!ts.isCleared) {
 223       // if we call methods or set array elements inside the loop in question,
 224       // we assume this is not an idle loop and terminate the checks
 225       // <2do> this is too restrictive - we should leave this to state matching
 226
 227       if ((executedInsn instanceof JVMInvokeInstruction)
 228           || (executedInsn instanceof ArrayStoreInstruction)) {
 229         int stackDepth = ti.getStackDepth();
 230         int pc = executedInsn.getPosition();
 231
 232         if (stackDepth == ts.loopStackDepth) {
 233           if ((pc >= ts.loopStartPc) && (pc < ts.loopEndPc)) {
 234             ts.isCleared = true;
 235           }
 236         }
 237       }
 238     }
 239   }
 240
 241   // thread ids are reused, so we have to clean up
 242   @Override
 243   public void threadTerminated (VM vm, ThreadInfo ti){
 244     int tid = ti.getId();
 245     threadStats.set(tid, null);
 246   }
 247
 248
 249 }