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:
020: package gov.nasa.jpf.tools;
021:
022: import java.util.ArrayList;
023: import java.util.HashMap;
024: import java.util.Iterator;
025: import java.util.LinkedList;
026: import java.util.Stack;
027:
028: import gov.nasa.jpf.PropertyListenerAdapter;
029: import gov.nasa.jpf.Search;
030: import gov.nasa.jpf.VM;
031: import gov.nasa.jpf.Config;
032: import gov.nasa.jpf.jvm.ElementInfo;
033: import gov.nasa.jpf.jvm.JVM;
034: import gov.nasa.jpf.jvm.ThreadInfo;
035: import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
036: import gov.nasa.jpf.jvm.bytecode.InstanceFieldInstruction;
037: import gov.nasa.jpf.jvm.bytecode.Instruction;
038: import gov.nasa.jpf.jvm.bytecode.PUTFIELD;
039: import gov.nasa.jpf.jvm.bytecode.PUTSTATIC;
040: import gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction;
041:
042: /**
043: * Simple field access race detector example
044: *
045: * This implemenation so far doesn't deal with synchronization via signals, it
046: * only checks if the lockset intersections of reads and writes from different
047: * threads get empty. A more sophisticated version would check if the two
048: * suspicious access operations (one read, one write) will also happen in reverse
049: * order (that's the beauty of using this inside a model checker)
050: */
051: public class RaceDetector extends PropertyListenerAdapter {
052:
053: /*** helper classes ***************************************************************/
054:
055: static class FieldAccess {
056: ThreadInfo ti;
057: Object[] locksHeld; // the ones we have during this operation (not really required)
058: Object[] lockCandidates; // the intersection for all prev operations
059: FieldInstruction finsn;
060:
061: FieldAccess prev;
062:
063: FieldAccess(ThreadInfo ti, FieldInstruction finsn) {
064: this .ti = ti;
065: this .finsn = finsn;
066:
067: // we have to do some sort of cloning, since the lockSet and the
068: // ElementInfos in it are going to be changed by JPF
069: LinkedList lockSet = ti.getLockedObjects();
070: locksHeld = new Object[lockSet.size()];
071: if (locksHeld.length > 0) {
072: Iterator it = lockSet.iterator();
073: for (int i = 0; it.hasNext(); i++) {
074: locksHeld[i] = ((ElementInfo) it.next()).toString(); // <2do> - that's lame, but convenient
075: }
076: }
077:
078: // <2do> we should also hash the threads callstack here
079: }
080:
081: Object[] intersect(Object[] a, Object[] b) {
082: ArrayList list = new ArrayList(a.length);
083: for (int i = 0; i < a.length; i++) {
084: for (int j = 0; j < b.length; j++) {
085: if (a[i].equals(b[j])) {
086: list.add(a[i]);
087: break;
088: }
089: }
090: }
091: return (list.size() == a.length) ? a : list.toArray();
092: }
093:
094: void updateLockCandidates() {
095: if (prev == null) {
096: lockCandidates = locksHeld;
097: } else {
098: lockCandidates = intersect(locksHeld,
099: prev.lockCandidates);
100: }
101: }
102:
103: boolean hasLockCandidates() {
104: return (lockCandidates.length > 0);
105: }
106:
107: boolean isWriteAccess() {
108: return ((finsn instanceof PUTFIELD) || (finsn instanceof PUTSTATIC));
109: }
110:
111: FieldAccess getConflict() {
112: boolean isWrite = isWriteAccess();
113:
114: for (FieldAccess c = prev; c != null; c = c.prev) {
115: if ((c.ti != ti) && (isWrite != c.isWriteAccess())) {
116: return c;
117: }
118: }
119: return null; // no potential conflict found
120: }
121:
122: public boolean equals(Object other) {
123: if (other instanceof FieldAccess) {
124: FieldAccess fa = (FieldAccess) other;
125: if (ti != fa.ti)
126: return false;
127: if (finsn != fa.finsn)
128: return false;
129: // <2do> we should also check for same callstack, but that's a detail we leave out for now
130:
131: return true;
132: }
133: return false;
134: }
135:
136: String describe() {
137: String s = isWriteAccess() ? "write" : "read";
138: s += " from thread: \"";
139: s += ti.getName();
140: s += "\", holding locks {";
141: for (int i = 0; i < locksHeld.length; i++) {
142: if (i > 0)
143: s += ',';
144: s += locksHeld[i];
145: }
146: s += "} in ";
147: s += finsn.getSourceLocation();
148: return s;
149: }
150: }
151:
152: static class FieldAccessSequence {
153: String id;
154: FieldAccess lastAccess;
155:
156: FieldAccessSequence(String id) {
157: this .id = id;
158: }
159:
160: void addAccess(FieldAccess fa) {
161: fa.prev = lastAccess;
162: lastAccess = fa;
163: fa.updateLockCandidates();
164: }
165:
166: void purgeLastAccess() {
167: lastAccess = lastAccess.prev;
168: }
169:
170: }
171:
172: /*** private fields and methods ****************************************/
173: HashMap fields = new HashMap();
174:
175: Stack transitions = new Stack(); // the stack of FieldStateChanges
176: ArrayList pendingChanges; // changed FieldStates during the last transition
177:
178: FieldAccessSequence raceField; // if this becomes non-null, we have a race and terminate
179:
180: ArrayList raceAccess1 = new ArrayList(); // to store our potential race candidate pairs in
181: ArrayList raceAccess2 = new ArrayList(); // case of verifyCyle=true
182:
183: String[] watchFields; // list of regular expressions to match class/field names
184: boolean terminate; // terminate search when we found a (potential) race
185: boolean verifyCycle; // don't report potentials, go on until encountering
186:
187: // the suspicious insns in both orders
188:
189: public RaceDetector(Config config) {
190: watchFields = config.getStringArray("race.fields");
191: terminate = config.getBoolean("race.terminate", true);
192: verifyCycle = config.getBoolean("race.verify_cycle", false);
193: }
194:
195: boolean isWatchedField(FieldInstruction finsn) {
196: if (watchFields == null) {
197: return true;
198: }
199:
200: String fname = finsn.getVariableId();
201:
202: for (int i = 0; i < watchFields.length; i++) {
203: if (fname.matches(watchFields[i])) {
204: return true;
205: }
206: }
207:
208: return false;
209: }
210:
211: /*** GenericProperty **************************************************/
212:
213: public boolean check(VM vm, Object arg) {
214: return (raceField == null);
215: }
216:
217: public String getErrorMessage() {
218: return ("potential field race: " + raceField.id);
219: }
220:
221: /*** SearchListener ****************************************************/
222:
223: public void stateAdvanced(Search search) {
224: transitions.push(pendingChanges);
225: pendingChanges = null;
226: }
227:
228: public void stateBacktracked(Search search) {
229: ArrayList fops = (ArrayList) transitions.pop();
230: if (fops != null) {
231: for (Iterator it = fops.iterator(); it.hasNext();) {
232: FieldAccessSequence fs = (FieldAccessSequence) it
233: .next();
234: fs.purgeLastAccess();
235: }
236: }
237: }
238:
239: /*** VMListener *******************************************************/
240:
241: public void instructionExecuted(VM vm) {
242: JVM jvm = (JVM) vm;
243: Instruction insn = jvm.getLastInstruction();
244:
245: if (insn instanceof FieldInstruction) {
246: ThreadInfo ti = jvm.getLastThreadInfo();
247: FieldInstruction finsn = (FieldInstruction) insn;
248: String id = null;
249:
250: if (raceField != null) { // we only report the first one
251: return;
252: }
253:
254: if (ti.hasOtherRunnables() && isWatchedField(finsn)) {
255: if (insn instanceof StaticFieldInstruction) { // that's shared per se
256: id = finsn.getVariableId();
257: } else { // instance field, check if the object is shared
258: ElementInfo ei = ((InstanceFieldInstruction) insn)
259: .getLastElementInfo();
260: if (ei.isShared()) {
261: id = finsn.getId(ei);
262: }
263: }
264:
265: if (id != null) {
266: FieldAccessSequence fs = (FieldAccessSequence) fields
267: .get(id);
268: if (fs == null) { // first time
269: fs = new FieldAccessSequence(id);
270: fields.put(id, fs);
271: }
272:
273: FieldAccess fa = new FieldAccess(ti, finsn);
274: fs.addAccess(fa);
275:
276: if (pendingChanges == null) {
277: pendingChanges = new ArrayList(5);
278: }
279: pendingChanges.add(fs);
280:
281: if (!fa.hasLockCandidates()) {
282: FieldAccess conflict = fa.getConflict();
283: if (conflict != null) {
284: if (verifyCycle) {
285: int idx = raceAccess1.indexOf(conflict);
286:
287: if ((idx >= 0)
288: && (fa.equals(raceAccess2
289: .get(idx)))) {
290: // this is the second time we encounter the pair, this time in reverse order -> report
291: if (terminate) {
292: raceField = fs;
293: }
294: System.err
295: .println("race detected (access occurred in both orders): "
296: + fs.id);
297: System.err.println("\t"
298: + fa.describe());
299: System.err.println("\t"
300: + conflict.describe());
301: } else {
302: // first time we see this pair -> store
303: raceAccess1.add(fa);
304: raceAccess2.add(conflict);
305: }
306: } else {
307: if (terminate) {
308: raceField = fs;
309: }
310: System.err
311: .println("potential race detected: "
312: + fs.id);
313: System.err
314: .println("\t" + fa.describe());
315: System.err.println("\t"
316: + conflict.describe());
317: }
318: }
319: }
320: }
321: }
322: }
323: }
324: }
|