gov.nasa.jpf.vm

Class AllRunnablesSyncPolicy

java.lang.Object

gov.nasa.jpf.vm.AllRunnablesSyncPolicy

All Implemented Interfaces:

SyncPolicy

Direct Known Subclasses:

PriorityRunnablesSyncPolicy

public class AllRunnablesSyncPolicy
extends java.lang.Object
implements SyncPolicy

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

Field Summary

Fields

Modifier and Type	Field and Description
protected static ChoiceGenerator<ThreadInfo>	blockedWithoutChoice
protected boolean	breakLockRelease
protected boolean	breakNotify
protected boolean	breakPriority
protected boolean	breakSingleChoice
protected boolean	breakSleep
protected boolean	breakYield
protected VM	vm

Fields inherited from interface gov.nasa.jpf.vm.SyncPolicy

BEGIN_ATOMIC, BLOCK, END_ATOMIC, INTERRUPT, JOIN, LOCK, NOTIFY, NOTIFYALL, PARK, POST_FINALIZE, PRIORITY, RELEASE, RESCHEDULE, RESUME, ROOT, SLEEP, START, STOP, SUSPEND, TERMINATE, UNPARK, WAIT, YIELD

Constructor Summary

Constructors

Constructor and Description
AllRunnablesSyncPolicy(Config config)

Method Summary

Modifier and Type	Method and Description
protected ChoiceGenerator<ThreadInfo>	getRunnableCG(java.lang.String id, ThreadInfo tiCurrent)
protected ThreadInfo[]	getTimeoutRunnables(ApplicationContext appCtx) this is the main policy method that can be overridden by subclasses, e.g.
void	initializeSyncPolicy(VM vm, ApplicationContext appCtx) called once per application, after the VM is fully initialized
void	initializeThreadSync(ThreadInfo tiCurrent, ThreadInfo tiNew) called during ThreadInfo initialization, before Thread.start()
protected boolean	setBlockingCG(java.lang.String id, ThreadInfo tiCurrent) set a runnable CG that would break a atomic section because it requires a context switch
protected boolean	setMaybeBlockingCG(java.lang.String id, ThreadInfo tiCurrent, ThreadInfo tiBlock) set a runnable CG that only breaks a atomic section if the blocking thread is the currently executing one
protected boolean	setNextChoiceGenerator(ChoiceGenerator<ThreadInfo> cg)
protected boolean	setNonBlockingCG(java.lang.String id, ThreadInfo tiCurrent) set a runnable CG that is optional if we are in a atomic section
void	setRootCG() this one has to be guaranteed to set a CG
boolean	setsBeginAtomicCG(ThreadInfo ti)
boolean	setsBlockedThreadCG(ThreadInfo ti, ElementInfo ei)
boolean	setsEndAtomicCG(ThreadInfo ti)
boolean	setsInterruptCG(ThreadInfo tiCurrent, ThreadInfo tiInterrupted)
boolean	setsJoinCG(ThreadInfo tiCurrent, ThreadInfo tiJoin, long timeout)
boolean	setsLockAcquisitionCG(ThreadInfo ti, ElementInfo ei)
boolean	setsLockReleaseCG(ThreadInfo ti, ElementInfo ei, boolean didUnblock)
boolean	setsNotifyAllCG(ThreadInfo ti, boolean didNotify)
boolean	setsNotifyCG(ThreadInfo ti, boolean didNotify)
boolean	setsParkCG(ThreadInfo ti, boolean isAbsTime, long timeout)
boolean	setsPostFinalizeCG(ThreadInfo tiFinalizer)
boolean	setsPriorityCG(ThreadInfo ti)
boolean	setsRescheduleCG(ThreadInfo ti, java.lang.String reason)
boolean	setsResumeCG(ThreadInfo tiCurrent, ThreadInfo tiResumed)
boolean	setsSleepCG(ThreadInfo ti, long millis, int nanos)
boolean	setsStartCG(ThreadInfo tiCurrent, ThreadInfo tiStarted)
boolean	setsStopCG(ThreadInfo tiCurrent, ThreadInfo tiStopped)
boolean	setsSuspendCG(ThreadInfo tiCurrent, ThreadInfo tiSuspended)
boolean	setsTerminationCG(ThreadInfo ti)
boolean	setsUnparkCG(ThreadInfo tiCurrent, ThreadInfo tiUnparked)
boolean	setsWaitCG(ThreadInfo ti, long timeout)
boolean	setsYieldCG(ThreadInfo ti)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

vm

protected VM vm

breakSingleChoice

protected boolean breakSingleChoice

breakLockRelease

protected boolean breakLockRelease

breakNotify

protected boolean breakNotify

breakSleep

protected boolean breakSleep

breakYield

protected boolean breakYield

breakPriority

protected boolean breakPriority

blockedWithoutChoice

protected static ChoiceGenerator<ThreadInfo> blockedWithoutChoice

Constructor Detail

AllRunnablesSyncPolicy

public AllRunnablesSyncPolicy(Config config)

Method Detail

getTimeoutRunnables

protected ThreadInfo[] getTimeoutRunnables(ApplicationContext appCtx)

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

getRunnableCG

protected ChoiceGenerator<ThreadInfo> getRunnableCG(java.lang.String id,
                                                    ThreadInfo tiCurrent)

setNextChoiceGenerator

