Mercurial > hg > Members > kono > jpf-core
comparison src/main/gov/nasa/jpf/vm/SharednessPolicy.java @ 0:61d41facf527
initial v8 import (history reset)
author | Peter Mehlitz <Peter.C.Mehlitz@nasa.gov> |
---|---|
date | Fri, 23 Jan 2015 10:14:01 -0800 |
parents | |
children |
comparison
equal
deleted
inserted
replaced
-1:000000000000 | 0:61d41facf527 |
---|---|
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 } |