gov.nasa.jpf.vm

Class ThresholdFieldLockInfo

java.lang.Object

gov.nasa.jpf.vm.FieldLockInfo

gov.nasa.jpf.vm.ThresholdFieldLockInfo

All Implemented Interfaces:

java.lang.Cloneable

Direct Known Subclasses:

LockSetThresholdFli, SingleLockThresholdFli

public abstract class ThresholdFieldLockInfo
extends FieldLockInfo
implements java.lang.Cloneable

a FieldLockInfo that assumes lock protection after n accesses with non-empty lock sets

Field Summary

Fields

Modifier and Type	Field and Description
protected int	remainingChecks

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

empty, tiLastCheck

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	ThresholdFieldLockInfo(int remainingChecks)

Method Summary

Modifier and Type	Method and Description
protected void	checkFailedLockAssumption(ThreadInfo ti, ElementInfo ei, FieldInfo fi)
protected FieldLockInfo	getInstance(int nRemaining) this implements a path-local FieldLockInfo that are never mutated this has to be overridden for search global FieldLockInfos
boolean	isProtected()

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

checkProtection, cleanUp, clone, getCandidateLockSet, getEmptyFieldLockInfo, isFinal, needsPindown

Methods inherited from class java.lang.Object

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

Field Detail

remainingChecks

protected int remainingChecks

Constructor Detail

ThresholdFieldLockInfo

protected ThresholdFieldLockInfo(int remainingChecks)

Method Detail

isProtected

public boolean isProtected()

Specified by:

isProtected in class FieldLockInfo

checkFailedLockAssumption

protected void checkFailedLockAssumption(ThreadInfo ti,
                                         ElementInfo ei,
                                         FieldInfo fi)

getInstance

protected FieldLockInfo getInstance(int nRemaining)

this implements a path-local FieldLockInfo that are never mutated this has to be overridden for search global FieldLockInfos