RaceDetector


1   //
2   // Copyright (C) 2005 United States Government as represented by the
3   // Administrator of the National Aeronautics and Space Administration
4   // (NASA).  All Rights Reserved.
5   // 
6   // This software is distributed under the NASA Open Source Agreement
7   // (NOSA), version 1.3.  The NOSA has been approved by the Open Source
8   // Initiative.  See the file NOSA-1.3-JPF at the top of the distribution
9   // directory tree for the complete NOSA document.
10  // 
11  // THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY OF ANY
12  // KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT
13  // LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO
14  // SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR
15  // A PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT
16  // THE SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT
17  // DOCUMENTATION, IF PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE.
18  //
19  
20  package gov.nasa.jpf.tools;
21  
22  import java.util.ArrayList  ;
23  import java.util.HashMap  ;
24  import java.util.Iterator  ;
25  import java.util.LinkedList  ;
26  import java.util.Stack  ;
27  
28  import gov.nasa.jpf.PropertyListenerAdapter;
29  import gov.nasa.jpf.Search;
30  import gov.nasa.jpf.VM;
31  import gov.nasa.jpf.Config;
32  import gov.nasa.jpf.jvm.ElementInfo;
33  import gov.nasa.jpf.jvm.JVM;
34  import gov.nasa.jpf.jvm.ThreadInfo;
35  import gov.nasa.jpf.jvm.bytecode.FieldInstruction;
36  import gov.nasa.jpf.jvm.bytecode.InstanceFieldInstruction;
37  import gov.nasa.jpf.jvm.bytecode.Instruction;
38  import gov.nasa.jpf.jvm.bytecode.PUTFIELD;
39  import gov.nasa.jpf.jvm.bytecode.PUTSTATIC;
40  import gov.nasa.jpf.jvm.bytecode.StaticFieldInstruction;
41  
42  /**
43   * Simple field access race detector example
44   * 
45   * This implemenation so far doesn't deal with synchronization via signals, it
46   * only checks if the lockset intersections of reads and writes from different
47   * threads get empty. A more sophisticated version would check if the two
48   * suspicious access operations (one read, one write) will also happen in reverse
49   * order (that's the beauty of using this inside a model checker)
50   */
51  public class RaceDetector extends PropertyListenerAdapter {
52    
53    
54    /*** helper classes ***************************************************************/
55    
56    static class FieldAccess {
57      ThreadInfo ti;
58      Object  [] locksHeld;          // the ones we have during this operation (not really required)
59      Object  [] lockCandidates;     // the intersection for all prev operations
60      FieldInstruction finsn;
61      
62      FieldAccess prev;
63      
64      FieldAccess (ThreadInfo ti, FieldInstruction finsn) {
65        this.ti = ti;
66        this.finsn = finsn;
67        
68        // we have to do some sort of cloning, since the lockSet and the 
69        // ElementInfos in it are going to be changed by JPF
70        LinkedList   lockSet = ti.getLockedObjects();
71        locksHeld = new Object  [lockSet.size()];
72        if (locksHeld.length > 0) {
73          Iterator   it = lockSet.iterator();
74          for (int i=0; it.hasNext(); i++) {
75            locksHeld[i] = ((ElementInfo)it.next()).toString(); // <2do> - that's lame, but convenient
76          }
77        }
78              
79        // <2do> we should also hash the threads callstack here
80      }
81    
82      Object  [] intersect (Object  [] a, Object  [] b) {
83        ArrayList   list = new ArrayList  (a.length);
84        for (int i=0; i<a.length; i++) {
85          for (int j=0; j<b.length; j++) {
86            if (a[i].equals(b[j])) {
87              list.add(a[i]);
88              break;
89            }
90          }
91        }
92        return (list.size() == a.length) ? a : list.toArray();
93      }
94      
95      void updateLockCandidates () {
96        if (prev == null) {
97          lockCandidates = locksHeld;
98        } else {
99          lockCandidates = intersect(locksHeld, 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) return false;
126         if (finsn != fa.finsn) return false;
127         // <2do> we should also check for same callstack, but that's a detail we leave out for now
128         
129         return true;
130       }
131       return false;
132     }
133     
134     String   describe () {
135       String   s = isWriteAccess() ? "write" : "read"; 
136       s += " from thread: \"";
137       s += ti.getName();
138       s += "\", holding locks {";
139       for (int i=0; i<locksHeld.length; i++) {
140         if (i>0) s += ',';
141         s += locksHeld[i];
142       }
143       s += "} in ";
144       s += finsn.getSourceLocation();
145       return s;
146     }
147   }
148   
149   static class FieldAccessSequence {
150     String   id;
151     FieldAccess lastAccess;
152     
153     FieldAccessSequence (String   id) {
154       this.id = id;
155     }
156       
157     void addAccess (FieldAccess fa) {
158       fa.prev = lastAccess;
159       lastAccess = fa;
160       fa.updateLockCandidates();
161     }
162     
163     void purgeLastAccess () {
164       lastAccess = lastAccess.prev;
165     }
166     
167   }
168     
169 
170   /*** private fields and methods ****************************************/
171   HashMap   fields = new HashMap  ();
172   
173   Stack   transitions = new Stack  ();   // the stack of FieldStateChanges
174   ArrayList   pendingChanges;          // changed FieldStates during the last transition
175 
176   FieldAccessSequence raceField;     // if this becomes non-null, we have a race and terminate
177   
178   ArrayList   raceAccess1 = new ArrayList  (); // to store our potential race candidate pairs in
179   ArrayList   raceAccess2 = new ArrayList  (); // case of verifyCyle=true
180   
181   String  [] watchFields;              // list of regular expressions to match class/field names
182   boolean terminate;                 // terminate search when we found a (potential) race
183   boolean verifyCycle;               // don't report potentials, go on until encountering
184                                      // the suspicious insns in both orders
185   
186   public RaceDetector (Config config) {
187     watchFields = config.getStringArray("race.fields");
188     terminate = config.getBoolean("race.terminate", true);
189     verifyCycle = config.getBoolean("race.verify_cycle", false);
190   }
191     
192   boolean isWatchedField (FieldInstruction finsn) {
193     if (watchFields == null) {
194       return true;
195     }
196     
197     String   fname = finsn.getVariableId();
198     
199     for (int i = 0; i<watchFields.length; i++) {
200       if (fname.matches(watchFields[i])){
201         return true;
202       }
203     }
204     
205     return false;
206   }
207     
208   
209   /*** GenericProperty **************************************************/
210   
211   public boolean check(VM vm, Object   arg) {
212     return (raceField == null);
213   }
214   
215   public String   getErrorMessage () {
216     return ("potential field race: " + raceField.id);
217   }
218   
219   /*** SearchListener ****************************************************/
220   
221   public void stateAdvanced(Search search) {
222     transitions.push(pendingChanges);
223     pendingChanges = null;
224   }
225 
226   public void stateBacktracked(Search search) {
227     ArrayList   fops = (ArrayList  ) transitions.pop();
228     if (fops != null) {
229       for (Iterator   it=fops.iterator(); it.hasNext(); ) {
230         FieldAccessSequence fs = (FieldAccessSequence) it.next();
231         fs.purgeLastAccess();
232       }      
233     }
234   }
235   
236   /*** VMListener *******************************************************/
237   
238   public void instructionExecuted(VM vm) {
239     JVM jvm = (JVM)vm;
240     Instruction insn = jvm.getLastInstruction();
241     
242     if (insn instanceof FieldInstruction) {
243       ThreadInfo ti = jvm.getLastThreadInfo();
244       FieldInstruction finsn = (FieldInstruction)insn;
245       String   id = null;
246 
247       if (raceField != null) { // we only report the first one
248         return;
249       }
250       
251       if (ti.hasOtherRunnables() && isWatchedField(finsn)) {
252         if (insn instanceof StaticFieldInstruction) { // that's shared per se
253           id = finsn.getVariableId();
254         } else { // instance field, check if the object is shared
255           ElementInfo ei = ((InstanceFieldInstruction)insn).getLastElementInfo();
256           if (ei.isShared()) {
257             id = finsn.getId(ei); 
258           }
259         }
260         
261         if (id != null) {
262           FieldAccessSequence fs = (FieldAccessSequence) fields.get(id);
263           if (fs == null) { // first time
264             fs = new FieldAccessSequence(id);
265             fields.put(id, fs);
266           }
267           
268           FieldAccess fa = new FieldAccess(ti, finsn);
269           fs.addAccess(fa);
270      
271           if (pendingChanges == null) {
272             pendingChanges = new ArrayList  (5);
273           }
274           pendingChanges.add(fs);
275           
276           if (!fa.hasLockCandidates()) {
277             FieldAccess conflict = fa.getConflict();            
278             if (conflict != null) {
279               if (verifyCycle) {
280                 int idx = raceAccess1.indexOf(conflict);
281                 
282                 if ((idx >=0) && (fa.equals(raceAccess2.get(idx)))) {
283                   // this is the second time we encounter the pair, this time in reverse order -> report
284                   if (terminate) {
285                     raceField = fs;
286                   }
287                   System.err.println("race detected (access occurred in both orders): " + fs.id);
288                   System.err.println("\t" + fa.describe());
289                   System.err.println("\t" + conflict.describe());                    
290                 } else {
291                   // first time we see this pair -> store
292                   raceAccess1.add(fa);
293                   raceAccess2.add(conflict);
294                 }
295               } else {
296                 if (terminate) {
297                   raceField = fs;
298                 }
299                 System.err.println("potential race detected: " + fs.id);
300                 System.err.println("\t" + fa.describe());
301                 System.err.println("\t" + conflict.describe());
302               }              
303             }
304           }
305         }
306       }
307     }
308   }  
309 }
310
A to Z: JavaDoc & Examples Daily Java News & Articles Open Source Projects Open Source Codes Free Computer Books Remove Frame
Popular Tags