comparison src/main/gov/nasa/jpf/vm/GlobalSharednessPolicy.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 import gov.nasa.jpf.Config;
21 import gov.nasa.jpf.util.SparseObjVector;
22
23 /**
24 * a SharedObjectPolicy that uses search global ThreadInfoSets and FieldLockInfos,
25 * i.e. we remember thread access of all previously executed paths.
26 *
27 * Use this policy for bug finding modes that don't have to create replay-able traces.
28 *
29 * Note that this policy requires search global object ids (SGOID), i.e. only works
30 * with Heap implementations providing SGOIDs
31 */
32
33 public class GlobalSharednessPolicy extends GenericSharednessPolicy {
34 // our global caches
35 protected SparseObjVector<ThreadInfoSet> globalTisCache = new SparseObjVector<ThreadInfoSet>(1024);
36 protected SparseObjVector<FieldLockInfo> globalFliCache = new SparseObjVector<FieldLockInfo>(1024);
37
38
39 public GlobalSharednessPolicy (Config config){
40 super(config);
41 }
42
43 protected ThreadInfoSet getRegisteredThreadInfoSet (int key, ThreadInfo allocThread) {
44 ThreadInfoSet tis = globalTisCache.get(key);
45 if (tis == null) {
46 tis = new TidSet(allocThread);
47 globalTisCache.set(key, tis);
48 }
49
50 return tis;
51 }
52
53 protected FieldLockInfo getRegisteredFieldLockInfo (int key, ThreadInfo ti){
54 FieldLockInfo fli = globalFliCache.get(key);
55
56 if (fli == null){
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);
62 } else {
63 fli = new PersistentLockSetThresholdFli(ti, lockRefs, lockThreshold);
64 }
65
66 globalFliCache.set(key, fli);
67 }
68
69 return fli;
70 }
71
72 @Override
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
75 return true;
76 }
77
78 @Override
79 public void initializeObjectSharedness (ThreadInfo allocThread, DynamicElementInfo ei) {
80 ThreadInfoSet tis = getRegisteredThreadInfoSet(ei.getObjectRef(), allocThread);
81 ei.setReferencingThreads( tis);
82 }
83
84 @Override
85 public void initializeClassSharedness (ThreadInfo allocThread, StaticElementInfo ei) {
86 ThreadInfoSet tis;
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);
93 } else {
94 tis = getRegisteredThreadInfoSet(ref, allocThread);
95 }
96
97 ei.setReferencingThreads(tis);
98 ei.setExposed(); // static fields are per se exposed
99 }
100
101 @Override
102 protected FieldLockInfo createFieldLockInfo (ThreadInfo ti, ElementInfo ei, FieldInfo fi) {
103 int id;
104
105 if (ei instanceof StaticElementInfo){
106 id = ((StaticElementInfo)ei).getClassObjectRef();
107 if (id == MJIEnv.NULL){
108 return null;
109 }
110 } else {
111 id = ei.getObjectRef();
112 }
113
114 return getRegisteredFieldLockInfo( id, ti);
115 }
116 }