src/main/gov/nasa/jpf/vm/SingleLockThresholdFli.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 single lock candidate
  22  * This is the base version that does destructive updates. Override singleLockThresholdFli for a persistent version
  23  */
  24 public class SingleLockThresholdFli extends ThresholdFieldLockInfo {
  25     protected int lockRef;
  26
  27     SingleLockThresholdFli (ThreadInfo ti, int lockRef, int remainingChecks) {
  28       super( remainingChecks);
  29
  30       tiLastCheck = ti;
  31       this.lockRef = lockRef;
  32     }
  33
  34     @Override
  35         protected int[] getCandidateLockSet() {
  36       int[] set = { lockRef };
  37       return set;
  38     }
  39
  40     /**
  41      * override this for path local flis
  42      */
  43     protected SingleLockThresholdFli singleLockThresholdFli (ThreadInfo ti, int lockRef, int remainingChecks){
  44       this.lockRef = lockRef;
  45       this.tiLastCheck = ti;
  46       this.remainingChecks = remainingChecks;
  47
  48       return this;
  49     }
  50
  51     @Override
  52         public FieldLockInfo checkProtection (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
  53       int[] currentLockRefs = ti.getLockedObjectReferences();
  54       int nLocks = currentLockRefs.length;
  55       int nRemaining = Math.max(0, remainingChecks--);
  56
  57       for (int i=0; i<nLocks; i++) {
  58         if (currentLockRefs[i] == lockRef) {
  59           return singleLockThresholdFli( ti, lockRef, nRemaining);
  60         }
  61       }
  62
  63       checkFailedLockAssumption(ti, ei, fi);
  64       return empty;
  65     }
  66
  67     /**
  68      * only called at the end of the gc on all live objects. The recycled ones
  69      * are either already nulled in the heap, or are not marked as live
  70      */
  71     @Override
  72         public FieldLockInfo cleanUp (Heap heap) {
  73       ElementInfo ei = heap.get(lockRef);
  74       if (!heap.isAlive(ei)) {
  75         return FieldLockInfo.empty;
  76       } else {
  77         return this;
  78       }
  79     }
  80
  81     @Override
  82         public String toString() {
  83       return ("SingleLockThresholdFli {remainingChecks="+remainingChecks+",lock="+lockRef + '}');
  84     }
  85
  86 }