src/main/gov/nasa/jpf/vm/LockSetThresholdFli.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 /**
  21  * a threshold FieldLockInfo with a set of lock candidates
  22  *
  23  * this is the destructive update version. Override singleLockThresholdFli() and lockSetthresholdFli() for
  24  * a persistent version
  25  */
  26 public class LockSetThresholdFli extends ThresholdFieldLockInfo {
  27
  28   protected int[] lockRefSet;
  29
  30   // this is only used once during prototype generation
  31   public LockSetThresholdFli(ThreadInfo ti, int[] currentLockRefs, int checkThreshold) {
  32     super(checkThreshold);
  33
  34     tiLastCheck = ti;
  35     lockRefSet = currentLockRefs;
  36   }
  37
  38   @Override
  39   protected int[] getCandidateLockSet() {
  40     return lockRefSet;
  41   }
  42
  43   /**
  44    * override this for search global FieldLockInfos
  45    */
  46   protected SingleLockThresholdFli singleLockThresholdFli (ThreadInfo ti, int lockRef, int remainingChecks) {
  47     return new SingleLockThresholdFli(ti, lockRef, remainingChecks);
  48   }
  49
  50   protected LockSetThresholdFli lockSetThresholdFli (ThreadInfo ti, int[] lockRefs, int remainingChecks){
  51     this.lockRefSet = lockRefs;
  52     this.tiLastCheck = ti;
  53     this.remainingChecks = remainingChecks;
  54
  55     return this;
  56   }
  57
  58   @Override
  59   public FieldLockInfo checkProtection(ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
  60     int[] currentLockRefs = ti.getLockedObjectReferences();
  61     int nLocks = currentLockRefs.length;
  62     int nRemaining = Math.max(0, remainingChecks--);
  63
  64     if (nLocks == 0) { // no current locks, so intersection is empty
  65       checkFailedLockAssumption(ti, ei, fi);
  66       return empty;
  67
  68     } else { // we had a lock set, and there currently is at least one lock held
  69       int l = 0;
  70       int[] newLset = new int[lockRefSet.length];
  71
  72       for (int i = 0; i < nLocks; i++) { // get the set intersection
  73         int leidx = currentLockRefs[i];
  74
  75         for (int j = 0; j < lockRefSet.length; j++) {
  76           if (lockRefSet[j] == leidx) {
  77             newLset[l++] = leidx;
  78             break; // sets don't contain duplicates
  79           }
  80         }
  81       }
  82
  83       if (l == 0) { // intersection empty
  84         checkFailedLockAssumption(ti, ei, fi);
  85         return empty;
  86
  87       } else if (l == 1) { // only one candidate left
  88         return singleLockThresholdFli(ti, newLset[0], nRemaining);
  89
  90       } else if (l < newLset.length) { // candidate set did shrink
  91         int[] newLockRefSet = new int[l];
  92         System.arraycopy(newLset, 0, newLockRefSet, 0, l);
  93         return lockSetThresholdFli(ti, newLockRefSet, nRemaining);
  94
  95       } else {
  96         return lockSetThresholdFli(ti, lockRefSet, nRemaining);
  97       }
  98     }
  99   }
 100
 101   /**
 102    * only called at the end of the gc on all live objects. The recycled ones are
 103    * either already nulled in the heap, or are not marked as live
 104    */
 105   @Override
 106   public FieldLockInfo cleanUp(Heap heap) {
 107     int[] newSet = null;
 108     int l = 0;
 109
 110     if (lockRefSet != null) {
 111       for (int i = 0; i < lockRefSet.length; i++) {
 112         ElementInfo ei = heap.get(lockRefSet[i]);
 113
 114         if (!heap.isAlive(ei)) { // we got a stale one, so we have to change us
 115           if (newSet == null) { // first one, copy everything up to it
 116             newSet = new int[lockRefSet.length - 1];
 117             if (i > 0) {
 118               System.arraycopy(lockRefSet, 0, newSet, 0, i);
 119               l = i;
 120             }
 121           }
 122
 123         } else {
 124           if (newSet != null) { // we already had a dangling ref, now copy the live ones
 125             newSet[l++] = lockRefSet[i];
 126           }
 127         }
 128       }
 129     }
 130
 131     if (l == 1) {
 132       assert (newSet != null);
 133       return new SingleLockThresholdFli(tiLastCheck, newSet[0], remainingChecks);
 134
 135     } else {
 136       if (newSet != null) {
 137         if (l == newSet.length) { // we just had one stale ref
 138           lockRefSet = newSet;
 139         } else { // several stales - make a new copy
 140           if (l == 0) {
 141             return empty;
 142           } else {
 143             lockRefSet = new int[l];
 144             System.arraycopy(newSet, 0, lockRefSet, 0, l);
 145           }
 146         }
 147       }
 148       return this;
 149     }
 150   }
 151
 152   @Override
 153   public String toString() {
 154     StringBuilder sb = new StringBuilder();
 155     sb.append("LockSetThresholdFli {");
 156     sb.append("remainingChecks=");
 157     sb.append(remainingChecks);
 158     sb.append(",lset=[");
 159     if (lockRefSet != null) {
 160       for (int i = 0; i < lockRefSet.length; i++) {
 161         if (i > 0) {
 162           sb.append(',');
 163         }
 164         sb.append(lockRefSet[i]);
 165       }
 166     }
 167     sb.append("]}");
 168
 169     return sb.toString();
 170   }
 171 }