gov.nasa.jpf.vm

Class GenericSharednessPolicy

java.lang.Object

gov.nasa.jpf.vm.GenericSharednessPolicy

All Implemented Interfaces:

Attributor, SharednessPolicy

Direct Known Subclasses:

GlobalSharednessPolicy, PathSharednessPolicy

public abstract class GenericSharednessPolicy
extends java.lang.Object
implements SharednessPolicy, Attributor

an abstract SharednessPolicy implementation that makes use of both shared field access CGs and exposure CGs. This class is highly configurable, both in terms of using exposure CGs and filters. The *never_break filters should be used with care to avoid missing defects, especially the (transitive) method filters. NOTE - the default settings from jpf-core/jpf.properties include several java.util.concurrent* and java.lang.* fields/methods that can in fact contribute to concurrency defects, esp. in SUTs that explicitly use Thread/ThreadGroup objects, in which case they should be removed. The *always_break field filter should only be used for white box SUT analysis if JPF fails to detect sharedness (e.g. because no exposure is used). This should only go into application property files

Field Summary

Fields

Modifier and Type	Field and Description
protected FieldSpecMatcher	alwaysBreakOnFields always break matching fields, no matter if object is already shared or not
protected TypeSpecMatcher	alwaysBreakOnTypes
protected boolean	breakOnExposure do we add CGs for objects that could become shared, e.g.
protected int	lockThreshold
protected static JPFLogger	logger
protected MethodSpecMatcher	neverBreakInMethods never break or expose if a matching method is on the stack
protected FieldSpecMatcher	neverBreakOnFields never break on matching fields
protected TypeSpecMatcher	neverBreakOnTypes
protected boolean	skipConstructedFinals
protected boolean	skipFinals do we break on final field access
protected boolean	skipInits do we break inside of constructors (note that 'this' references could leak from ctors, but this is rather unusual)
protected boolean	skipStaticFinals
protected boolean	useSyncDetection options to filter out lock protected field access, which is not supposed to cause shared CGs (this has no effect on exposure though)
protected VM	vm

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	GenericSharednessPolicy(Config config)

Method Summary

Modifier and Type	Method and Description
boolean	canHaveSharedArrayCG(ThreadInfo ti, Instruction insn, ElementInfo eiArray, int idx)
boolean	canHaveSharedClassCG(ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi)
protected java.lang.Boolean	canHaveSharednessCG(ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi)
boolean	canHaveSharedObjectCG(ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi) check to determine if call site, object/class attributes and thread execution state could cause CGs.
protected abstract boolean	checkOtherRunnables(ThreadInfo ti)
void	cleanupThreadTermination(ThreadInfo ti) give policy a chance to clean up referencing ThreadInfoSets upon thread termination
protected abstract 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 ChoiceGenerator<ThreadInfo>	getRunnableCG(java.lang.String id, ThreadInfo tiCurrent)
protected ThreadInfo[]	getRunnables(ApplicationContext appCtx)
void	initializeSharednessPolicy(VM vm, ApplicationContext appCtx) this can be used to initializeSharednessPolicy per-application mechanisms such as ClassInfo attribution
protected boolean	isFirstExposure(ElementInfo eiFieldOwner, ElementInfo eiExposed)
protected boolean	isInNeverBreakMethod(ThreadInfo ti)
protected boolean	isRelevantArrayAccess(ThreadInfo ti, Instruction insn, ElementInfo ei, int index)
protected boolean	isRelevantStaticFieldAccess(ThreadInfo ti, Instruction insn, ElementInfo ei, FieldInfo fi)
void	setAttributes(ClassInfo ci)
protected void	setFieldAttributes(FieldSpecMatcher neverMatcher, FieldSpecMatcher alwaysMatcher, ClassInfo ci)
protected boolean	setNextChoiceGenerator(ChoiceGenerator<ThreadInfo> cg)
protected boolean	setsExposureCG(ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed)
boolean	setsSharedArrayCG(ThreadInfo ti, Instruction insn, ElementInfo eiArray, int index)
boolean	setsSharedClassCG(ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi)
boolean	setsSharedClassExposureCG(ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed)
boolean	setsSharedObjectCG(ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi) <2do> explain why not transitive these are the public interfaces towards FieldInstructions.
boolean	setsSharedObjectExposureCG(ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed)
protected void	setTypeAttributes(TypeSpecMatcher neverMatcher, TypeSpecMatcher alwaysMatcher, ClassInfo ciLoaded)
ElementInfo	updateArraySharedness(ThreadInfo ti, ElementInfo ei, int idx)
ElementInfo	updateClassSharedness(ThreadInfo ti, ElementInfo ei, FieldInfo fi)
protected ElementInfo	updateFieldLockInfo(ThreadInfo ti, ElementInfo ei, FieldInfo fi) generic version of FieldLockInfo update, which relies on FieldLockInfo implementation to determine if ElementInfo needs to be cloned
ElementInfo	updateObjectSharedness(ThreadInfo ti, ElementInfo ei, FieldInfo fi)
protected ElementInfo	updateSharedness(ThreadInfo ti, ElementInfo ei, FieldInfo fi)

