001: //
002: // Copyright (C) 2005 United States Government as represented by the
003: // Administrator of the National Aeronautics and Space Administration
004: // (NASA). All Rights Reserved.
005: //
006: // This software is distributed under the NASA Open Source Agreement
007: // (NOSA), version 1.3. The NOSA has been approved by the Open Source
008: // Initiative. See the file NOSA-1.3-JPF at the top of the distribution
009: // directory tree for the complete NOSA document.
010: //
011: // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
012: // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
013: // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
014: // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
015: // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
016: // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
017: // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
018: //
019: package gov.nasa.jpf.jvm;
020:
021: import java.util.List;
022: import gov.nasa.jpf.util.Debug;
023: import java.util.BitSet;
024:
025: /**
026: * a FieldLockSet implementation with the following strategy
027: * - at each check, store the intersection of the current threads lock set
028: * with the previous field lock set
029: * - if the access was checked less than CHECK_THRESHOLD times, report the
030: * field as unprotected
031: * - if the field lock set doesn't become empty after CHECK_THRESHOLD, report
032: * the field as protected
033: *
034: * - as an optimization, raise the check level above the threshold if we
035: * have a good probability that a current lock is a protection lock for this
036: * field
037: */
038:
039: public class StatisticFieldLockInfo extends FieldLockInfo {
040: final static int CHECK_THRESHOLD = 5;
041:
042: int[] lset;
043: int checkLevel;
044:
045: // just a debugging tool
046: static String printLocks(int[] lockSet) {
047: DynamicArea heap = DynamicArea.getHeap();
048:
049: if ((lockSet == null) || (lockSet.length == 0)) {
050: return "{}";
051: } else {
052: StringBuffer sb = new StringBuffer();
053: sb.append("{");
054: for (int i = 0; i < lockSet.length;) {
055: int ref = lockSet[i];
056: if (ref != -1) {
057: ElementInfo ei = heap.get(ref);
058: if (ei != null) {
059: sb.append(ei);
060: } else {
061: sb.append("?@");
062: sb.append(lockSet[i]);
063: }
064: }
065: i++;
066: if (i < lockSet.length)
067: sb.append(',');
068: }
069: sb.append("}");
070: return sb.toString();
071: }
072: }
073:
074: void lockAssumptionFailed(ElementInfo ei, FieldInfo fi,
075: ThreadInfo ti) {
076: String src = ti.getMethod().getClassInfo().getSourceFileName();
077: int line = ti.getLine();
078:
079: Debug.println(Debug.ERROR,
080: "MESSAGE: unprotected field access of: " + ei + "."
081: + fi.getName() + " in thread:" + " \""
082: + ti.getName() + "\" " + src + ":" + line);
083: Debug.println(Debug.ERROR,
084: " sync-detection assumed to be protected by: "
085: + printLocks(lset));
086: Debug.println(Debug.ERROR, " found to be protected by: "
087: + printLocks(ti.getLockedObjectReferences()));
088: Debug.println(Debug.ERROR,
089: " >>> re-run without '-sync-detection' <<<");
090: }
091:
092: /**
093: * check if the current thread lockset contains a lock with a high probability
094: * that it is a protection lock for this field. We need this to avoid
095: * state explosion due to the number of fields to check. Note that we don't
096: * necessarily have to answer/decide which one is the best match in case of
097: * several candidates (if we don't use this to reduce to StatisticFieldLockInfo1)
098: *
099: * For instance fields, this would be a lock with a distance <= 1.
100: * For static fields, the corresponding class object is a good candidate.
101: */
102: static ElementInfo strongProtectionCandidate(ElementInfo ei,
103: FieldInfo fi, ThreadInfo ti) {
104: List currentLocks = ti.getLockedObjects();
105: int n = currentLocks.size();
106:
107: if (fi.isStatic()) { // static field, check for class object locking
108: ClassInfo ci = fi.getClassInfo();
109: int cref = ci.getClassObjectRef();
110:
111: for (int i = 0; i < n; i++) {
112: ElementInfo e = (ElementInfo) currentLocks.get(i); // the locked object
113: if (e.getIndex() == cref) {
114: Debug.print(Debug.MESSAGE, "sync-detection: ");
115: Debug.print(Debug.MESSAGE, ei);
116: Debug.print(Debug.MESSAGE,
117: " assumed to be synced on class object: ");
118: Debug.println(Debug.MESSAGE, e);
119: return e;
120: }
121: }
122:
123: } else { // instance field, use lock distance as a heuristic
124: for (int i = 0; i < n; i++) {
125: ElementInfo e = (ElementInfo) currentLocks.get(i); // the locked object
126: int eidx = e.getIndex();
127:
128: // case 1: synchronization on field owner itself
129: if (ei == e) {
130: Debug.print(Debug.MESSAGE, "sync-detection: ");
131: Debug.print(Debug.MESSAGE, ei);
132: Debug.println(Debug.MESSAGE,
133: " assumed to be synced on itself");
134: return e;
135: }
136:
137: // case 2: synchronization on owner of object holding field (sync wrapper)
138: if (e.hasRefField(ei.getIndex())) {
139: Debug.print(Debug.MESSAGE, "sync-detection: ");
140: Debug.print(Debug.MESSAGE, ei);
141: Debug
142: .print(Debug.MESSAGE,
143: " assumed to be synced on object wrapper: ");
144: Debug.println(Debug.MESSAGE, e);
145: return e;
146: }
147:
148: // case 3: synchronization on sibling field that is a private lock object
149: if (ei.hasRefField(eidx)) {
150: Debug.print(Debug.MESSAGE, "sync-detection: ");
151: Debug.print(Debug.MESSAGE, ei);
152: Debug.print(Debug.MESSAGE,
153: " assumed to be synced on sibling: ");
154: Debug.println(Debug.MESSAGE, e);
155: return e;
156: }
157: }
158: }
159:
160: return null;
161: }
162:
163: public FieldLockInfo checkProtection(ElementInfo ei, FieldInfo fi,
164: ThreadInfo ti) {
165: List currentLocks = ti.getLockedObjects();
166: int n = currentLocks.size();
167:
168: checkLevel++;
169: if (checkLevel == 1) { // first time, not checked before
170: if (n == 0) {
171: //System.out.println("@ no lock active: " + ei);
172: return empty;
173: } else {
174: ElementInfo lcei = strongProtectionCandidate(ei, fi, ti);
175: if (lcei != null) {
176: //System.out.println("@ strong prot-lock candidate for: " + ei + " is: " + lcei);
177: // we could also turn it into a StaticFieldLockInfo1 here
178: checkLevel = CHECK_THRESHOLD;
179: }
180:
181: if (n == 1) {
182: // Ok, let's simplify this, no need to waste all the memory
183: return new StatisticFieldLockInfo1(ei, fi, ti,
184: checkLevel);
185: }
186:
187: lset = new int[n];
188: for (int i = 0; i < n; i++) {
189: ElementInfo lei = (ElementInfo) currentLocks.get(i);
190: lset[i] = lei.getIndex();
191: }
192: }
193:
194: } else { // already checked this before
195: if (n == 0) {
196: lockAssumptionFailed(ei, fi, ti);
197: return empty;
198: } else {
199: int i, j;
200: BitSet active = new BitSet(lset.length);
201:
202: for (i = 0; i < n; i++) {
203: ElementInfo lei = (ElementInfo) currentLocks.get(i);
204: int leidx = lei.getIndex();
205:
206: // unfortunately, we can't shortcut since we have to nullify all
207: // lock refs that are not in the current intersection (which has
208: // to be accumulative)
209: for (j = 0; j < lset.length; j++) {
210: if (lset[j] == leidx) {
211: active.set(j);
212: }
213: }
214:
215: int nActive = active.size();
216: if (nActive == 0) {
217: lockAssumptionFailed(ei, fi, ti);
218: return empty;
219: } else {
220: for (j = 0; j < lset.length; j++) {
221: if (!active.get(j)) {
222: lset[j] = -1;
223: }
224: }
225: }
226: }
227: }
228: }
229:
230: return this ;
231: }
232:
233: public boolean isProtected() {
234: //System.out.println("@ isProtected: " + (checkLevel >= CHECK_THRESHOLD));
235: return (checkLevel >= CHECK_THRESHOLD);
236: }
237: }
238:
239: /**
240: * private optimization for the trivial case of single locks. We definitely don't
241: * want to allocate int[] and long[] (BitSet) objects to store a single ref!
242: */
243: class StatisticFieldLockInfo1 extends FieldLockInfo {
244: int lock;
245: boolean active;
246: int checkLevel;
247:
248: StatisticFieldLockInfo1(ElementInfo ei, FieldInfo fi,
249: ThreadInfo ti, int nChecks) {
250: List currentLocks = ti.getLockedObjects();
251:
252: lock = ((ElementInfo) currentLocks.get(0)).getIndex();
253: active = true;
254: this .checkLevel = nChecks;
255: }
256:
257: void lockAssumptionFailed(ElementInfo ei, FieldInfo fi,
258: ThreadInfo ti) {
259: String src = ti.getMethod().getClassInfo().getSourceFileName();
260: int line = ti.getLine();
261:
262: Debug.println(Debug.ERROR,
263: "Warning: unprotected field access of: " + ei + "."
264: + fi.getName() + " in thread:" + " \""
265: + ti.getName() + "\" " + src + ":" + line);
266: Debug.println(Debug.ERROR,
267: " sync-detection assumed to be protected by: "
268: + DynamicArea.getHeap().get(lock));
269: Debug.println(Debug.ERROR, " found to be protected by: "
270: + StatisticFieldLockInfo.printLocks(ti
271: .getLockedObjectReferences()));
272: Debug.println(Debug.ERROR,
273: " >>> re-run without '-sync-detection' <<<");
274: }
275:
276: public FieldLockInfo checkProtection(ElementInfo ei, FieldInfo fi,
277: ThreadInfo ti) {
278: List currentLocks = ti.getLockedObjects();
279: int n = currentLocks.size();
280:
281: checkLevel++;
282: active = false;
283: for (int i = 0; i < n; i++) {
284: ElementInfo lei = (ElementInfo) currentLocks.get(i);
285: if (lei.getIndex() == lock) {
286: active = true;
287: break;
288: }
289: }
290:
291: if (!active) {
292: if (checkLevel > StatisticFieldLockInfo.CHECK_THRESHOLD) {
293: lockAssumptionFailed(ei, fi, ti);
294: }
295: return empty;
296: }
297:
298: return this ;
299: }
300:
301: public boolean isProtected() {
302: //System.out.println("@ isProtected1: " + (checkLevel >= StatisticFieldLockInfo.CHECK_THRESHOLD));
303: return (checkLevel >= StatisticFieldLockInfo.CHECK_THRESHOLD);
304: }
305: }
|