src/main/gov/nasa/jpf/vm/StatisticFieldLockInfoFactory.java

   1 /*
   2  * Copyright (C) 2014, United States Government, as represented by the
   3  * Administrator of the National Aeronautics and Space Administration.
   4  * All rights reserved.
   5  *
   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
   9  *
  10  *        http://www.apache.org/licenses/LICENSE-2.0.
  11  *
  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.
  17  */
  18 package gov.nasa.jpf.vm;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22
  23 import java.util.logging.Logger;
  24
  25 /**
  26  * a FieldLockInfo implementation with the following strategy:
  27  *
  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
  36  *     field
  37  *   - continue to check even after reaching the threshold, so that we
  38  *     can at least report a violated assumption
  39  *
  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)
  46  */
  47
  48 public class StatisticFieldLockInfoFactory implements FieldLockInfoFactory {
  49
  50   static Logger log = JPF.getLogger("gov.nasa.jpf.vm.FieldLockInfo");
  51
  52   /**
  53    * the number of checks after which we decide if a non-empty lock set
  54    * means this field is protected
  55    */
  56   static int CHECK_THRESHOLD = 5;
  57
  58   /**
  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)
  63    */
  64   static boolean PINDOWN = false;
  65
  66   /**
  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
  70    * subsequently fails
  71    */
  72   static boolean AGRESSIVE = false;
  73
  74
  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);
  79   }
  80
  81   @Override
  82   public FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
  83     int[] currentLockRefs = ti.getLockedObjectReferences();
  84     int nLocks = currentLockRefs.length;
  85
  86     if (nLocks == 0) {
  87       return FieldLockInfo.empty; // not protected, never will
  88
  89     } else {
  90
  91       if (AGRESSIVE) {
  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);
  96         }
  97       }
  98
  99       if (nLocks == 1) { // most common case
 100         return new SingleLockFli( ti, currentLockRefs[0], 0);
 101
 102       } else {
 103         return new MultiLockFli( ti, fi, currentLockRefs);
 104       }
 105     }
 106   }
 107
 108   /**
 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)
 114    *
 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.
 117    */
 118   int strongProtectionCandidate (ElementInfo ei, FieldInfo fi, int[] currentLockRefs) {
 119     int n = currentLockRefs.length;
 120     Heap heap = VM.getVM().getHeap();
 121
 122     if (fi.isStatic()) { // static field, check for class object locking
 123       ClassInfo ci = fi.getClassInfo();
 124       int cref = ci.getClassObjectRef();
 125
 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);
 130           return cref;
 131         }
 132       }
 133
 134     } else { // instance field, use lock distance as a heuristic
 135       int objRef = ei.getObjectRef();
 136
 137       for (int i=0; i<n; i++) {
 138         int eidx = currentLockRefs[i];
 139
 140         // case 1: synchronization on field owner itself
 141         if (eidx == objRef) {
 142           log.info("sync-detection: " + ei + " assumed to be synced on itself");
 143           return objRef;
 144         }
 145
 146         ElementInfo e = heap.get(eidx);
 147
 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);
 151           return eidx;
 152         }
 153
 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);
 157           return eidx;
 158         }
 159       }
 160     }
 161
 162     return -1;
 163   }
 164
 165
 166
 167   //--- root for our concrete FieldLockInfo classes
 168   static abstract class StatisticFieldLockInfo extends FieldLockInfo {
 169     int checkLevel;
 170
 171     @Override
 172         public boolean isProtected () {
 173       return (checkLevel >= CHECK_THRESHOLD);
 174     }
 175
 176     @Override
 177         public boolean needsPindown (ElementInfo ei) {
 178       return PINDOWN && (checkLevel >= CHECK_THRESHOLD);
 179     }
 180
 181     protected void checkFailedLockAssumption(ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
 182       if (checkLevel >= CHECK_THRESHOLD) {
 183         lockAssumptionFailed(ti,ei,fi);
 184       }
 185     }
 186   }
 187
 188   //--- Fli for a single lock
 189   static class SingleLockFli extends StatisticFieldLockInfo {
 190     int lockRef;
 191
 192     SingleLockFli (ThreadInfo ti, int lockRef, int nChecks) {
 193       tiLastCheck = ti;
 194
 195       this.lockRef = lockRef;
 196       checkLevel = nChecks;
 197     }
 198
 199     @Override
 200         protected int[] getCandidateLockSet() {
 201       int[] set = { lockRef };
 202       return set;
 203     }
 204
 205
 206     @Override
 207         public FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
 208       int[] currentLockRefs = ti.getLockedObjectReferences();
 209       int nLocks = currentLockRefs.length;
 210
 211       checkLevel++;
 212
 213       for (int i=0; i<nLocks; i++) {
 214         if (currentLockRefs[i] == lockRef) {
 215           return this;
 216         }
 217       }
 218
 219       checkFailedLockAssumption(ti, ei, fi);
 220       return empty;
 221     }
 222
 223     /**
 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
 226      */
 227     @Override
 228         public FieldLockInfo cleanUp (Heap heap) {
 229       ElementInfo ei = heap.get(lockRef);
 230       if (!heap.isAlive(ei)) {
 231         return FieldLockInfo.empty;
 232       } else {
 233         return this;
 234       }
 235     }
 236
 237     @Override
 238         public String toString() {
 239       return ("SingleLockFli {checkLevel="+checkLevel+",lock="+lockRef + '}');
 240     }
 241   }
 242
 243
 244   //--- StatisticFieldLockInfo for lock sets
 245   static class MultiLockFli extends StatisticFieldLockInfo {
 246
 247     int[] lockRefSet;
 248
 249     // this is only used once during prototype generation
 250     public MultiLockFli (ThreadInfo ti, FieldInfo fi, int[] currentLockRefs) {
 251       lockRefSet = currentLockRefs;
 252     }
 253
 254     @Override
 255         protected int[] getCandidateLockSet() {
 256       return lockRefSet;
 257     }
 258
 259
 260     @Override
 261         public FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
 262       int[] currentLockRefs = ti.getLockedObjectReferences();
 263       int nLocks = currentLockRefs.length;
 264
 265       checkLevel++;
 266
 267       if (nLocks == 0) { // no current locks, so intersection is empty
 268         checkFailedLockAssumption(ti, ei, fi);
 269         return empty;
 270
 271       } else { // we had a lock set, and there currently is at least one lock held
 272         int l =0;
 273         int[] newLset = new int[lockRefSet.length];
 274
 275         for (int i=0; i<nLocks; i++) { // get the set intersection
 276           int leidx = currentLockRefs[i];
 277
 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
 282             }
 283           }
 284         }
 285
 286         if (l == 0) { // intersection empty
 287           checkFailedLockAssumption(ti, ei, fi);
 288           return empty;
 289
 290         } else if (l == 1) { // only one candidate left
 291           return new SingleLockFli( ti, newLset[0], checkLevel);
 292
 293         } else if (l < newLset.length) { // candidate set did shrink
 294           lockRefSet = new int[l];
 295           System.arraycopy(newLset, 0, lockRefSet, 0, l);
 296
 297         } else {
 298           // no change
 299         }
 300       }
 301
 302       tiLastCheck = ti;
 303       return this;
 304     }
 305
 306     /**
 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
 309      */
 310     @Override
 311         public FieldLockInfo cleanUp (Heap heap) {
 312       int[] newSet = null;
 313       int l = 0;
 314
 315       if (lockRefSet != null) {
 316         for (int i=0; i<lockRefSet.length; i++) {
 317           ElementInfo ei = heap.get(lockRefSet[i]);
 318
 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];
 322               if (i > 0) {
 323                 System.arraycopy(lockRefSet, 0, newSet, 0, i);
 324                 l = i;
 325               }
 326             }
 327
 328           } else {
 329             if (newSet != null) { // we already had a dangling ref, now copy the live ones
 330               newSet[l++] = lockRefSet[i];
 331             }
 332           }
 333         }
 334       }
 335
 336       if (l == 1) {
 337           assert (newSet != null);
 338           return new SingleLockFli(tiLastCheck, newSet[0], checkLevel);
 339
 340       } else {
 341         if (newSet != null) {
 342           if (l == newSet.length) { // we just had one stale ref
 343             lockRefSet = newSet;
 344           } else { // several stales - make a new copy
 345             if (l == 0) {
 346               return empty;
 347             } else {
 348               lockRefSet = new int[l];
 349               System.arraycopy(newSet, 0, lockRefSet, 0, l);
 350             }
 351           }
 352         }
 353         return this;
 354       }
 355     }
 356
 357     @Override
 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++) {
 366           if (i>0) {
 367             sb.append(',');
 368           }
 369           sb.append(lockRefSet[i]);
 370         }
 371       }
 372       sb.append("]}");
 373
 374       return sb.toString();
 375     }
 376   }
 377 }