src/main/gov/nasa/jpf/vm/SharednessPolicy.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  * SharednessPolicy is a configured policy that is used to detect data races for objects that are accessible from concurrent
  22  * threads.
  23  *
  24  * Its major purpose is to detect operations that need CGs in order to expose races, and introduce such CGs in a way that
  25  * minimizes state space overhead. This was previously implemented in various different places (ThreadInfo, FieldInstruction etc.)
  26  * and controlled by a number of "vm.por.*" properties. Strictly speaking, the default implementation does not do classic partial
  27  * order reduction, it merely tries to reduce states associated with shared objects based on information that was collected by
  28  * previous execution. All configuration therefore is now done through "vm.shared.*" properties that are loaded in
  29  * SharednessPolicy implementations.
  30  *
  31  * The interface of this class, which is used by field and array element accessors (GETx, PUTx, xASTORE, xALOAD, Field
  32  * reflection), revolves around two concepts:
  33  *
  34  * (1) OBJECT SHAREDNESS - this is supposed to be precise, i.e. a property associated with ElementInfo instances that is set if
  35  * such an instance is in fact used by two different threads. As such, it has to be updated from the respective accessors (e.g.
  36  * GETx, PUTx). Detecting sharedness is the responsibility of the SharednessPolicy, storing it is done by means of ElementInfo
  37  * flags (which could also be set explicitly by listeners or peers).
  38  *
  39  * Once an object is marked as shared, respective field and element access operations can lead to races and hence it has to be
  40  * determined if a CG should be registered to re-execute such instructions. In order to minimize superfluous states, the default
  41  * policies filter out a number of access specific conditions such as immutable objects, and access point state such as number of
  42  * runnable threads and especially LOCK PROTECTION (which should normally happen for well designed concurrent programs). Detecting
  43  * lock protection is field specific and is done by keeping track of (intersections of) lock sets held by the accessing thread.
  44  * The corresponding FieldLockInfo objects are stored in the respective ElementInfo. The default FieldLockInfo is semi-conservative
  45  * - even if there is a non-empty lock set it treats the access as unprotected for a certain number of times. If the set becomes
  46  * empty the object/field is permanently marked as unprotected. If the threshold is reached with a non-empty set, the object/field
  47  * is henceforth treated as protected (a warning is issued should the lock set subsequently become empty).  *
  48  * If the access operation passes all filters, the SharednessPolicy registers a CG, i.e. the respective operation is re-executed
  49  * after performing a scheduling choice. Semantic actions (pushing operand values, changing field values) is done in the bottom
  50  * half of such operations. However, this can lead to cases in which sharedness is not detected due to non-overlapping lifetimes
  51  * of accessing threads. Note this does not mean that there is only one live thread at a time, only that threads don't have a CG
  52  * within their overlapping lifetime that would expose the race. This can lead to missed paths/errors.
  53  *
  54  * (2) OBJECT EXPOSURE - is a conservative measure to avoid such missed paths. It is used to introduce additional CGs when a
  55  * reference to an unshared object gets stored in a shared object, i.e. it is conceptually related to the object whose reference
  56  * gets stored (i.e. the field value), not to the object that holds the field. Exposure CGs are conservative since at this point
  57  * JPF only knows that the exposed object /could/ become shared in the future, not that it will. There are various different
  58  * degrees of conservatism that can be employed (transitive, only first object etc.), but exposure CGs can be a major contributor
  59  * to state explosion and hence should be minimized. Exposure CGs should break /after/ the semantic action (e.g. field
  60  * assignment), so that it becomes visible to other threads. This leads to a tricky problem that the bottom half of related
  61  * accessors has to determine if the semantic action already took place (exposure CGs) or not (sharedness CG). The action is not
  62  * allowed to be re-executed in the bottom half since this could change the SUT program behavior. In order to determine execution
  63  * state, implementation mechanisms have to be aware of that there can be any number of transitions between the top and bottom
  64  * half, i.e. cannot rely on the current CG in the bottom half execution. Conceptually, the execution state is a StackFrame
  65  * attribute.
  66  *
  67  * Note that exposure CGs are not mandatory. Concrete SharednessPolicy implementations can either ignore them in bug finding mode,
  68  * or can replace them by means of re-execution.
  69  *
  70  * Concrete SharednessPolicy implementations fall within a spectrum that is marked by two extremes: SEARCH GLOBAL and PATH LOCAL
  71  * behavior. Search global policies are mostly for bug finding and keep sharedness, lock protection and exposure information from
  72  * previously executed paths. This has two implications: (a) the search policy / execution order matters (e.g. leading to
  73  * different results when randomizing choice selection), (b) path replay based on CG traces can lead to different results (e.g.
  74  * not showing errors found in a previous search).
  75  *
  76  * The opposite mode is path local behavior, i.e. no sharednes/protection/exposure information from previous execution paths is
  77  * used. This should yield the same results for the same path, no matter of execution history. This mode requires the use of
  78  * persistent data structures for sharedness, lock info and exposure, and hence can be significantly more expensive. However, it
  79  * is required to guarantee path reply that preserves outcome.
  80  *
  81  * Although the two standard policy implementations (GlobalSharednessPolicy and PathSharednessPolicy) correspond to static
  82  * incarnations of these extremes, it should be noted that the SharednessPolicy interface strives to accommodate mixed and dynamic
  83  * modes, especially controlling re-execution with adaptive behavior. A primary use for this could be to avoid exposure CGs until
  84  * additional information becomes available that indicates object sharedness (e.g. non-overlapping thread access), then backtrack
  85  * to a common ancestor state and re-execute with added exposure CGs for the respective object/field.
  86  *
  87  * The motivation for this flexibility and the related implementation complexity/cost is that race detection based on field/array
  88  * access is a major contributor to state explosion. In many cases, suitable optimizations make the difference between running
  89  * into search constraints or finishing the search.
  90  */
  91 public interface SharednessPolicy {
  92
  93   /**
  94    * per application / SystemClassLoaderInfo specific initialization of this policy
  95    */
  96   void initializeSharednessPolicy (VM vm, ApplicationContext appCtx);
  97
  98   /**
  99    * initializeSharednessPolicy object specific sharedness data
 100    */
 101   void initializeObjectSharedness (ThreadInfo allocThread, DynamicElementInfo ei);
 102
 103   /**
 104    * initializeSharednessPolicy class specific sharedness data
 105    */
 106   void initializeClassSharedness (ThreadInfo allocThread, StaticElementInfo ei);
 107
 108
 109   boolean canHaveSharedObjectCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi);
 110   ElementInfo updateObjectSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi);
 111   boolean setsSharedObjectCG  (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi);
 112
 113   boolean canHaveSharedClassCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi);
 114   ElementInfo updateClassSharedness (ThreadInfo ti, ElementInfo ei, FieldInfo fi);
 115   boolean setsSharedClassCG  (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi);
 116
 117   boolean canHaveSharedArrayCG (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int idx);
 118   ElementInfo updateArraySharedness (ThreadInfo ti, ElementInfo eiArray, int idx);
 119   boolean setsSharedArrayCG  (ThreadInfo ti, Instruction insn, ElementInfo eiArray, int idx);
 120
 121   boolean setsSharedObjectExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed);
 122   boolean setsSharedClassExposureCG (ThreadInfo ti, Instruction insn, ElementInfo eiFieldOwner, FieldInfo fi, ElementInfo eiExposed);
 123
 124
 125   /**
 126    * give policy a chance to clean up referencing ThreadInfoSets upon
 127    * thread termination
 128    */
 129   void cleanupThreadTermination(ThreadInfo ti);
 130 }