src/main/gov/nasa/jpf/vm/PathSharednessPolicy.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
  19 package gov.nasa.jpf.vm;
  20
  21 import gov.nasa.jpf.Config;
  22
  23 /**
  24  * a SharednessPolicy implementation that only computes and keeps sharedness
  25  * along the same path, i.e. not search global.
  26  *
  27  * This is the policy that should be used to create traces that can be replayed.
  28  *
  29  * This policy uses PersistentTids, i.e. it does not modify existing ThreadInfoSet
  30  * instances but replaces upon add/remove with new ones. This ensures that ThreadInfoSets
  31  * are path local, but it also means that operations that add/remove ThreadInfos
  32  * have to be aware of the associated ElementInfo cloning and don't keep/use references
  33  * to old ElementInfos. The upside is that sharedness should be the same along any
  34  * given path, regardless of which paths were executed before. The downside is that all
  35  * callers of ThreadInfoSet updates have to be aware of that the ElementInfo might change.
  36  *
  37  * Note that without additional transition breaks this can miss races due
  38  * to non-overlapping thread execution along all paths. Most real world systems
  39  * have enough scheduling points (sync, field access within loops etc.) to avoid this,
  40  * but short living threads that only have single field access interaction points can
  41  * run into this effect: T1 creates O, starts T2, accesses O and
  42  * terminates before T2 runs. When T2 runs, it only sees access to O from an already
  43  * terminated thread and therefore treats this as a clean handover. Even if
  44  * T2 would break at its O access, there is no CG that would bring T1 back
  45  * into a state between creation and access of O, hence races caused by the O access
  46  * of T1 are missed (see .test.mc.threads.MissedPathTest).
  47  * Two additional scheduling points help to prevent this case: thread start CGs and
  48  * object exposure CGs (/after/ assignment in reference field PUTs where the owning
  49  * object is shared, but the referenced object isn't yet). Both are conservative by
  50  * nature, i.e. might introduce superfluous states for the sake of not missing paths to
  51  * race points. Both can be controlled by configuration options ('cg.threads.break_start'
  52  * and 'vm.por.break_on_exposure').
  53  *
  54  * Note also that shared-ness is not the same along all paths, because our goal
  55  * is just to find potential data races. As long as JPF explores /one/ path that
  56  * leads into a race we are fine - we don't care how many paths don't detect a race.
  57  */
  58 public class PathSharednessPolicy extends GenericSharednessPolicy {
  59
  60   public PathSharednessPolicy (Config config){
  61     super(config);
  62   }
  63
  64   @Override
  65   public void initializeObjectSharedness (ThreadInfo allocThread, DynamicElementInfo ei) {
  66     ei.setReferencingThreads( new PersistentTidSet(allocThread));
  67   }
  68
  69   @Override
  70   public void initializeClassSharedness (ThreadInfo allocThread, StaticElementInfo ei) {
  71     ei.setReferencingThreads( new PersistentTidSet(allocThread));
  72     ei.setExposed(); // static fields are per se exposed
  73   }
  74
  75   @Override
  76   protected FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
  77     int[] lockRefs = ti.getLockedObjectReferences();
  78     switch (lockRefs.length){
  79       case 0:
  80         return FieldLockInfo.getEmptyFieldLockInfo();
  81       case 1:
  82         return new PersistentSingleLockThresholdFli(ti, lockRefs[0], lockThreshold);
  83       default:
  84         return new PersistentLockSetThresholdFli(ti, lockRefs, lockThreshold);
  85     }
  86   }
  87
  88   @Override
  89   protected boolean checkOtherRunnables (ThreadInfo ti){
  90     // since we only consider properties along this path, we can
  91     // ignore states that don't have other runnables
  92     return ti.hasOtherRunnables();
  93   }
  94 }