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.
18 package gov.nasa.jpf.vm;
20 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.util.SparseObjVector;
24 * a SharedObjectPolicy that uses search global ThreadInfoSets and FieldLockInfos,
25 * i.e. we remember thread access of all previously executed paths.
27 * Use this policy for bug finding modes that don't have to create replay-able traces.
29 * Note that this policy requires search global object ids (SGOID), i.e. only works
30 * with Heap implementations providing SGOIDs
33 public class GlobalSharednessPolicy extends GenericSharednessPolicy {
35 protected SparseObjVector<ThreadInfoSet> globalTisCache = new SparseObjVector<ThreadInfoSet>(1024);
36 protected SparseObjVector<FieldLockInfo> globalFliCache = new SparseObjVector<FieldLockInfo>(1024);
39 public GlobalSharednessPolicy (Config config){
43 protected ThreadInfoSet getRegisteredThreadInfoSet (int key, ThreadInfo allocThread) {
44 ThreadInfoSet tis = globalTisCache.get(key);
46 tis = new TidSet(allocThread);
47 globalTisCache.set(key, tis);
53 protected FieldLockInfo getRegisteredFieldLockInfo (int key, ThreadInfo ti){
54 FieldLockInfo fli = globalFliCache.get(key);
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);
63 fli = new PersistentLockSetThresholdFli(ti, lockRefs, lockThreshold);
66 globalFliCache.set(key, fli);
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
79 public void initializeObjectSharedness (ThreadInfo allocThread, DynamicElementInfo ei) {
80 ThreadInfoSet tis = getRegisteredThreadInfoSet(ei.getObjectRef(), allocThread);
81 ei.setReferencingThreads( tis);
85 public void initializeClassSharedness (ThreadInfo allocThread, StaticElementInfo ei) {
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);
94 tis = getRegisteredThreadInfoSet(ref, allocThread);
97 ei.setReferencingThreads(tis);
98 ei.setExposed(); // static fields are per se exposed
102 protected FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
105 if (ei instanceof StaticElementInfo){
106 id = ((StaticElementInfo)ei).getClassObjectRef();
107 if (id == MJIEnv.NULL){
111 id = ei.getObjectRef();
114 return getRegisteredFieldLockInfo( id, ti);