Methods inherited from class java.lang.Object

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

Methods inherited from interface gov.nasa.jpf.vm.SharednessPolicy

initializeClassSharedness, initializeObjectSharedness

Field Detail

logger

protected static JPFLogger logger

neverBreakOnTypes

protected TypeSpecMatcher neverBreakOnTypes

alwaysBreakOnTypes

protected TypeSpecMatcher alwaysBreakOnTypes

neverBreakInMethods

protected MethodSpecMatcher neverBreakInMethods

never break or expose if a matching method is on the stack

neverBreakOnFields

protected FieldSpecMatcher neverBreakOnFields

never break on matching fields

alwaysBreakOnFields

protected FieldSpecMatcher alwaysBreakOnFields

always break matching fields, no matter if object is already shared or not

skipFinals

protected boolean skipFinals

do we break on final field access

skipConstructedFinals

protected boolean skipConstructedFinals

skipStaticFinals

protected boolean skipStaticFinals

skipInits

protected boolean skipInits

do we break inside of constructors (note that 'this' references could leak from ctors, but this is rather unusual)

breakOnExposure

protected boolean breakOnExposure

do we add CGs for objects that could become shared, e.g. when storing a reference to a non-shared object in a shared object field. NOTE: this is a conservative measure since we don't know yet at the point of exposure if the object will ever be shared, which means it can cause state explosion.

useSyncDetection

protected boolean useSyncDetection

options to filter out lock protected field access, which is not supposed to cause shared CGs (this has no effect on exposure though)

lockThreshold

protected int lockThreshold

vm

protected VM vm

Constructor Detail

GenericSharednessPolicy

protected GenericSharednessPolicy(Config config)

Method Detail

setTypeAttributes

protected void setTypeAttributes(TypeSpecMatcher neverMatcher,
                                 TypeSpecMatcher alwaysMatcher,
                                 ClassInfo ciLoaded)

setFieldAttributes

protected void setFieldAttributes(FieldSpecMatcher neverMatcher,
                                  FieldSpecMatcher alwaysMatcher,
                                  ClassInfo ci)

isInNeverBreakMethod

protected boolean isInNeverBreakMethod(ThreadInfo ti)

checkOtherRunnables

protected abstract boolean checkOtherRunnables(ThreadInfo ti)

canHaveSharednessCG

protected java.lang.Boolean canHaveSharednessCG(ThreadInfo ti,
                                                Instruction insn,
                                                ElementInfo eiFieldOwner,
                                                FieldInfo fi)

createFieldLockInfo

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

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.

updateFieldLockInfo

protected ElementInfo updateFieldLockInfo(ThreadInfo ti,
                                          ElementInfo ei,
                                          FieldInfo fi)

generic version of FieldLockInfo update, which relies on FieldLockInfo implementation to determine if ElementInfo needs to be cloned

getRunnables

protected ThreadInfo[] getRunnables(ApplicationContext appCtx)

getRunnableCG

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

setNextChoiceGenerator

protected boolean setNextChoiceGenerator(ChoiceGenerator<ThreadInfo> cg)

updateSharedness

protected ElementInfo updateSharedness(ThreadInfo ti,
                                       ElementInfo ei,
                                       FieldInfo fi)

setsExposureCG

protected boolean setsExposureCG(ThreadInfo ti,
                                 Instruction insn,
                                 ElementInfo eiFieldOwner,
                                 FieldInfo fi,
                                 ElementInfo eiExposed)

isFirstExposure

protected boolean isFirstExposure(ElementInfo eiFieldOwner,
                                  ElementInfo eiExposed)

