2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
18 package gov.nasa.jpf.listener;
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;
34 import java.util.logging.Logger;
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
41 * for (long l=0; l<1000000; l++);
43 * which would give us a pretty long path. Even worse, things like
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
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)
63 public class IdleFilter extends PropertyListenerAdapter {
65 static Logger log = JPF.getLogger("gov.nasa.jpf.listener.IdleFilter");
67 static class ThreadStat {
72 boolean isCleared = false;
80 ThreadStat(String tname) {
85 static enum Action { JUMP, PRUNE, BREAK, YIELD, WARN }
87 DynamicObjectArray<ThreadStat> threadStats = new DynamicObjectArray<ThreadStat>(4,16);
91 // we use this to remember that we just broke the transition
92 boolean brokeTransition;
98 // ----------------------------------------------------- SearchListener
101 public IdleFilter(Config config) {
102 maxBackJumps = config.getInt("idle.max_backjumps", 500);
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;
116 throw new JPFConfigException("unknown IdleFilter action: " +act);
122 public void stateAdvanced(Search search) {
124 ts.isCleared = false;
125 ts.loopStackDepth = 0;
126 ts.loopStartPc = ts.loopEndPc = 0;
128 brokeTransition = false;
132 public void stateBacktracked(Search search) {
134 ts.isCleared = false;
135 ts.loopStackDepth = 0;
136 ts.loopStartPc = ts.loopEndPc = 0;
139 // ----------------------------------------------------- VMListener interface
141 public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
143 int tid = ti.getId();
144 ts = threadStats.get(tid);
146 ts = new ThreadStat(ti.getName());
147 threadStats.set(tid, ts);
150 if (executedInsn.isBackJump()) {
153 int loopStackDepth = ti.getStackDepth();
154 int loopPc = nextInsn.getPosition();
156 if ((loopStackDepth != ts.loopStackDepth) || (loopPc != ts.loopStartPc)) {
158 ts.isCleared = false;
159 ts.loopStackDepth = loopStackDepth;
160 ts.loopStartPc = loopPc;
161 ts.loopEndPc = executedInsn.getPosition();
166 if (ts.backJumps > maxBackJumps) {
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();
176 // pretty bold, we jump past the loop end and go on from there
178 Instruction next = executedInsn.getNext();
181 log.warning("jumped past loop in: " + ti.getName() +
182 "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
186 // cut this sucker off - we declare this a visited state
188 log.warning("pruned thread: " + ti.getName() +
189 "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
193 // just break the transition and let the state matching take over
194 brokeTransition = true;
195 ti.breakTransition("breakIdleLoop");
197 log.warning("breaks transition on suspicious loop in thread: " + ti.getName() +
198 "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
203 // give other threads a chance to run
204 brokeTransition = true;
205 ti.reschedule("rescheduleIdleLoop");
207 log.warning("yield on suspicious loop in thread: " + ti.getName() +
208 "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
213 log.warning("detected suspicious loop in thread: " + ti.getName() +
214 "\n\tat " + ci.getName() + "." + mi.getName() + "(" + file + ":" + line + ")");
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
227 if ((executedInsn instanceof JVMInvokeInstruction)
228 || (executedInsn instanceof ArrayStoreInstruction)) {
229 int stackDepth = ti.getStackDepth();
230 int pc = executedInsn.getPosition();
232 if (stackDepth == ts.loopStackDepth) {
233 if ((pc >= ts.loopStartPc) && (pc < ts.loopEndPc)) {
241 // thread ids are reused, so we have to clean up
243 public void threadTerminated (VM vm, ThreadInfo ti){
244 int tid = ti.getId();
245 threadStats.set(tid, null);