src/main/gov/nasa/jpf/vm/GlobalSharednessPolicy.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.util.SparseObjVector;
  22
  23 /**
  24  * a SharedObjectPolicy that uses search global ThreadInfoSets and FieldLockInfos,
  25  * i.e. we remember thread access of all previously executed paths.
  26  *
  27  * Use this policy for bug finding modes that don't have to create replay-able traces.
  28  *
  29  * Note that this policy requires search global object ids (SGOID), i.e. only works
  30  * with Heap implementations providing SGOIDs
  31  */
  32
  33 public class GlobalSharednessPolicy extends GenericSharednessPolicy {
  34   // our global caches
  35   protected SparseObjVector<ThreadInfoSet> globalTisCache = new SparseObjVector<ThreadInfoSet>(1024);
  36   protected SparseObjVector<FieldLockInfo> globalFliCache = new SparseObjVector<FieldLockInfo>(1024);
  37
  38
  39   public GlobalSharednessPolicy (Config config){
  40     super(config);
  41   }
  42
  43   protected ThreadInfoSet getRegisteredThreadInfoSet (int key, ThreadInfo allocThread) {
  44     ThreadInfoSet tis = globalTisCache.get(key);
  45     if (tis == null) {
  46       tis = new TidSet(allocThread);
  47       globalTisCache.set(key, tis);
  48     }
  49
  50     return tis;
  51   }
  52
  53   protected FieldLockInfo getRegisteredFieldLockInfo (int key, ThreadInfo ti){
  54     FieldLockInfo fli = globalFliCache.get(key);
  55
  56     if (fli == null){
  57       int[] lockRefs = ti.getLockedObjectReferences();
  58       if (lockRefs.length == 0) {
  59         fli = FieldLockInfo.getEmptyFieldLockInfo();
  60       } else if (lockRefs.length == 1){
  61         fli = new SingleLockThresholdFli(ti, lockRefs[0], lockThreshold);
  62       } else {
  63         fli = new PersistentLockSetThresholdFli(ti, lockRefs, lockThreshold);
  64       }
  65
  66       globalFliCache.set(key, fli);
  67     }
  68
  69     return fli;
  70   }
  71
  72   @Override
  73   protected boolean checkOtherRunnables (ThreadInfo ti){
  74     // this is a search global policy we don't care if other threads are runnable or already terminated
  75     return true;
  76   }
  77
  78   @Override
  79   public void initializeObjectSharedness (ThreadInfo allocThread, DynamicElementInfo ei) {
  80     ThreadInfoSet tis = getRegisteredThreadInfoSet(ei.getObjectRef(), allocThread);
  81     ei.setReferencingThreads( tis);
  82   }
  83
  84   @Override
  85   public void initializeClassSharedness (ThreadInfo allocThread, StaticElementInfo ei) {
  86     ThreadInfoSet tis;
  87     int ref = ei.getClassObjectRef();
  88     if (ref == MJIEnv.NULL) { // startup class, we don't have a class object yet
  89       // note that we don't have to store this in our globalCache since we can never
  90       // backtrack to a point where the startup classes were not initialized yet.
  91       // <2do> is this true for MultiProcessVM ?
  92       tis = new TidSet(allocThread);
  93     } else {
  94       tis = getRegisteredThreadInfoSet(ref, allocThread);
  95     }
  96
  97     ei.setReferencingThreads(tis);
  98     ei.setExposed(); // static fields are per se exposed
  99   }
 100
 101   @Override
 102   protected FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
 103     int id;
 104
 105     if (ei instanceof StaticElementInfo){
 106       id = ((StaticElementInfo)ei).getClassObjectRef();
 107       if (id == MJIEnv.NULL){
 108         return null;
 109       }
 110     } else {
 111       id = ei.getObjectRef();
 112     }
 113
 114     return getRegisteredFieldLockInfo( id, ti);
 115   }
 116 }