gov.nasa.jpf.vm

Class PathSharednessPolicy

java.lang.Object

gov.nasa.jpf.vm.GenericSharednessPolicy

gov.nasa.jpf.vm.PathSharednessPolicy

All Implemented Interfaces:

Attributor, SharednessPolicy

public class PathSharednessPolicy
extends GenericSharednessPolicy

a SharednessPolicy implementation that only computes and keeps sharedness along the same path, i.e. not search global. This is the policy that should be used to create traces that can be replayed. This policy uses PersistentTids, i.e. it does not modify existing ThreadInfoSet instances but replaces upon add/remove with new ones. This ensures that ThreadInfoSets are path local, but it also means that operations that add/remove ThreadInfos have to be aware of the associated ElementInfo cloning and don't keep/use references to old ElementInfos. The upside is that sharedness should be the same along any given path, regardless of which paths were executed before. The downside is that all callers of ThreadInfoSet updates have to be aware of that the ElementInfo might change. Note that without additional transition breaks this can miss races due to non-overlapping thread execution along all paths. Most real world systems have enough scheduling points (sync, field access within loops etc.) to avoid this, but short living threads that only have single field access interaction points can run into this effect: T1 creates O, starts T2, accesses O and terminates before T2 runs. When T2 runs, it only sees access to O from an already terminated thread and therefore treats this as a clean handover. Even if T2 would break at its O access, there is no CG that would bring T1 back into a state between creation and access of O, hence races caused by the O access of T1 are missed (see .test.mc.threads.MissedPathTest). Two additional scheduling points help to prevent this case: thread start CGs and object exposure CGs (/after/ assignment in reference field PUTs where the owning object is shared, but the referenced object isn't yet). Both are conservative by nature, i.e. might introduce superfluous states for the sake of not missing paths to race points. Both can be controlled by configuration options ('cg.threads.break_start' and 'vm.por.break_on_exposure'). Note also that shared-ness is not the same along all paths, because our goal is just to find potential data races. As long as JPF explores /one/ path that leads into a race we are fine - we don't care how many paths don't detect a race.

Field Summary

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

alwaysBreakOnFields, alwaysBreakOnTypes, breakOnExposure, lockThreshold, logger, neverBreakInMethods, neverBreakOnFields, neverBreakOnTypes, skipConstructedFinals, skipFinals, skipInits, skipStaticFinals, useSyncDetection, vm

Constructor Summary

Constructors

Constructor and Description
PathSharednessPolicy(Config config)

Method Summary

Modifier and Type	Method and Description
protected boolean	checkOtherRunnables(ThreadInfo ti)
protected FieldLockInfo	createFieldLockInfo(ThreadInfo ti, ElementInfo ei, FieldInfo fi) static attribute filters that determine if the check..Access() and check..Exposure() methods should be called.
void	initializeClassSharedness(ThreadInfo allocThread, StaticElementInfo ei) initializeSharednessPolicy class specific sharedness data
void	initializeObjectSharedness(ThreadInfo allocThread, DynamicElementInfo ei) initializeSharednessPolicy object specific sharedness data

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

canHaveSharedArrayCG, canHaveSharedClassCG, canHaveSharednessCG, canHaveSharedObjectCG, cleanupThreadTermination, getRunnableCG, getRunnables, initializeSharednessPolicy, isFirstExposure, isInNeverBreakMethod, isRelevantArrayAccess, isRelevantStaticFieldAccess, setAttributes, setFieldAttributes, setNextChoiceGenerator, setsExposureCG, setsSharedArrayCG, setsSharedClassCG, setsSharedClassExposureCG, setsSharedObjectCG, setsSharedObjectExposureCG, setTypeAttributes, updateArraySharedness, updateClassSharedness, updateFieldLockInfo, updateObjectSharedness, updateSharedness

Methods inherited from class java.lang.Object

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

Constructor Detail

PathSharednessPolicy

public PathSharednessPolicy(Config config)

Method Detail

initializeObjectSharedness

public void initializeObjectSharedness(ThreadInfo allocThread,
                                       DynamicElementInfo ei)

Description copied from interface: SharednessPolicy

initializeSharednessPolicy object specific sharedness data

initializeClassSharedness

public void initializeClassSharedness(ThreadInfo allocThread,
                                      StaticElementInfo ei)

Description copied from interface: SharednessPolicy

initializeSharednessPolicy class specific sharedness data

createFieldLockInfo

protected FieldLockInfo createFieldLockInfo(ThreadInfo ti,
                                            ElementInfo ei,
                                            FieldInfo fi)

Description copied from class: GenericSharednessPolicy

static attribute filters that determine if the check..Access() and check..Exposure() methods should be called. This is only called once per instruction execution since it filters all cases that would set a CG. Filter conditions have to apply to both field access and object exposure.

Specified by:

createFieldLockInfo in class GenericSharednessPolicy

checkOtherRunnables

protected boolean checkOtherRunnables(ThreadInfo ti)

Specified by:

checkOtherRunnables in class GenericSharednessPolicy