protected boolean setNextChoiceGenerator(ChoiceGenerator<ThreadInfo> cg)

setNonBlockingCG

protected boolean setNonBlockingCG(java.lang.String id,
                                   ThreadInfo tiCurrent)

set a runnable CG that is optional if we are in a atomic section

setBlockingCG

protected boolean setBlockingCG(java.lang.String id,
                                ThreadInfo tiCurrent)

set a runnable CG that would break a atomic section because it requires a context switch

setMaybeBlockingCG

protected boolean setMaybeBlockingCG(java.lang.String id,
                                     ThreadInfo tiCurrent,
                                     ThreadInfo tiBlock)

set a runnable CG that only breaks a atomic section if the blocking thread is the currently executing one

initializeSyncPolicy

public void initializeSyncPolicy(VM vm,
                                 ApplicationContext appCtx)

Description copied from interface: SyncPolicy

called once per application, after the VM is fully initialized

Specified by:

initializeSyncPolicy in interface SyncPolicy

initializeThreadSync

public void initializeThreadSync(ThreadInfo tiCurrent,
                                 ThreadInfo tiNew)

Description copied from interface: SyncPolicy

called during ThreadInfo initialization, before Thread.start()

Specified by:

initializeThreadSync in interface SyncPolicy

setsBlockedThreadCG

public boolean setsBlockedThreadCG(ThreadInfo ti,
                                   ElementInfo ei)

Specified by:

setsBlockedThreadCG in interface SyncPolicy

setsLockAcquisitionCG

public boolean setsLockAcquisitionCG(ThreadInfo ti,
                                     ElementInfo ei)

Specified by:

setsLockAcquisitionCG in interface SyncPolicy

setsLockReleaseCG

public boolean setsLockReleaseCG(ThreadInfo ti,
                                 ElementInfo ei,
                                 boolean didUnblock)

Specified by:

setsLockReleaseCG in interface SyncPolicy

setsTerminationCG

public boolean setsTerminationCG(ThreadInfo ti)

Specified by:

setsTerminationCG in interface SyncPolicy

setsWaitCG

public boolean setsWaitCG(ThreadInfo ti,
                          long timeout)

Specified by:

setsWaitCG in interface SyncPolicy

setsNotifyCG

public boolean setsNotifyCG(ThreadInfo ti,
                            boolean didNotify)

Specified by:

setsNotifyCG in interface SyncPolicy

setsNotifyAllCG

public boolean setsNotifyAllCG(ThreadInfo ti,
                               boolean didNotify)

Specified by:

setsNotifyAllCG in interface SyncPolicy

setsStartCG

public boolean setsStartCG(ThreadInfo tiCurrent,
                           ThreadInfo tiStarted)

Specified by:

setsStartCG in interface SyncPolicy

setsYieldCG

public boolean setsYieldCG(ThreadInfo ti)

Specified by:

setsYieldCG in interface SyncPolicy

setsPriorityCG

public boolean setsPriorityCG(ThreadInfo ti)

Specified by:

setsPriorityCG in interface SyncPolicy

setsSleepCG

public boolean setsSleepCG(ThreadInfo ti,
                           long millis,
                           int nanos)

Specified by:

setsSleepCG in interface SyncPolicy

setsSuspendCG

public boolean setsSuspendCG(ThreadInfo tiCurrent,
                             ThreadInfo tiSuspended)

Specified by:

setsSuspendCG in interface SyncPolicy

setsResumeCG

public boolean setsResumeCG(ThreadInfo tiCurrent,
                            ThreadInfo tiResumed)

Specified by:

setsResumeCG in interface SyncPolicy

setsJoinCG

public boolean setsJoinCG(ThreadInfo tiCurrent,
                          ThreadInfo tiJoin,
                          long timeout)

Specified by:

setsJoinCG in interface SyncPolicy

setsStopCG

public boolean setsStopCG(ThreadInfo tiCurrent,
                          ThreadInfo tiStopped)

Specified by:

setsStopCG in interface SyncPolicy

setsInterruptCG

public boolean setsInterruptCG(ThreadInfo tiCurrent,
                               ThreadInfo tiInterrupted)

Specified by:

setsInterruptCG in interface SyncPolicy

setsParkCG

public boolean setsParkCG(ThreadInfo ti,
                          boolean isAbsTime,
                          long timeout)

Specified by:

setsParkCG in interface SyncPolicy

setsUnparkCG

public boolean setsUnparkCG(ThreadInfo tiCurrent,
                            ThreadInfo tiUnparked)

Specified by:

setsUnparkCG in interface SyncPolicy

setRootCG

public void setRootCG()

this one has to be guaranteed to set a CG

Specified by:

setRootCG in interface SyncPolicy

setsBeginAtomicCG

public boolean setsBeginAtomicCG(ThreadInfo ti)

Specified by:

setsBeginAtomicCG in interface SyncPolicy

setsEndAtomicCG

public boolean setsEndAtomicCG(ThreadInfo ti)

Specified by:

setsEndAtomicCG in interface SyncPolicy

setsRescheduleCG

public boolean setsRescheduleCG(ThreadInfo ti,
                                java.lang.String reason)

Specified by:

setsRescheduleCG in interface SyncPolicy

setsPostFinalizeCG

public boolean setsPostFinalizeCG(ThreadInfo tiFinalizer)

Specified by:

setsPostFinalizeCG in interface SyncPolicy