| java.lang.Object
 gov.nasa.jpf.jvm.FieldLockInfo
gov.nasa.jpf.jvm.StatisticFieldLockInfo
| StatisticFieldLockInfo | | public class StatisticFieldLockInfo extends FieldLockInfo (Code) | | a FieldLockSet implementation with the following strategy
- at each check, store the intersection of the current threads lock set
with the previous field lock set
- if the access was checked less than CHECK_THRESHOLD times, report the
field as unprotected
- if the field lock set doesn't become empty after CHECK_THRESHOLD, report
the field as protected
- as an optimization, raise the check level above the threshold if we
have a good probability that a current lock is a protection lock for this
field
|
| CHECK_THRESHOLD | | final static int CHECK_THRESHOLD(Code) | | |
| checkLevel | | int checkLevel(Code) | | |
| isProtected | | public boolean isProtected()(Code) | | |
| strongProtectionCandidate | | static ElementInfo strongProtectionCandidate(ElementInfo ei, FieldInfo fi, ThreadInfo ti)(Code) | | check if the current thread lockset contains a lock with a high probability
that it is a protection lock for this field. We need this to avoid
state explosion due to the number of fields to check. Note that we don't
necessarily have to answer/decide which one is the best match in case of
several candidates (if we don't use this to reduce to StatisticFieldLockInfo1)
For instance fields, this would be a lock with a distance <= 1.
For static fields, the corresponding class object is a good candidate.
|
|
|