gov.nasa.jpf.vm

Class GlobalSharednessPolicy

java.lang.Object

gov.nasa.jpf.vm.GenericSharednessPolicy

gov.nasa.jpf.vm.GlobalSharednessPolicy

All Implemented Interfaces:

Attributor, SharednessPolicy

public class GlobalSharednessPolicy
extends GenericSharednessPolicy

a SharedObjectPolicy that uses search global ThreadInfoSets and FieldLockInfos, i.e. we remember thread access of all previously executed paths. Use this policy for bug finding modes that don't have to create replay-able traces. Note that this policy requires search global object ids (SGOID), i.e. only works with Heap implementations providing SGOIDs

Field Summary

Fields

Modifier and Type	Field and Description
protected SparseObjVector<FieldLockInfo>	globalFliCache
protected SparseObjVector<ThreadInfoSet>	globalTisCache

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
GlobalSharednessPolicy(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.
protected FieldLockInfo	getRegisteredFieldLockInfo(int key, ThreadInfo ti)
protected ThreadInfoSet	getRegisteredThreadInfoSet(int key, ThreadInfo allocThread)
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

Field Detail

globalTisCache

protected SparseObjVector<ThreadInfoSet> globalTisCache

globalFliCache

protected SparseObjVector<FieldLockInfo> globalFliCache

Constructor Detail

GlobalSharednessPolicy

public GlobalSharednessPolicy(Config config)

Method Detail

getRegisteredThreadInfoSet

protected ThreadInfoSet getRegisteredThreadInfoSet(int key,
                                                   ThreadInfo allocThread)

getRegisteredFieldLockInfo

protected FieldLockInfo getRegisteredFieldLockInfo(int key,
                                                   ThreadInfo ti)

checkOtherRunnables

protected boolean checkOtherRunnables(ThreadInfo ti)

Specified by:

checkOtherRunnables in class GenericSharednessPolicy

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