src/main/gov/nasa/jpf/listener/BudgetChecker.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.ListenerAdapter;
  23 import gov.nasa.jpf.annotation.JPFOption;
  24 import gov.nasa.jpf.annotation.JPFOptions;
  25 import gov.nasa.jpf.report.Publisher;
  26 import gov.nasa.jpf.search.Search;
  27 import gov.nasa.jpf.vm.Instruction;
  28 import gov.nasa.jpf.vm.ThreadInfo;
  29 import gov.nasa.jpf.vm.VM;
  30
  31 import java.lang.management.ManagementFactory;
  32 import java.lang.management.MemoryMXBean;
  33 import java.lang.management.MemoryUsage;
  34
  35 /**
  36  * Listener that implements various budget constraints
  37  */
  38 @JPFOptions({
  39   @JPFOption(type = "Long", key = "budget.max_time", defaultValue= "-1", comment = "stop search after specified duration [msec]"),
  40   @JPFOption(type = "Long", key = "budget.max_heap", defaultValue = "-1", comment="stop search when VM heapsize reaches specified limit"),
  41   @JPFOption(type = "Int", key = "budget.max_depth", defaultValue = "-1", comment = "stop search at specified search depth"),
  42   @JPFOption(type = "long", key = "budget.max_insn", defaultValue = "-1", comment = "stop search after specified number of intstructions"),
  43   @JPFOption(type = "Int", key = "budget.max_state", defaultValue = "-1", comment = "stop search when reaching specified number of new states"),
  44   @JPFOption(type = "Int", key = "budget.max_new_states", defaultValue = "-1", comment="stop search ater specified number of non-replayed new states")
  45 })
  46 public class BudgetChecker extends ListenerAdapter {
  47
  48   static final int CHECK_INTERVAL = 10000;
  49   static final int CHECK_INTERVAL1 = CHECK_INTERVAL-1;
  50
  51   long tStart;
  52   MemoryUsage muStart;
  53   long mStart;
  54   MemoryMXBean mxb;
  55
  56   VM vm;
  57   Search search;
  58   long insnCount;
  59
  60   //--- the budget thresholds
  61   long maxTime;
  62   long maxHeap;
  63
  64   int maxDepth;
  65   long maxInsn;
  66   int maxState;
  67   int maxNewStates;
  68
  69   int newStates;
  70
  71   // the message explaining the exceeded budget
  72   String message;
  73
  74   public BudgetChecker (Config conf, JPF jpf) {
  75
  76     //--- get the configured budget limits (0 means not set)
  77     maxTime = conf.getDuration("budget.max_time", 0);
  78     maxHeap = conf.getMemorySize("budget.max_heap", 0);
  79     maxDepth = conf.getInt("budget.max_depth", 0);
  80     maxInsn = conf.getLong("budget.max_insn", 0);
  81     maxState = conf.getInt("budget.max_state", 0);
  82     maxNewStates = conf.getInt("budget.max_new_states", 0);
  83
  84     tStart = System.currentTimeMillis();
  85
  86     if (maxHeap > 0) {
  87       mxb = ManagementFactory.getMemoryMXBean();
  88       muStart = mxb.getHeapMemoryUsage();
  89       mStart = muStart.getUsed();
  90     }
  91
  92     search = jpf.getSearch();
  93     vm = jpf.getVM();
  94   }
  95
  96   public boolean timeExceeded() {
  97     if (maxTime > 0) {
  98       long dur = System.currentTimeMillis() - tStart;
  99       if (dur > maxTime) {
 100         message = "max time exceeded: " + Publisher.formatHMS(dur)
 101                + " >= " + Publisher.formatHMS(maxTime);
 102         return true;
 103       }
 104     }
 105
 106     return false;
 107   }
 108
 109   public boolean heapExceeded() {
 110     if (maxHeap > 0) {
 111       MemoryUsage mu = mxb.getHeapMemoryUsage();
 112       long used = mu.getUsed() - mStart;
 113       if (used > maxHeap) {
 114         message = "max heap exceeded: " + (used / (1024*1024)) + "MB"
 115                       + " >= " + (maxHeap / (1024*1024)) + "MB" ;
 116         return true;
 117       }
 118     }
 119
 120     return false;
 121   }
 122
 123   public boolean depthExceeded () {
 124     if (maxDepth > 0) {
 125       int d = search.getDepth();
 126       if (d > maxDepth) {
 127         message = "max search depth exceeded: " + maxDepth;
 128         return true;
 129       }
 130     }
 131
 132     return false;
 133   }
 134
 135   public boolean statesExceeded () {
 136     if (maxState > 0) {
 137       int stateId = vm.getStateId();
 138       if (stateId > maxState) {
 139         message = "max states exceeded: " + maxState;;
 140         return true;
 141       }
 142     }
 143
 144     return false;
 145   }
 146
 147   public boolean insnExceeded () {
 148     if (maxInsn > 0) {
 149       if (insnCount > maxInsn) {
 150         message = "max instruction count exceeded: " + maxInsn;
 151         return true;
 152       }
 153     }
 154     return false;
 155   }
 156
 157   public boolean newStatesExceeded(){
 158     if (maxNewStates > 0){
 159       if (newStates > maxNewStates) {
 160         message = "max new state count exceeded: " + maxNewStates;
 161         return true;
 162       }
 163     }
 164     return false;
 165   }
 166
 167   @Override
 168   public void stateAdvanced (Search search) {
 169     if (timeExceeded() || heapExceeded()) {
 170       search.notifySearchConstraintHit(message);
 171       search.terminate();
 172     }
 173
 174     if (search.isNewState()){
 175       if (!vm.isTraceReplay()){
 176         newStates++;
 177       }
 178       if (statesExceeded() || depthExceeded() || newStatesExceeded()){
 179         search.notifySearchConstraintHit(message);
 180         search.terminate();
 181       }
 182     }
 183   }
 184
 185   @Override
 186   public void instructionExecuted (VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 187     if ((insnCount++ % CHECK_INTERVAL) == CHECK_INTERVAL1) {
 188
 189       if (timeExceeded() || heapExceeded() || insnExceeded()) {
 190         search.notifySearchConstraintHit(message);
 191
 192         vm.getCurrentThread().breakTransition("budgetConstraint");
 193         search.terminate();
 194       }
 195     }
 196   }
 197
 198 }