Members/kono/jpf-core: src/main/gov/nasa/jpf/vm/AllRunnablesSyncPolicy.java comparison

comparison src/main/gov/nasa/jpf/vm/AllRunnablesSyncPolicy.java @ 0:61d41facf527

initial v8 import (history reset)

author	Peter Mehlitz <Peter.C.Mehlitz@nasa.gov>
date	Fri, 23 Jan 2015 10:14:01 -0800
parents
children	87e9c7544a06

comparison

equal deleted inserted replaced

--1:000000000000
+:61d41facf527
+/*
+* Copyright (C) 2014, United States Government, as represented by the
+* Administrator of the National Aeronautics and Space Administration.
+* All rights reserved.
+*
+* The Java Pathfinder core (jpf-core) platform is licensed under the
+* Apache License, Version 2.0 (the "License"); you may not use this file except
+* in compliance with the License. You may obtain a copy of the License at
+*
+*        http://www.apache.org/licenses/LICENSE-2.0.
+*
+* Unless required by applicable law or agreed to in writing, software
+* distributed under the License is distributed on an "AS IS" BASIS,
+* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+* See the License for the specific language governing permissions and
+* limitations under the License.
+*/
+package gov.nasa.jpf.vm;
+import gov.nasa.jpf.Config;
+import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
+/**
+* a Scheduler implementation base class that allows filtering of runnable threads and
+* implements SyncPolicy without backtracking or empty transitions, i.e. choice sets that
+* include all runnable threads
+*/
+public class AllRunnablesSyncPolicy implements SyncPolicy {
+protected VM vm;
+protected boolean breakSingleChoice;
+protected boolean breakLockRelease;
+protected boolean breakNotify;
+protected boolean breakSleep;
+protected boolean breakYield;
+protected boolean breakPriority;
+public AllRunnablesSyncPolicy (Config config){
+breakSingleChoice = config.getBoolean("cg.break_single_choice", false);
+breakLockRelease = config.getBoolean("cg.break_lock_release", true);
+breakNotify = config.getBoolean("cg.break_notify", true);
+breakSleep = config.getBoolean("cg.break_sleep", true);
+breakYield = config.getBoolean("cg.break_yield", true);
+breakPriority = config.getBoolean("cg.break_priority", true);
+}
+//--- internal methods
+/**
+* this is the main policy method that can be overridden by subclasses, e.g. by filtering
+* out the highest priority runnables, or by ordering according to priority
+*
+* Default behavior is to first try to find runnables within the provided ApplicationContext,
+* and fall back to any runnable if there are none in this context
+*
+* this includes threads that are in operations that can timeout
+*/
+protected ThreadInfo[] getTimeoutRunnables (ApplicationContext appCtx){
+ThreadList tlist = vm.getThreadList();
+if (tlist.hasProcessTimeoutRunnables(appCtx)){
+return tlist.getProcessTimeoutRunnables(appCtx);
+} else {
+return tlist.getTimeoutRunnables();
+}
+}
+protected ChoiceGenerator<ThreadInfo> getRunnableCG (String id, ThreadInfo tiCurrent){
+ThreadInfo[] choices = getTimeoutRunnables(tiCurrent.getApplicationContext());
+if (choices.length == 0){
+return null;
+}
+if ((choices.length == 1) && (choices[0] == tiCurrent) && !tiCurrent.isTimeoutWaiting()){ // no context switch
+if (!breakSingleChoice){
+return null;
+}
+}
+return new ThreadChoiceFromSet( id, choices, true);
+}
+protected boolean setNextChoiceGenerator (ChoiceGenerator<ThreadInfo> cg){
+if (cg != null){
+return vm.getSystemState().setNextChoiceGenerator(cg); // listeners could still remove CGs
+} else {
+return false;
+}
+}
+/**
+* set a runnable CG that is optional if we are in a atomic section
+*/
+protected boolean setNonBlockingCG (String id, ThreadInfo tiCurrent){
+if (!tiCurrent.isFirstStepInsn() || tiCurrent.isEmptyTransitionEnabled()) {
+if (vm.getSystemState().isAtomic()) {
+return false;
+} else {
+return setNextChoiceGenerator(getRunnableCG(id, tiCurrent));
+}
+} else {
+return false;  // no empty transitions
+}
+}
+protected static ChoiceGenerator<ThreadInfo> blockedWithoutChoice =
+new ThreadChoiceFromSet("BLOCKED_NO_CHOICE", new ThreadInfo[0], true);
+/**
+* set a runnable CG that would break a atomic section because it requires
+* a context switch
+*/
+protected boolean setBlockingCG (String id, ThreadInfo tiCurrent){
+if (!tiCurrent.isFirstStepInsn() || tiCurrent.isEmptyTransitionEnabled()) {
+if (vm.getSystemState().isAtomic()) {
+vm.getSystemState().setBlockedInAtomicSection();
+}
+ChoiceGenerator<ThreadInfo> cg = getRunnableCG(id, tiCurrent);
+if (cg == null){ // make sure we don't mask a deadlock
+if (vm.getThreadList().hasLiveThreads()){
+cg = blockedWithoutChoice;
+}
+}
+return setNextChoiceGenerator(cg);
+} else {
+return false;  // no empty transitions
+}
+}
+/**
+* set a runnable CG that only breaks a atomic section if the blocking thread
+* is the currently executing one
+*/
+protected boolean setMaybeBlockingCG (String id, ThreadInfo tiCurrent, ThreadInfo tiBlock){
+if (tiCurrent == tiBlock){
+return setBlockingCG( id, tiCurrent);
+} else {
+return setNonBlockingCG( id, tiCurrent);
+}
+}
+//--- SyncPolicy interface
+//--- initialization
+@Override
+public void initializeSyncPolicy (VM vm, ApplicationContext appCtx){
+this.vm  = vm;
+}
+@Override
+public void initializeThreadSync (ThreadInfo tiCurrent, ThreadInfo tiNew){
+}
+//--- locks
+@Override
+public boolean setsBlockedThreadCG (ThreadInfo ti, ElementInfo ei){
+return setBlockingCG( BLOCK, ti);
+}
+@Override
+public boolean setsLockAcquisitionCG (ThreadInfo ti, ElementInfo ei){
+return setNonBlockingCG( LOCK, ti);
+}
+@Override
+public boolean setsLockReleaseCG (ThreadInfo ti, ElementInfo ei, boolean didUnblock){
+if (breakLockRelease){
+if (didUnblock){
+return setNonBlockingCG( RELEASE, ti);
+}
+}
+return false;
+}
+//--- thread termination
+@Override
+public boolean setsTerminationCG (ThreadInfo ti){
+return setBlockingCG( TERMINATE, ti);
+}
+//--- java.lang.Object APIs
+@Override
+public boolean setsWaitCG (ThreadInfo ti, long timeout){
+return setBlockingCG( WAIT, ti);
+}
+@Override
+public boolean setsNotifyCG (ThreadInfo ti, boolean didNotify){
+if (breakNotify){
+if (didNotify){
+return setNonBlockingCG( NOTIFY, ti);
+}
+}
+return false;
+}
+@Override
+public boolean setsNotifyAllCG (ThreadInfo ti, boolean didNotify){
+if (breakNotify){
+if (didNotify){
+return setNonBlockingCG( NOTIFYALL, ti);
+}
+}
+return false;
+}
+//--- the java.lang.Thread APIs
+@Override
+public boolean setsStartCG (ThreadInfo tiCurrent, ThreadInfo tiStarted){
+return setNonBlockingCG( START, tiCurrent);
+}
+@Override
+public boolean setsYieldCG (ThreadInfo ti){
+if (breakYield){
+return setNonBlockingCG( YIELD, ti);
+} else {
+return false;
+}
+}
+@Override
+public boolean setsPriorityCG (ThreadInfo ti){
+if (breakPriority){
+return setNonBlockingCG( PRIORITY, ti);
+} else {
+return false;
+}
+}
+@Override
+public boolean setsSleepCG (ThreadInfo ti, long millis, int nanos){
+if (breakSleep){
+return setNonBlockingCG( SLEEP, ti);
+} else {
+return false;
+}
+}
+@Override
+public boolean setsSuspendCG (ThreadInfo tiCurrent, ThreadInfo tiSuspended){
+return setMaybeBlockingCG( SUSPEND, tiCurrent, tiSuspended);
+}
+@Override
+public boolean setsResumeCG (ThreadInfo tiCurrent, ThreadInfo tiResumed){
+return setNonBlockingCG( RESUME, tiCurrent);
+}
+@Override
+public boolean setsJoinCG (ThreadInfo tiCurrent, ThreadInfo tiJoin, long timeout){
+return setBlockingCG( JOIN, tiCurrent);
+}
+@Override
+public boolean setsStopCG (ThreadInfo tiCurrent, ThreadInfo tiStopped){
+return setMaybeBlockingCG( STOP, tiCurrent, tiStopped);
+}
+@Override
+public boolean setsInterruptCG (ThreadInfo tiCurrent, ThreadInfo tiInterrupted){
+if (tiInterrupted.isWaiting()){
+return setNonBlockingCG( INTERRUPT, tiCurrent);
+} else {
+return false;
+}
+}
+//--- sun.misc.Unsafe
+@Override
+public boolean setsParkCG (ThreadInfo ti, boolean isAbsTime, long timeout){
+return setBlockingCG( PARK, ti);
+}
+@Override
+public boolean setsUnparkCG (ThreadInfo tiCurrent, ThreadInfo tiUnparked){
+// if the unparked thread is not blocked there is no point
+if (tiUnparked.isBlocked()){
+return setNonBlockingCG( UNPARK, tiCurrent);
+} else {
+return false;
+}
+}
+//--- system scheduling events
+/**
+* this one has to be guaranteed to set a CG
+*/
+@Override
+public void setRootCG (){
+ThreadInfo[] runnables = vm.getThreadList().getTimeoutRunnables();
+ChoiceGenerator<ThreadInfo> cg = new ThreadChoiceFromSet( ROOT, runnables, true);
+vm.getSystemState().setMandatoryNextChoiceGenerator( cg, "no ROOT choice generator");
+}
+//--- gov.nasa.jpf.vm.Verify
+@Override
+public boolean setsBeginAtomicCG (ThreadInfo ti){
+return setNonBlockingCG( BEGIN_ATOMIC, ti);
+}
+@Override
+public boolean setsEndAtomicCG (ThreadInfo ti){
+return setNonBlockingCG( END_ATOMIC, ti);
+}
+//--- ThreadInfo reschedule request
+@Override
+public boolean setsRescheduleCG (ThreadInfo ti, String reason){
+return setNonBlockingCG( reason, ti);
+}
+//--- FinalizerThread
+@Override
+public boolean setsPostFinalizeCG (ThreadInfo tiFinalizer){
+// the finalizer is already waiting at this point, i.e. it's not runnable anymore
+return setBlockingCG( POST_FINALIZE, tiFinalizer);
+}
+}

Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/vm/AllRunnablesSyncPolicy.java @ 0:61d41facf527