2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
6 * The Java Pathfinder core (jpf-core) platform is licensed under the
7 * Apache License, Version 2.0 (the "License"); you may not use this file except
8 * in compliance with the License. You may obtain a copy of the License at
10 * http://www.apache.org/licenses/LICENSE-2.0.
12 * Unless required by applicable law or agreed to in writing, software
13 * distributed under the License is distributed on an "AS IS" BASIS,
14 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
15 * See the License for the specific language governing permissions and
16 * limitations under the License.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.JPF;
23 import java.util.logging.Logger;
26 * a FieldLockInfo implementation with the following strategy:
28 * - at each check, store the intersection of the current threads lock set
29 * with the previous field lock set
30 * - if the access was checked less than CHECK_THRESHOLD times, report the
31 * field as unprotected
32 * - if the field lock set doesn't become empty after CHECK_THRESHOLD, report
33 * the field as protected
34 * - as an optimization, raise the check level above the threshold if we
35 * have a good probability that a current lock is a protection lock for this
37 * - continue to check even after reaching the threshold, so that we
38 * can at least report a violated assumption
40 * NOTE there is a subtle problem: if we ever falsely assume lock protection
41 * in a path that subsequently recycles the shared object (e.g. by leading
42 * into an end state), we loose the assumption. If this is followed by
43 * a backtrack and execution of a path that uses a conflicting assumption
44 * (different or no lock), we will NOT detect potential races unless
45 * vm.por.sync_detection.pindown is set (which has some runtime costs)
48 public class StatisticFieldLockInfoFactory implements FieldLockInfoFactory {
50 static Logger log = JPF.getLogger("gov.nasa.jpf.vm.FieldLockInfo");
53 * the number of checks after which we decide if a non-empty lock set
54 * means this field is protected
56 static int CHECK_THRESHOLD = 5;
59 * do we want objects with final field lock assumptions to be pinned
60 * down (not garbage collected), to make sure we don't loose these
61 * assumptions and subsequently fail to detect an assumption violation
62 * after backtracking (see above)
64 static boolean PINDOWN = false;
67 * do we look for strong locking candidates (i.e. assume protection
68 * if there is a lock related to the object).
69 * NOTE this can lead to undetected race conditions if the assumption
72 static boolean AGRESSIVE = false;
75 public StatisticFieldLockInfoFactory (Config conf) {
76 CHECK_THRESHOLD = conf.getInt("vm.por.sync_detection.threshold", CHECK_THRESHOLD);
77 PINDOWN = conf.getBoolean("vm.por.sync_detection.pindown", PINDOWN);
78 AGRESSIVE = conf.getBoolean("vm.por.sync_detection.agressive",AGRESSIVE);
82 public FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
83 int[] currentLockRefs = ti.getLockedObjectReferences();
84 int nLocks = currentLockRefs.length;
87 return FieldLockInfo.empty; // not protected, never will
92 int lockCandidateRef = strongProtectionCandidate(ei,fi,currentLockRefs);
93 if (lockCandidateRef != MJIEnv.NULL) {
94 // NOTE we raise the checklevel
95 return new SingleLockFli( ti, lockCandidateRef, CHECK_THRESHOLD);
99 if (nLocks == 1) { // most common case
100 return new SingleLockFli( ti, currentLockRefs[0], 0);
103 return new MultiLockFli( ti, fi, currentLockRefs);
109 * check if the current thread lockset contains a lock with a high probability
110 * that it is a protection lock for this field. We need this to avoid
111 * state explosion due to the number of fields to check. Note that we don't
112 * necessarily have to answer/decide which one is the best match in case of
113 * several candidates (if we don't use this to reduce to StatisticFieldLockInfo1)
115 * For instance fields, this would be a lock with a distance <= 1.
116 * For static fields, the corresponding class object is a good candidate.
118 int strongProtectionCandidate (ElementInfo ei, FieldInfo fi, int[] currentLockRefs) {
119 int n = currentLockRefs.length;
120 Heap heap = VM.getVM().getHeap();
122 if (fi.isStatic()) { // static field, check for class object locking
123 ClassInfo ci = fi.getClassInfo();
124 int cref = ci.getClassObjectRef();
126 for (int i=0; i<n; i++) {
127 if (currentLockRefs[i] == cref) {
128 ElementInfo e = heap.get(cref);
129 log.info("sync-detection: " + ei + " assumed to be synced on class object: @" + e);
134 } else { // instance field, use lock distance as a heuristic
135 int objRef = ei.getObjectRef();
137 for (int i=0; i<n; i++) {
138 int eidx = currentLockRefs[i];
140 // case 1: synchronization on field owner itself
141 if (eidx == objRef) {
142 log.info("sync-detection: " + ei + " assumed to be synced on itself");
146 ElementInfo e = heap.get(eidx);
148 // case 2: synchronization on sibling field that is a private lock object
149 if (ei.hasRefField(eidx)) {
150 log.info("sync-detection: "+ ei + " assumed to be synced on sibling: " + e);
154 // case 3: synchronization on owner of object holding field (sync wrapper)
155 if (e.hasRefField(objRef)) {
156 log.info("sync-detection: " + ei + " assumed to be synced on object wrapper: " + e);
167 //--- root for our concrete FieldLockInfo classes
168 static abstract class StatisticFieldLockInfo extends FieldLockInfo {
172 public boolean isProtected () {
173 return (checkLevel >= CHECK_THRESHOLD);
177 public boolean needsPindown (ElementInfo ei) {
178 return PINDOWN && (checkLevel >= CHECK_THRESHOLD);
181 protected void checkFailedLockAssumption(ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
182 if (checkLevel >= CHECK_THRESHOLD) {
183 lockAssumptionFailed(ti,ei,fi);
188 //--- Fli for a single lock
189 static class SingleLockFli extends StatisticFieldLockInfo {
192 SingleLockFli (ThreadInfo ti, int lockRef, int nChecks) {
195 this.lockRef = lockRef;
196 checkLevel = nChecks;
200 protected int[] getCandidateLockSet() {
201 int[] set = { lockRef };
207 public FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
208 int[] currentLockRefs = ti.getLockedObjectReferences();
209 int nLocks = currentLockRefs.length;
213 for (int i=0; i<nLocks; i++) {
214 if (currentLockRefs[i] == lockRef) {
219 checkFailedLockAssumption(ti, ei, fi);
224 * only called at the end of the gc on all live objects. The recycled ones
225 * are either already nulled in the heap, or are not marked as live
228 public FieldLockInfo cleanUp (Heap heap) {
229 ElementInfo ei = heap.get(lockRef);
230 if (!heap.isAlive(ei)) {
231 return FieldLockInfo.empty;
238 public String toString() {
239 return ("SingleLockFli {checkLevel="+checkLevel+",lock="+lockRef + '}');
244 //--- StatisticFieldLockInfo for lock sets
245 static class MultiLockFli extends StatisticFieldLockInfo {
249 // this is only used once during prototype generation
250 public MultiLockFli (ThreadInfo ti, FieldInfo fi, int[] currentLockRefs) {
251 lockRefSet = currentLockRefs;
255 protected int[] getCandidateLockSet() {
261 public FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
262 int[] currentLockRefs = ti.getLockedObjectReferences();
263 int nLocks = currentLockRefs.length;
267 if (nLocks == 0) { // no current locks, so intersection is empty
268 checkFailedLockAssumption(ti, ei, fi);
271 } else { // we had a lock set, and there currently is at least one lock held
273 int[] newLset = new int[lockRefSet.length];
275 for (int i=0; i<nLocks; i++) { // get the set intersection
276 int leidx = currentLockRefs[i];
278 for (int j=0; j<lockRefSet.length; j++) {
279 if (lockRefSet[j] == leidx) {
280 newLset[l++] = leidx;
281 break; // sets don't contain duplicates
286 if (l == 0) { // intersection empty
287 checkFailedLockAssumption(ti, ei, fi);
290 } else if (l == 1) { // only one candidate left
291 return new SingleLockFli( ti, newLset[0], checkLevel);
293 } else if (l < newLset.length) { // candidate set did shrink
294 lockRefSet = new int[l];
295 System.arraycopy(newLset, 0, lockRefSet, 0, l);
307 * only called at the end of the gc on all live objects. The recycled ones
308 * are either already nulled in the heap, or are not marked as live
311 public FieldLockInfo cleanUp (Heap heap) {
315 if (lockRefSet != null) {
316 for (int i=0; i<lockRefSet.length; i++) {
317 ElementInfo ei = heap.get(lockRefSet[i]);
319 if (!heap.isAlive(ei)) { // we got a stale one, so we have to change us
320 if (newSet == null) { // first one, copy everything up to it
321 newSet = new int[lockRefSet.length-1];
323 System.arraycopy(lockRefSet, 0, newSet, 0, i);
329 if (newSet != null) { // we already had a dangling ref, now copy the live ones
330 newSet[l++] = lockRefSet[i];
337 assert (newSet != null);
338 return new SingleLockFli(tiLastCheck, newSet[0], checkLevel);
341 if (newSet != null) {
342 if (l == newSet.length) { // we just had one stale ref
344 } else { // several stales - make a new copy
348 lockRefSet = new int[l];
349 System.arraycopy(newSet, 0, lockRefSet, 0, l);
358 public String toString() {
359 StringBuilder sb = new StringBuilder();
360 sb.append("MultiLockFli {");
361 sb.append("checkLevel=");
362 sb.append(checkLevel);
363 sb.append(",lset=[");
364 if (lockRefSet != null) {
365 for (int i=0; i<lockRefSet.length; i++) {
369 sb.append(lockRefSet[i]);
374 return sb.toString();