2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.vm;
21 import gov.nasa.jpf.Config;
24 * a SharednessPolicy implementation that only computes and keeps sharedness
25 * along the same path, i.e. not search global.
27 * This is the policy that should be used to create traces that can be replayed.
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.
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').
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.
58 public class PathSharednessPolicy extends GenericSharednessPolicy {
60 public PathSharednessPolicy (Config config){
65 public void initializeObjectSharedness (ThreadInfo allocThread, DynamicElementInfo ei) {
66 ei.setReferencingThreads( new PersistentTidSet(allocThread));
70 public void initializeClassSharedness (ThreadInfo allocThread, StaticElementInfo ei) {
71 ei.setReferencingThreads( new PersistentTidSet(allocThread));
72 ei.setExposed(); // static fields are per se exposed
76 protected FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi){
77 int[] lockRefs = ti.getLockedObjectReferences();
78 switch (lockRefs.length){
80 return FieldLockInfo.getEmptyFieldLockInfo();
82 return new PersistentSingleLockThresholdFli(ti, lockRefs[0], lockThreshold);
84 return new PersistentLockSetThresholdFli(ti, lockRefs, lockThreshold);
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();