gov.nasa.jpf.vm

Interface SchedulerFactory

All Known Implementing Classes:

ContextBoundingSchedulerFactory, DefaultSchedulerFactory, DistributedSchedulerFactory, PrioritySchedulerFactory

public interface SchedulerFactory

interface of factory object that creates all ChoiceGenerators required to implement scheduling strategies

Field Summary

Fields

Modifier and Type	Field and Description
static String	BEGIN_ATOMIC used by Verify.beginAtomic()
static String	END_ATOMIC used by Verify.andAtomic()
static String	MONITOR_ENTER used by MonitorEnter insns
static String	MONITOR_EXIT used by MonitorExit insns
static String	NOTIFY used by Object.notify()
static String	NOTIFY_ALL used by Object.notifyAll()
static String	PARK used by sun.misc.Unsafe.park()
static String	SHARED_ARRAY_ACCESS used from ArrayInstruction (various array element access insns)
static String	SHARED_FIELD_ACCESS used by GetField,PutField,GetStatic,PutStatic insns of shared objects
static String	SHARED_OBJECT_EXPOSURE used by PutField,PutStatic insns if previously unshared objects get stored in shared object fields
static String	SYNC_METHOD_ENTER used by InvokeInstructions of sync methods
static String	SYNC_METHOD_EXIT user by Returns of sync methods
static String	THREAD_INTERRUPT used by Thread.interrupt()
static String	THREAD_RESUME used by Thread.resume()
static String	THREAD_SLEEP used by Thread.sleep()
static String	THREAD_START used by Thread.start()
static String	THREAD_STOP used by Thread.stop()
static String	THREAD_SUSPEND used by Thread.suspend()
static String	THREAD_TERMINATE used by Return from run()
static String	THREAD_YIELD used by Thread.yield()
static String	UNPARK used by sun.misc.Unsafe.unpark()
static String	WAIT used by Object.wait()

Method Summary

Methods

