src/main/gov/nasa/jpf/listener/PreciseRaceDetector.java

   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
  19 package gov.nasa.jpf.listener;
  20
  21 import gov.nasa.jpf.Config;
  22 import gov.nasa.jpf.PropertyListenerAdapter;
  23 import gov.nasa.jpf.vm.bytecode.ArrayElementInstruction;
  24 import gov.nasa.jpf.vm.bytecode.FieldInstruction;
  25 import gov.nasa.jpf.search.Search;
  26 import gov.nasa.jpf.util.StringSetMatcher;
  27 import gov.nasa.jpf.vm.ChoiceGenerator;
  28 import gov.nasa.jpf.vm.ElementInfo;
  29 import gov.nasa.jpf.vm.FieldInfo;
  30 import gov.nasa.jpf.vm.Instruction;
  31 import gov.nasa.jpf.vm.VM;
  32 import gov.nasa.jpf.vm.MethodInfo;
  33 import gov.nasa.jpf.vm.bytecode.ReadOrWriteInstruction;
  34 import gov.nasa.jpf.vm.ThreadInfo;
  35 import gov.nasa.jpf.vm.choice.ThreadChoiceFromSet;
  36
  37 import java.io.PrintWriter;
  38 import java.io.StringWriter;
  39
  40 /**
  41  * This is a Race Detection Algorithm that is precise in its calculation of races, i.e. no false warnings.
  42  * It exploits the fact that every thread choice selection point could be due to a possible race. It just runs
  43  * through all the thread choices and checks whether there are more than one thread trying to read & write to the
  44  * same field of an object.
  45  *
  46  * Current limitation is that it is only sound, i.e. will not miss a race, if the sync-detection is switched off
  47  * during model checking. This is due to the fact that the sync-detection guesses that an acess is lock-protected
  48  * when it in reality might not be.
  49  *
  50  * The listener also checks races for array elements, but in order to do so you have to set
  51  * "cg.threads.break_arrays=true" (note that it is false by default because this can cause serious state
  52  * explosion)
  53  *
  54  * This algorithm came out of a discussion with Franck van Breugel and Sergey Kulikov from the University of York.
  55  * All credits for it goes to Franck and Sergey, all the bugs are mine.
  56  *
  57  * NOTE - the PreciseRaceDetector is machine type agnostic
  58  *
  59  * Author: Willem Visser
  60  *
  61  */
  62
  63 public class PreciseRaceDetector extends PropertyListenerAdapter {
  64
  65   static class Race {
  66     Race prev;   // linked list
  67
  68     ThreadInfo ti1, ti2;
  69     ReadOrWriteInstruction insn1, insn2;
  70     ElementInfo ei;
  71     boolean isRead1, isRead2;
  72
  73     boolean isRace() {
  74       return insn2 != null && ti1 != null && ti2 != null && ( ! ti1.equals(ti2) );
  75     }
  76
  77     void printOn(PrintWriter pw){
  78       pw.print("  ");
  79       pw.print( ti1.getName());
  80       pw.print(" at ");
  81       pw.println(insn1.getSourceLocation());
  82       String line = insn1.getSourceLine();
  83       if (line != null){
  84         pw.print("\t\t\"" + line.trim());
  85       }
  86       pw.print("\"  ");
  87       pw.print( insn1.isRead() ? "READ:  " : "WRITE: ");
  88       pw.println(insn1);
  89
  90       if (insn2 != null){
  91         pw.print("  ");
  92         pw.print(ti2.getName());
  93         pw.print(" at ");
  94         pw.println(insn2.getSourceLocation());
  95         line = insn2.getSourceLine();
  96         if (line != null){
  97           pw.print("\t\t\"" + line.trim());
  98         }
  99         pw.print("\"  ");
 100         pw.print( insn2.isRead() ? "READ:  " : "WRITE: ");
 101         pw.println(insn2);
 102       }
 103     }
 104   }
 105
 106   static class FieldRace extends Race {
 107     FieldInfo   fi;
 108
 109     static Race check (Race prev, ThreadInfo ti,  ReadOrWriteInstruction insn, ElementInfo ei, FieldInfo fi){
 110       for (Race r = prev; r != null; r = r.prev){
 111         if (r instanceof FieldRace){
 112           FieldRace fr = (FieldRace)r;
 113           if (fr.ei == ei && fr.fi == fi){
 114
 115             if (!((FieldInstruction)fr.insn1).isRead() || !((FieldInstruction)insn).isRead()){
 116               fr.ti2 = ti;
 117               fr.insn2 = insn;
 118               return fr;
 119             }
 120           }
 121         }
 122       }
 123
 124       FieldRace fr = new FieldRace();
 125       fr.ei = ei;
 126       fr.ti1 = ti;
 127       fr.insn1 = insn;
 128       fr.fi = fi;
 129       fr.prev = prev;
 130       return fr;
 131     }
 132
 133     @Override
 134         void printOn(PrintWriter pw){
 135       pw.print("race for field ");
 136       pw.print(ei);
 137       pw.print('.');
 138       pw.println(fi.getName());
 139
 140       super.printOn(pw);
 141     }
 142   }
 143
 144   static class ArrayElementRace extends Race {
 145     int idx;
 146
 147     static Race check (Race prev, ThreadInfo ti, ReadOrWriteInstruction insn, ElementInfo ei, int idx){
 148       for (Race r = prev; r != null; r = r.prev){
 149         if (r instanceof ArrayElementRace){
 150           ArrayElementRace ar = (ArrayElementRace)r;
 151           if (ar.ei == ei && ar.idx == idx){
 152             if (!((ArrayElementInstruction)ar.insn1).isRead() || !((ArrayElementInstruction)insn).isRead()){
 153               ar.ti2 = ti;
 154               ar.insn2 = insn;
 155               return ar;
 156             }
 157           }
 158         }
 159       }
 160
 161       ArrayElementRace ar = new ArrayElementRace();
 162       ar.ei = ei;
 163       ar.ti1 = ti;
 164       ar.insn1 = insn;
 165       ar.idx = idx;
 166       ar.prev = prev;
 167       return ar;
 168     }
 169
 170     @Override
 171         void printOn(PrintWriter pw){
 172       pw.print("race for array element ");
 173       pw.print(ei);
 174       pw.print('[');
 175       pw.print(idx);
 176       pw.println(']');
 177
 178       super.printOn(pw);
 179     }
 180   }
 181
 182   // this is where we store if we detect one
 183   protected Race race;
 184
 185
 186   // our matchers to determine which code we have to check
 187   protected StringSetMatcher includes = null; //  means all
 188   protected StringSetMatcher excludes = null; //  means none
 189
 190
 191   public PreciseRaceDetector (Config conf) {
 192     includes = StringSetMatcher.getNonEmpty(conf.getStringArray("race.include"));
 193     excludes = StringSetMatcher.getNonEmpty(conf.getStringArray("race.exclude"));
 194   }
 195
 196   @Override
 197   public boolean check(Search search, VM vm) {
 198     return (race == null);
 199   }
 200
 201   @Override
 202   public void reset() {
 203     race = null;
 204   }
 205
 206
 207   @Override
 208   public String getErrorMessage () {
 209     if (race != null){
 210       StringWriter sw = new StringWriter();
 211       PrintWriter pw = new PrintWriter(sw);
 212       race.printOn(pw);
 213       pw.flush();
 214       return sw.toString();
 215
 216     } else {
 217       return null;
 218     }
 219   }
 220
 221   protected boolean checkRace (ThreadInfo[] threads){
 222     Race candidate = null;
 223
 224     for (int i = 0; i < threads.length; i++) {
 225       ThreadInfo ti = threads[i];
 226       Instruction insn = ti.getPC();
 227       MethodInfo mi = insn.getMethodInfo();
 228
 229       if (StringSetMatcher.isMatch(mi.getBaseName(), includes, excludes)) {
 230         if (insn instanceof FieldInstruction) {
 231           FieldInstruction finsn = (FieldInstruction) insn;
 232           FieldInfo fi = finsn.getFieldInfo();
 233           ElementInfo ei = finsn.peekElementInfo(ti);
 234
 235           candidate = FieldRace.check(candidate, ti, finsn, ei, fi);
 236
 237         } else if (insn instanceof ArrayElementInstruction) {
 238           ArrayElementInstruction ainsn = (ArrayElementInstruction) insn;
 239           ElementInfo ei = ainsn.peekArrayElementInfo(ti);
 240
 241           // these insns have been through their top half since they created CGs, but they haven't
 242           // removed the operands from the stack
 243           int idx = ainsn.peekIndex(ti);
 244
 245           candidate = ArrayElementRace.check(candidate, ti, ainsn, ei, idx);
 246         }
 247       }
 248
 249       if (candidate != null && candidate.isRace()){
 250         race = candidate;
 251         return true;
 252       }
 253     }
 254
 255     return false;
 256   }
 257
 258
 259   //----------- our VMListener interface
 260
 261   // All we rely on here is that the scheduler breaks transitions at all
 262   // insns that could be races. We then just have to look at all currently
 263   // executed insns and don't rely on any past-exec info, PROVIDED that we only
 264   // use execution parameters (index or reference values) that are retrieved
 265   // from the operand stack, and not cached in the insn from a previous exec
 266   // (all the insns we look at are pre-exec, i.e. don't have their caches
 267   // updated yet)
 268   @Override
 269   public void choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG) {
 270
 271     if (newCG instanceof ThreadChoiceFromSet) {
 272       ThreadInfo[] threads = ((ThreadChoiceFromSet)newCG).getAllThreadChoices();
 273       checkRace(threads);
 274     }
 275   }
 276
 277   @Override
 278   public void executeInstruction (VM vm, ThreadInfo ti, Instruction insnToExecute) {
 279     if (race != null) {
 280       // we're done, report as quickly as possible
 281       //ti.skipInstruction();
 282       ti.breakTransition("dataRace");
 283     }
 284   }
 285
 286 }