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.
19 package gov.nasa.jpf.vm;
21 import gov.nasa.jpf.Config;
22 import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
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
29 public class AllRunnablesSyncPolicy implements SyncPolicy {
32 protected boolean breakSingleChoice;
33 protected boolean breakLockRelease;
34 protected boolean breakNotify;
35 protected boolean breakSleep;
36 protected boolean breakYield;
37 protected boolean breakPriority;
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);
49 //--- internal methods
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
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
58 * this includes threads that are in operations that can timeout
60 protected ThreadInfo[] getTimeoutRunnables (ApplicationContext appCtx){
61 ThreadList tlist = vm.getThreadList();
63 if (tlist.hasProcessTimeoutRunnables(appCtx)){
64 return tlist.getProcessTimeoutRunnables(appCtx);
66 return tlist.getTimeoutRunnables();
71 protected ChoiceGenerator<ThreadInfo> getRunnableCG (String id, ThreadInfo tiCurrent){
72 ApplicationContext appCtx = tiCurrent.getApplicationContext();
73 ThreadInfo[] choices = getTimeoutRunnables(appCtx);
75 if (choices.length == 0){
79 if ((choices.length == 1) && (choices[0] == tiCurrent) && !tiCurrent.isTimeoutWaiting()){ // no context switch
80 if (!breakSingleChoice){
85 ChoiceGenerator<ThreadInfo> cg = new ThreadChoiceFromSet( id, choices, true);
87 if(!vm.getThreadList().hasProcessTimeoutRunnables(appCtx)) {
88 GlobalSchedulingPoint.setGlobal(cg);
94 protected boolean setNextChoiceGenerator (ChoiceGenerator<ThreadInfo> cg){
96 return vm.getSystemState().setNextChoiceGenerator(cg); // listeners could still remove CGs
103 * set a runnable CG that is optional if we are in a atomic section
105 protected boolean setNonBlockingCG (String id, ThreadInfo tiCurrent){
106 if (!tiCurrent.isFirstStepInsn() || tiCurrent.isEmptyTransitionEnabled()) {
107 if (vm.getSystemState().isAtomic()) {
110 return setNextChoiceGenerator(getRunnableCG(id, tiCurrent));
114 return false; // no empty transitions
118 protected static ChoiceGenerator<ThreadInfo> blockedWithoutChoice =
119 new ThreadChoiceFromSet("BLOCKED_NO_CHOICE", new ThreadInfo[0], true);
122 * set a runnable CG that would break a atomic section because it requires
125 protected boolean setBlockingCG (String id, ThreadInfo tiCurrent){
126 if (!tiCurrent.isFirstStepInsn() || tiCurrent.isEmptyTransitionEnabled()) {
127 if (vm.getSystemState().isAtomic()) {
128 vm.getSystemState().setBlockedInAtomicSection();
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;
138 return setNextChoiceGenerator(cg);
141 return false; // no empty transitions
146 * set a runnable CG that only breaks a atomic section if the blocking thread
147 * is the currently executing one
149 protected boolean setMaybeBlockingCG (String id, ThreadInfo tiCurrent, ThreadInfo tiBlock){
150 if (tiCurrent == tiBlock){
151 return setBlockingCG( id, tiCurrent);
153 return setNonBlockingCG( id, tiCurrent);
158 //--- SyncPolicy interface
162 public void initializeSyncPolicy (VM vm, ApplicationContext appCtx){
167 public void initializeThreadSync (ThreadInfo tiCurrent, ThreadInfo tiNew){
172 public boolean setsBlockedThreadCG (ThreadInfo ti, ElementInfo ei){
173 return setBlockingCG( BLOCK, ti);
177 public boolean setsLockAcquisitionCG (ThreadInfo ti, ElementInfo ei){
178 return setNonBlockingCG( LOCK, ti);
182 public boolean setsLockReleaseCG (ThreadInfo ti, ElementInfo ei, boolean didUnblock){
183 if (breakLockRelease){
185 return setNonBlockingCG( RELEASE, ti);
192 //--- thread termination
194 public boolean setsTerminationCG (ThreadInfo ti){
195 return setBlockingCG( TERMINATE, ti);
198 //--- java.lang.Object APIs
200 public boolean setsWaitCG (ThreadInfo ti, long timeout){
201 return setBlockingCG( WAIT, ti);
205 public boolean setsNotifyCG (ThreadInfo ti, boolean didNotify){
208 return setNonBlockingCG( NOTIFY, ti);
216 public boolean setsNotifyAllCG (ThreadInfo ti, boolean didNotify){
219 return setNonBlockingCG( NOTIFYALL, ti);
227 //--- the java.lang.Thread APIs
229 public boolean setsStartCG (ThreadInfo tiCurrent, ThreadInfo tiStarted){
230 return setNonBlockingCG( START, tiCurrent);
234 public boolean setsYieldCG (ThreadInfo ti){
236 return setNonBlockingCG( YIELD, ti);
243 public boolean setsPriorityCG (ThreadInfo ti){
245 return setNonBlockingCG( PRIORITY, ti);
252 public boolean setsSleepCG (ThreadInfo ti, long millis, int nanos){
254 return setNonBlockingCG( SLEEP, ti);
261 public boolean setsSuspendCG (ThreadInfo tiCurrent, ThreadInfo tiSuspended){
262 return setMaybeBlockingCG( SUSPEND, tiCurrent, tiSuspended);
266 public boolean setsResumeCG (ThreadInfo tiCurrent, ThreadInfo tiResumed){
267 return setNonBlockingCG( RESUME, tiCurrent);
271 public boolean setsJoinCG (ThreadInfo tiCurrent, ThreadInfo tiJoin, long timeout){
272 return setBlockingCG( JOIN, tiCurrent);
276 public boolean setsStopCG (ThreadInfo tiCurrent, ThreadInfo tiStopped){
277 return setMaybeBlockingCG( STOP, tiCurrent, tiStopped);
281 public boolean setsInterruptCG (ThreadInfo tiCurrent, ThreadInfo tiInterrupted){
282 if (tiInterrupted.isWaiting()){
283 return setNonBlockingCG( INTERRUPT, tiCurrent);
290 //--- sun.misc.Unsafe
292 public boolean setsParkCG (ThreadInfo ti, boolean isAbsTime, long timeout){
293 return setBlockingCG( PARK, ti);
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);
307 //--- system scheduling events
310 * this one has to be guaranteed to set a CG
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");
320 //--- gov.nasa.jpf.vm.Verify
322 public boolean setsBeginAtomicCG (ThreadInfo ti){
323 return setNonBlockingCG( BEGIN_ATOMIC, ti);
327 public boolean setsEndAtomicCG (ThreadInfo ti){
328 return setNonBlockingCG( END_ATOMIC, ti);
331 //--- ThreadInfo reschedule request
333 public boolean setsRescheduleCG (ThreadInfo ti, String reason){
334 return setNonBlockingCG( reason, ti);
337 //--- FinalizerThread
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);