gov.nasa.jpf.vm

Class ContextBoundingSchedulerFactory

java.lang.Object

gov.nasa.jpf.vm.DefaultSchedulerFactory

gov.nasa.jpf.vm.ContextBoundingSchedulerFactory

All Implemented Interfaces:

SchedulerFactory

public class ContextBoundingSchedulerFactory
extends DefaultSchedulerFactory

SchedulerFactory that limits the search by imposing a maximum number of thread preemptions (i.e., preempting context switches) that can occur per execution path. This factory internally creates ContextBoundingThreadChoiceFromSet choice generators.

Configuration parameters:

vm.scheduler_factory.class=gov.nasa.jpf.vm.ContextBoundingSchedulerFactory
setting scheduler factory class to this class

cg.max_number_of_preemptions=N
where N is the number of allowed preemptions per execution path

The idea of context bounding is based on the PLDI 2007 paper
"Iterative Context Bounding for Systematic Testing of Multithreaded Programs"
by Madanlal Musuvathi and Shaz Qadeer
This factory does not implement the paper's iterative context-bounding algorithm, i.e., the specific order of states that get explored. (For that, one needs to use a search strategy.) This factory simply provides a limit on the number of preemptions that are allowed and can be used with various search strategies, including DFS, BFS, heuristics, etc.

Author:

Igor Andjelkovic (igor.andjelkovic@gmail.com), Mirko Stojmenovic (mirko.stojmenovic@gmail.com), Steven Lauterburg (slauter2@cs.uiuc.edu)

Field Summary

Fields inherited from class gov.nasa.jpf.vm.DefaultSchedulerFactory

ss, vm

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

BEGIN_ATOMIC, END_ATOMIC, MONITOR_ENTER, MONITOR_EXIT, NOTIFY, NOTIFY_ALL, PARK, SHARED_ARRAY_ACCESS, SHARED_FIELD_ACCESS, SHARED_OBJECT_EXPOSURE, SYNC_METHOD_ENTER, SYNC_METHOD_EXIT, THREAD_INTERRUPT, THREAD_RESUME, THREAD_SLEEP, THREAD_START, THREAD_STOP, THREAD_SUSPEND, THREAD_TERMINATE, THREAD_YIELD, UNPARK, WAIT

Constructor Summary

Constructors

Constructor and Description
ContextBoundingSchedulerFactory(Config config, VM vm, SystemState ss)

Method Summary

Methods

Modifier and Type	Method and Description
ChoiceGenerator<ThreadInfo>	createMonitorEnterCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createNotifyCG(ElementInfo ei, ThreadInfo ti)
ChoiceGenerator<ThreadInfo>	createThreadTerminateCG(ThreadInfo terminateThread)
ChoiceGenerator<ThreadInfo>	createWaitCG(ElementInfo ei, ThreadInfo ti, long timeOut)
protected ThreadInfo[]	filter(ThreadInfo[] list) post process a list of choices.
protected ChoiceGenerator<ThreadInfo>	getRunnableCG(String id, ThreadInfo ti)

Methods inherited from class gov.nasa.jpf.vm.DefaultSchedulerFactory

createBeginAtomicCG, createEndAtomicCG, createEnterCG, createExitCG, createInterruptCG, createMonitorExitCG, createNotifyAllCG, createParkCG, createSharedArrayAccessCG, createSharedFieldAccessCG, createSharedObjectExposureCG, createSyncMethodEnterCG, createSyncMethodExitCG, createThreadResumeCG, createThreadSleepCG, createThreadStartCG, createThreadStopCG, createThreadSuspendCG, createThreadYieldCG, createUnparkCG, getRunnables, getRunnablesIfChoices, getRunnablesWith, getRunnablesWithout, getSyncCG

Methods inherited from class java.lang.Object

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

Constructor Detail

ContextBoundingSchedulerFactory

public ContextBoundingSchedulerFactory(Config config,
                               VM vm,
                               SystemState ss)

Method Detail

filter

protected ThreadInfo[] filter(ThreadInfo[] list)

Description copied from class: DefaultSchedulerFactory

post process a list of choices. This is our primary interface towards subclasses (together with overriding the relevant ainsn APIs

Overrides:

filter in class DefaultSchedulerFactory

getRunnableCG

protected ChoiceGenerator<ThreadInfo> getRunnableCG(String id,
                                        ThreadInfo ti)

Overrides:

getRunnableCG in class DefaultSchedulerFactory

createMonitorEnterCG

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

Specified by:

createMonitorEnterCG in interface SchedulerFactory

Overrides:

createMonitorEnterCG in class DefaultSchedulerFactory

createWaitCG

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

Specified by:

createWaitCG in interface SchedulerFactory

Overrides:

createWaitCG in class DefaultSchedulerFactory

createNotifyCG

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

Specified by:

createNotifyCG in interface SchedulerFactory

Overrides:

createNotifyCG in class DefaultSchedulerFactory

createThreadTerminateCG

public ChoiceGenerator<ThreadInfo> createThreadTerminateCG(ThreadInfo terminateThread)

Specified by:

createThreadTerminateCG in interface SchedulerFactory

Overrides:

createThreadTerminateCG in class DefaultSchedulerFactory