src/main/gov/nasa/jpf/vm/AllRunnablesSyncPolicy.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
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
  23
  24 /**
  25  * a Scheduler implementation base class that allows filtering of runnable threads and
  26  * implements SyncPolicy without backtracking or empty transitions, i.e. choice sets that
  27  * include all runnable threads
  28  */
  29 public class AllRunnablesSyncPolicy implements SyncPolicy {
  30
  31   protected VM vm;
  32   protected boolean breakSingleChoice;
  33   protected boolean breakLockRelease;
  34   protected boolean breakNotify;
  35   protected boolean breakSleep;
  36   protected boolean breakYield;
  37   protected boolean breakPriority;
  38
  39   public AllRunnablesSyncPolicy (Config config){
  40     breakSingleChoice = config.getBoolean("cg.break_single_choice", false);
  41     breakLockRelease = config.getBoolean("cg.break_lock_release", true);
  42     breakNotify = config.getBoolean("cg.break_notify", true);
  43     breakSleep = config.getBoolean("cg.break_sleep", true);
  44     breakYield = config.getBoolean("cg.break_yield", true);
  45     breakPriority = config.getBoolean("cg.break_priority", true);
  46   }
  47
  48
  49   //--- internal methods
  50
  51   /**
  52    * this is the main policy method that can be overridden by subclasses, e.g. by filtering
  53    * out the highest priority runnables, or by ordering according to priority
  54    *
  55    * Default behavior is to first try to find runnables within the provided ApplicationContext,
  56    * and fall back to any runnable if there are none in this context
  57    *
  58    * this includes threads that are in operations that can timeout
  59    */
  60   protected ThreadInfo[] getTimeoutRunnables (ApplicationContext appCtx){
  61     ThreadList tlist = vm.getThreadList();
  62
  63     if (tlist.hasProcessTimeoutRunnables(appCtx)){
  64       return tlist.getProcessTimeoutRunnables(appCtx);
  65     } else {
  66       return tlist.getTimeoutRunnables();
  67     }
  68   }
  69
  70
  71   protected ChoiceGenerator<ThreadInfo> getRunnableCG (String id, ThreadInfo tiCurrent){
  72     ApplicationContext appCtx = tiCurrent.getApplicationContext();
  73     ThreadInfo[] choices = getTimeoutRunnables(appCtx);
  74
  75     if (choices.length == 0){
  76       return null;
  77     }
  78
  79     if ((choices.length == 1) && (choices[0] == tiCurrent) && !tiCurrent.isTimeoutWaiting()){ // no context switch
  80       if (!breakSingleChoice){
  81         return null;
  82       }
  83     }
  84
  85     ChoiceGenerator<ThreadInfo> cg = new ThreadChoiceFromSet( id, choices, true);
  86
  87     if(!vm.getThreadList().hasProcessTimeoutRunnables(appCtx)) {
  88       GlobalSchedulingPoint.setGlobal(cg);
  89     }
  90
  91     return cg;
  92   }
  93
  94   protected boolean setNextChoiceGenerator (ChoiceGenerator<ThreadInfo> cg){
  95     if (cg != null){
  96       return vm.getSystemState().setNextChoiceGenerator(cg); // listeners could still remove CGs
  97     } else {
  98       return false;
  99     }
 100   }
 101
 102   /**
 103    * set a runnable CG that is optional if we are in a atomic section
 104    */
 105   protected boolean setNonBlockingCG (String id, ThreadInfo tiCurrent){
 106     if (!tiCurrent.isFirstStepInsn() || tiCurrent.isEmptyTransitionEnabled()) {
 107       if (vm.getSystemState().isAtomic()) {
 108         return false;
 109       } else {
 110         return setNextChoiceGenerator(getRunnableCG(id, tiCurrent));
 111       }
 112
 113     } else {
 114       return false;  // no empty transitions
 115     }
 116   }
 117
 118   protected static ChoiceGenerator<ThreadInfo> blockedWithoutChoice =
 119           new ThreadChoiceFromSet("BLOCKED_NO_CHOICE", new ThreadInfo[0], true);
 120
 121   /**
 122    * set a runnable CG that would break a atomic section because it requires
 123    * a context switch
 124    */
 125   protected boolean setBlockingCG (String id, ThreadInfo tiCurrent){
 126     if (!tiCurrent.isFirstStepInsn() || tiCurrent.isEmptyTransitionEnabled()) {
 127       if (vm.getSystemState().isAtomic()) {
 128         vm.getSystemState().setBlockedInAtomicSection();
 129       }
 130
 131       ChoiceGenerator<ThreadInfo> cg = getRunnableCG(id, tiCurrent);
 132       if (cg == null){ // make sure we don't mask a deadlock
 133         if (vm.getThreadList().hasLiveThreads()){
 134           cg = blockedWithoutChoice;
 135         }
 136       }
 137
 138       return setNextChoiceGenerator(cg);
 139
 140     } else {
 141       return false;  // no empty transitions
 142     }
 143   }
 144
 145   /**
 146    * set a runnable CG that only breaks a atomic section if the blocking thread
 147    * is the currently executing one
 148    */
 149   protected boolean setMaybeBlockingCG (String id, ThreadInfo tiCurrent, ThreadInfo tiBlock){
 150     if (tiCurrent == tiBlock){
 151       return setBlockingCG( id, tiCurrent);
 152     } else {
 153       return setNonBlockingCG( id, tiCurrent);
 154     }
 155   }
 156
 157
 158   //--- SyncPolicy interface
 159
 160   //--- initialization
 161   @Override
 162   public void initializeSyncPolicy (VM vm, ApplicationContext appCtx){
 163     this.vm  = vm;
 164   }
 165
 166   @Override
 167   public void initializeThreadSync (ThreadInfo tiCurrent, ThreadInfo tiNew){
 168   }
 169
 170   //--- locks
 171   @Override
 172   public boolean setsBlockedThreadCG (ThreadInfo ti, ElementInfo ei){
 173     return setBlockingCG( BLOCK, ti);
 174   }
 175
 176   @Override
 177   public boolean setsLockAcquisitionCG (ThreadInfo ti, ElementInfo ei){
 178     return setNonBlockingCG( LOCK, ti);
 179   }
 180
 181   @Override
 182   public boolean setsLockReleaseCG (ThreadInfo ti, ElementInfo ei, boolean didUnblock){
 183     if (breakLockRelease){
 184       if (didUnblock){
 185         return setNonBlockingCG( RELEASE, ti);
 186       }
 187     }
 188
 189     return false;
 190   }
 191
 192   //--- thread termination
 193   @Override
 194   public boolean setsTerminationCG (ThreadInfo ti){
 195     return setBlockingCG( TERMINATE, ti);
 196   }
 197
 198   //--- java.lang.Object APIs
 199   @Override
 200   public boolean setsWaitCG (ThreadInfo ti, long timeout){
 201     return setBlockingCG( WAIT, ti);
 202   }
 203
 204   @Override
 205   public boolean setsNotifyCG (ThreadInfo ti, boolean didNotify){
 206     if (breakNotify){
 207       if (didNotify){
 208         return setNonBlockingCG( NOTIFY, ti);
 209       }
 210     }
 211
 212     return false;
 213   }
 214
 215   @Override
 216   public boolean setsNotifyAllCG (ThreadInfo ti, boolean didNotify){
 217     if (breakNotify){
 218       if (didNotify){
 219         return setNonBlockingCG( NOTIFYALL, ti);
 220       }
 221     }
 222
 223     return false;
 224   }
 225
 226
 227   //--- the java.lang.Thread APIs
 228   @Override
 229   public boolean setsStartCG (ThreadInfo tiCurrent, ThreadInfo tiStarted){
 230     return setNonBlockingCG( START, tiCurrent);
 231   }
 232
 233   @Override
 234   public boolean setsYieldCG (ThreadInfo ti){
 235     if (breakYield){
 236       return setNonBlockingCG( YIELD, ti);
 237     } else {
 238       return false;
 239     }
 240   }
 241
 242   @Override
 243   public boolean setsPriorityCG (ThreadInfo ti){
 244     if (breakPriority){
 245       return setNonBlockingCG( PRIORITY, ti);
 246     } else {
 247       return false;
 248     }
 249   }
 250
 251   @Override
 252   public boolean setsSleepCG (ThreadInfo ti, long millis, int nanos){
 253     if (breakSleep){
 254       return setNonBlockingCG( SLEEP, ti);
 255     } else {
 256       return false;
 257     }
 258   }
 259
 260   @Override
 261   public boolean setsSuspendCG (ThreadInfo tiCurrent, ThreadInfo tiSuspended){
 262     return setMaybeBlockingCG( SUSPEND, tiCurrent, tiSuspended);
 263   }
 264
 265   @Override
 266   public boolean setsResumeCG (ThreadInfo tiCurrent, ThreadInfo tiResumed){
 267     return setNonBlockingCG( RESUME, tiCurrent);
 268   }
 269
 270   @Override
 271   public boolean setsJoinCG (ThreadInfo tiCurrent, ThreadInfo tiJoin, long timeout){
 272     return setBlockingCG( JOIN, tiCurrent);
 273   }
 274
 275   @Override
 276   public boolean setsStopCG (ThreadInfo tiCurrent, ThreadInfo tiStopped){
 277     return setMaybeBlockingCG( STOP, tiCurrent, tiStopped);
 278   }
 279
 280   @Override
 281   public boolean setsInterruptCG (ThreadInfo tiCurrent, ThreadInfo tiInterrupted){
 282     if (tiInterrupted.isWaiting()){
 283       return setNonBlockingCG( INTERRUPT, tiCurrent);
 284     } else {
 285       return false;
 286     }
 287   }
 288
 289
 290   //--- sun.misc.Unsafe
 291   @Override
 292   public boolean setsParkCG (ThreadInfo ti, boolean isAbsTime, long timeout){
 293     return setBlockingCG( PARK, ti);
 294   }
 295
 296   @Override
 297   public boolean setsUnparkCG (ThreadInfo tiCurrent, ThreadInfo tiUnparked){
 298     // if the unparked thread is not blocked there is no point
 299     if (tiUnparked.isBlocked()){
 300       return setNonBlockingCG( UNPARK, tiCurrent);
 301     } else {
 302       return false;
 303     }
 304   }
 305
 306
 307   //--- system scheduling events
 308
 309   /**
 310    * this one has to be guaranteed to set a CG
 311    */
 312   @Override
 313   public void setRootCG (){
 314     ThreadInfo[] runnables = vm.getThreadList().getTimeoutRunnables();
 315     ChoiceGenerator<ThreadInfo> cg = new ThreadChoiceFromSet( ROOT, runnables, true);
 316     vm.getSystemState().setMandatoryNextChoiceGenerator( cg, "no ROOT choice generator");
 317   }
 318
 319
 320   //--- gov.nasa.jpf.vm.Verify
 321   @Override
 322   public boolean setsBeginAtomicCG (ThreadInfo ti){
 323     return setNonBlockingCG( BEGIN_ATOMIC, ti);
 324   }
 325
 326   @Override
 327   public boolean setsEndAtomicCG (ThreadInfo ti){
 328     return setNonBlockingCG( END_ATOMIC, ti);
 329   }
 330
 331   //--- ThreadInfo reschedule request
 332   @Override
 333   public boolean setsRescheduleCG (ThreadInfo ti, String reason){
 334     return setNonBlockingCG( reason, ti);
 335   }
 336
 337   //--- FinalizerThread
 338   @Override
 339   public boolean setsPostFinalizeCG (ThreadInfo tiFinalizer){
 340     // the finalizer is already waiting at this point, i.e. it's not runnable anymore
 341     return setBlockingCG( POST_FINALIZE, tiFinalizer);
 342   }
 343
 344
 345 }