Modifier and Type	Method and Description
ChoiceGenerator<ThreadInfo>	createBeginAtomicCG(ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createEndAtomicCG(ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createInterruptCG(ThreadInfo interruptedThread)
ChoiceGenerator<ThreadInfo>	createMonitorEnterCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createMonitorExitCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createNotifyAllCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createNotifyCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createParkCG(ElementInfo ei, ThreadInfo tiPark, boolean isAbsoluteTime, long timeOut)
ChoiceGenerator<ThreadInfo>	createSharedArrayAccessCG(ElementInfo eiArray, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createSharedFieldAccessCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createSharedObjectExposureCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createSyncMethodEnterCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createSyncMethodExitCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createThreadResumeCG(ThreadInfo resumedThread)
ChoiceGenerator<ThreadInfo>	createThreadSleepCG(ThreadInfo sleepThread, long millis, int nanos)
ChoiceGenerator<ThreadInfo>	createThreadStartCG(ThreadInfo newThread)
ChoiceGenerator<ThreadInfo>	createThreadStopCG(ThreadInfo stoppedThread)
ChoiceGenerator<ThreadInfo>	createThreadSuspendCG(ThreadInfo suspendedThread)
ChoiceGenerator<ThreadInfo>	createThreadTerminateCG(ThreadInfo terminatedThread)
ChoiceGenerator<ThreadInfo>	createThreadYieldCG(ThreadInfo yieldThread)
ChoiceGenerator<ThreadInfo>	createUnparkCG(ThreadInfo tiUnparked)
ChoiceGenerator<ThreadInfo>	createWaitCG(ElementInfo ei, ThreadInfo ti, long timeOut)

Field Detail

SYNC_METHOD_ENTER

static final String SYNC_METHOD_ENTER

used by InvokeInstructions of sync methods

See Also:

Constant Field Values

SYNC_METHOD_EXIT

static final String SYNC_METHOD_EXIT

user by Returns of sync methods

See Also:

Constant Field Values

MONITOR_ENTER

static final String MONITOR_ENTER

used by MonitorEnter insns

See Also:

Constant Field Values

MONITOR_EXIT

static final String MONITOR_EXIT

used by MonitorExit insns

See Also:

Constant Field Values

WAIT

static final String WAIT

used by Object.wait()

See Also:

Constant Field Values

NOTIFY

static final String NOTIFY

used by Object.notify()

See Also:

Constant Field Values

NOTIFY_ALL

static final String NOTIFY_ALL

used by Object.notifyAll()

See Also:

Constant Field Values

PARK

static final String PARK

used by sun.misc.Unsafe.park()

See Also:

Constant Field Values

UNPARK

static final String UNPARK

used by sun.misc.Unsafe.unpark()

See Also:

Constant Field Values

SHARED_FIELD_ACCESS

static final String SHARED_FIELD_ACCESS

used by GetField,PutField,GetStatic,PutStatic insns of shared objects

See Also:

Constant Field Values

SHARED_ARRAY_ACCESS

static final String SHARED_ARRAY_ACCESS

used from ArrayInstruction (various array element access insns)

See Also:

Constant Field Values

SHARED_OBJECT_EXPOSURE

static final String SHARED_OBJECT_EXPOSURE

used by PutField,PutStatic insns if previously unshared objects get stored in shared object fields

See Also:

Constant Field Values

THREAD_START

static final String THREAD_START

used by Thread.start()

See Also:

Constant Field Values

THREAD_YIELD

static final String THREAD_YIELD

used by Thread.yield()

See Also:

Constant Field Values

THREAD_SLEEP

static final String THREAD_SLEEP

used by Thread.sleep()

See Also:

Constant Field Values

THREAD_INTERRUPT

static final String THREAD_INTERRUPT

used by Thread.interrupt()

See Also:

Constant Field Values

THREAD_TERMINATE

static final String THREAD_TERMINATE

used by Return from run()

See Also:

Constant Field Values

THREAD_SUSPEND

static final String THREAD_SUSPEND

used by Thread.suspend()

See Also:

Constant Field Values

THREAD_RESUME

static final String THREAD_RESUME

used by Thread.resume()

See Also:

Constant Field Values

THREAD_STOP

static final String THREAD_STOP

used by Thread.stop()

See Also:

Constant Field Values

BEGIN_ATOMIC

static final String BEGIN_ATOMIC

used by Verify.beginAtomic()

See Also:

Constant Field Values

END_ATOMIC

static final String END_ATOMIC

used by Verify.andAtomic()

See Also:

Constant Field Values

Method Detail

createSyncMethodEnterCG

ChoiceGenerator<ThreadInfo> createSyncMethodEnterCG(ElementInfo ei,
                                                  ThreadInfo ti)

createSyncMethodExitCG

ChoiceGenerator<ThreadInfo> createSyncMethodExitCG(ElementInfo ei,
                                                 ThreadInfo ti)

createMonitorEnterCG

ChoiceGenerator<ThreadInfo> createMonitorEnterCG(ElementInfo ei,
                                               ThreadInfo ti)

createMonitorExitCG

ChoiceGenerator<ThreadInfo> createMonitorExitCG(ElementInfo ei,
                                              ThreadInfo ti)

createWaitCG

ChoiceGenerator<ThreadInfo> createWaitCG(ElementInfo ei,
                                       ThreadInfo ti,
                                       long timeOut)

createNotifyCG

ChoiceGenerator<ThreadInfo> createNotifyCG(ElementInfo ei,
                                         ThreadInfo ti)

createNotifyAllCG

ChoiceGenerator<ThreadInfo> createNotifyAllCG(ElementInfo ei,
                                            ThreadInfo ti)

createParkCG

ChoiceGenerator<ThreadInfo> createParkCG(ElementInfo ei,
                                       ThreadInfo tiPark,
                                       boolean isAbsoluteTime,
                                       long timeOut)

createUnparkCG

ChoiceGenerator<ThreadInfo> createUnparkCG(ThreadInfo tiUnparked)

createSharedFieldAccessCG

ChoiceGenerator<ThreadInfo> createSharedFieldAccessCG(ElementInfo ei,
                                                    ThreadInfo ti)

createSharedArrayAccessCG

ChoiceGenerator<ThreadInfo> createSharedArrayAccessCG(ElementInfo eiArray,
                                                    ThreadInfo ti)

createSharedObjectExposureCG

ChoiceGenerator<ThreadInfo> createSharedObjectExposureCG(ElementInfo ei,
                                                       ThreadInfo ti)

createThreadStartCG

ChoiceGenerator<ThreadInfo> createThreadStartCG(ThreadInfo newThread)

createThreadYieldCG

ChoiceGenerator<ThreadInfo> createThreadYieldCG(ThreadInfo yieldThread)

createThreadSleepCG

ChoiceGenerator<ThreadInfo> createThreadSleepCG(ThreadInfo sleepThread,
                                              long millis,
                                              int nanos)

createInterruptCG

ChoiceGenerator<ThreadInfo> createInterruptCG(ThreadInfo interruptedThread)

createThreadTerminateCG

ChoiceGenerator<ThreadInfo> createThreadTerminateCG(ThreadInfo terminatedThread)

createThreadSuspendCG

ChoiceGenerator<ThreadInfo> createThreadSuspendCG(ThreadInfo suspendedThread)

createThreadResumeCG

ChoiceGenerator<ThreadInfo> createThreadResumeCG(ThreadInfo resumedThread)

createThreadStopCG

ChoiceGenerator<ThreadInfo> createThreadStopCG(ThreadInfo stoppedThread)

createBeginAtomicCG

ChoiceGenerator<ThreadInfo> createBeginAtomicCG(ThreadInfo ti)

createEndAtomicCG

ChoiceGenerator<ThreadInfo> createEndAtomicCG(ThreadInfo ti)