initializeSharednessPolicy

public void initializeSharednessPolicy(VM vm,
                                       ApplicationContext appCtx)

this can be used to initializeSharednessPolicy per-application mechanisms such as ClassInfo attribution

Specified by:

initializeSharednessPolicy in interface SharednessPolicy

setAttributes

public void setAttributes(ClassInfo ci)

Specified by:

setAttributes in interface Attributor

updateObjectSharedness

public ElementInfo updateObjectSharedness(ThreadInfo ti,
                                          ElementInfo ei,
                                          FieldInfo fi)

Specified by:

updateObjectSharedness in interface SharednessPolicy

updateClassSharedness

public ElementInfo updateClassSharedness(ThreadInfo ti,
                                         ElementInfo ei,
                                         FieldInfo fi)

Specified by:

updateClassSharedness in interface SharednessPolicy

updateArraySharedness

public ElementInfo updateArraySharedness(ThreadInfo ti,
                                         ElementInfo ei,
                                         int idx)

Specified by:

updateArraySharedness in interface SharednessPolicy

canHaveSharedObjectCG

public boolean canHaveSharedObjectCG(ThreadInfo ti,
                                     Instruction insn,
                                     ElementInfo eiFieldOwner,
                                     FieldInfo fi)

check to determine if call site, object/class attributes and thread execution state could cause CGs. This is called before sharedness is updated, i.e. can be used to filter objects/classes that should not be sharedness tracked

Specified by:

canHaveSharedObjectCG in interface SharednessPolicy

canHaveSharedClassCG

public boolean canHaveSharedClassCG(ThreadInfo ti,
                                    Instruction insn,
                                    ElementInfo eiFieldOwner,
                                    FieldInfo fi)

Specified by:

canHaveSharedClassCG in interface SharednessPolicy

canHaveSharedArrayCG

public boolean canHaveSharedArrayCG(ThreadInfo ti,
                                    Instruction insn,
                                    ElementInfo eiArray,
                                    int idx)

Specified by:

canHaveSharedArrayCG in interface SharednessPolicy

setsSharedObjectCG

public boolean setsSharedObjectCG(ThreadInfo ti,
                                  Instruction insn,
                                  ElementInfo eiFieldOwner,
                                  FieldInfo fi)

<2do> explain why not transitive these are the public interfaces towards FieldInstructions. Callers have to be aware this will change the /referenced/ ElementInfo in case the respective object becomes exposed

Specified by:

setsSharedObjectCG in interface SharednessPolicy

setsSharedClassCG

public boolean setsSharedClassCG(ThreadInfo ti,
                                 Instruction insn,
                                 ElementInfo eiFieldOwner,
                                 FieldInfo fi)

Specified by:

setsSharedClassCG in interface SharednessPolicy

setsSharedArrayCG

public boolean setsSharedArrayCG(ThreadInfo ti,
                                 Instruction insn,
                                 ElementInfo eiArray,
                                 int index)

Specified by:

setsSharedArrayCG in interface SharednessPolicy

isRelevantStaticFieldAccess

protected boolean isRelevantStaticFieldAccess(ThreadInfo ti,
                                              Instruction insn,
                                              ElementInfo ei,
                                              FieldInfo fi)

isRelevantArrayAccess

protected boolean isRelevantArrayAccess(ThreadInfo ti,
                                        Instruction insn,
                                        ElementInfo ei,
                                        int index)

setsSharedObjectExposureCG

public boolean setsSharedObjectExposureCG(ThreadInfo ti,
                                          Instruction insn,
                                          ElementInfo eiFieldOwner,
                                          FieldInfo fi,
                                          ElementInfo eiExposed)

Specified by:

setsSharedObjectExposureCG in interface SharednessPolicy

setsSharedClassExposureCG

public boolean setsSharedClassExposureCG(ThreadInfo ti,
                                         Instruction insn,
                                         ElementInfo eiFieldOwner,
                                         FieldInfo fi,
                                         ElementInfo eiExposed)

Specified by:

setsSharedClassExposureCG in interface SharednessPolicy

cleanupThreadTermination

public void cleanupThreadTermination(ThreadInfo ti)

Description copied from interface: SharednessPolicy

give policy a chance to clean up referencing ThreadInfoSets upon thread termination

Specified by:

cleanupThreadTermination in interface SharednessPolicy