gov.nasa.jpf.vm

Class FieldLockInfo

java.lang.Object

gov.nasa.jpf.vm.FieldLockInfo

All Implemented Interfaces:

java.lang.Cloneable

Direct Known Subclasses:

ThresholdFieldLockInfo

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

class encapsulating the lock protection status for field access instructions. Used by on-the-fly partial order reduction in FieldInstruction to determine if a GET/PUT_FIELD/STATIC insn has to be treated as a boundary step (terminates a transition). If the field access is always protected by a lock, only the corresponding sync (INVOKExx or MONITORENTER) are boundary steps, thus the number of states can be significantly reduced. FieldLockInfos are only used if vm.por.sync_detection is set NOTE this might involve assumptions that can be violated in subsequent paths, and might cause potential races to go undetected

Field Summary

Fields

Modifier and Type	Field and Description
protected static FieldLockInfo	empty
protected ThreadInfo	tiLastCheck

Constructor Summary

Constructors

Constructor and Description
FieldLockInfo()

Method Summary

Modifier and Type	Method and Description
abstract FieldLockInfo	checkProtection(ThreadInfo ti, ElementInfo ei, FieldInfo fi)
abstract FieldLockInfo	cleanUp(Heap heap)
java.lang.Object	clone()
protected abstract int[]	getCandidateLockSet()
static FieldLockInfo	getEmptyFieldLockInfo()
boolean	isFinal()
abstract boolean	isProtected()
boolean	needsPindown(ElementInfo ei)

Methods inherited from class java.lang.Object

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

Field Detail

empty

protected static final FieldLockInfo empty

tiLastCheck

protected ThreadInfo tiLastCheck

Constructor Detail

FieldLockInfo

public FieldLockInfo()

Method Detail

getEmptyFieldLockInfo

public static FieldLockInfo getEmptyFieldLockInfo()

checkProtection

public abstract FieldLockInfo checkProtection(ThreadInfo ti,
                                              ElementInfo ei,
                                              FieldInfo fi)

isProtected

public abstract boolean isProtected()

cleanUp

public abstract FieldLockInfo cleanUp(Heap heap)

getCandidateLockSet

protected abstract int[] getCandidateLockSet()

isFinal

public boolean isFinal()

needsPindown

public boolean needsPindown(ElementInfo ei)

clone

public java.lang.Object clone()
                       throws java.lang.CloneNotSupportedException

Overrides:

clone in class java.lang.Object

Throws:

java.lang.CloneNotSupportedException