2 * Copyright (C) 2014, United States Government, as represented by the
3 * Administrator of the National Aeronautics and Space Administration.
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
10 * http://www.apache.org/licenses/LICENSE-2.0.
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.
19 package gov.nasa.jpf.listener;
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;
37 import java.io.PrintWriter;
38 import java.io.StringWriter;
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.
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.
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
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.
57 * NOTE - the PreciseRaceDetector is machine type agnostic
59 * Author: Willem Visser
63 public class PreciseRaceDetector extends PropertyListenerAdapter {
66 Race prev; // linked list
69 ReadOrWriteInstruction insn1, insn2;
71 boolean isRead1, isRead2;
74 return insn2 != null && ti1 != null && ti2 != null && ( ! ti1.equals(ti2) );
77 void printOn(PrintWriter pw){
79 pw.print( ti1.getName());
81 pw.println(insn1.getSourceLocation());
82 String line = insn1.getSourceLine();
84 pw.print("\t\t\"" + line.trim());
87 pw.print( insn1.isRead() ? "READ: " : "WRITE: ");
92 pw.print(ti2.getName());
94 pw.println(insn2.getSourceLocation());
95 line = insn2.getSourceLine();
97 pw.print("\t\t\"" + line.trim());
100 pw.print( insn2.isRead() ? "READ: " : "WRITE: ");
106 static class FieldRace extends Race {
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){
115 if (!((FieldInstruction)fr.insn1).isRead() || !((FieldInstruction)insn).isRead()){
124 FieldRace fr = new FieldRace();
134 void printOn(PrintWriter pw){
135 pw.print("race for field ");
138 pw.println(fi.getName());
144 static class ArrayElementRace extends Race {
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()){
161 ArrayElementRace ar = new ArrayElementRace();
171 void printOn(PrintWriter pw){
172 pw.print("race for array element ");
182 // this is where we store if we detect one
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
191 public PreciseRaceDetector (Config conf) {
192 includes = StringSetMatcher.getNonEmpty(conf.getStringArray("race.include"));
193 excludes = StringSetMatcher.getNonEmpty(conf.getStringArray("race.exclude"));
197 public boolean check(Search search, VM vm) {
198 return (race == null);
202 public void reset() {
208 public String getErrorMessage () {
210 StringWriter sw = new StringWriter();
211 PrintWriter pw = new PrintWriter(sw);
214 return sw.toString();
221 protected boolean checkRace (ThreadInfo[] threads){
222 Race candidate = null;
224 for (int i = 0; i < threads.length; i++) {
225 ThreadInfo ti = threads[i];
226 Instruction insn = ti.getPC();
227 MethodInfo mi = insn.getMethodInfo();
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);
235 candidate = FieldRace.check(candidate, ti, finsn, ei, fi);
237 } else if (insn instanceof ArrayElementInstruction) {
238 ArrayElementInstruction ainsn = (ArrayElementInstruction) insn;
239 ElementInfo ei = ainsn.peekArrayElementInfo(ti);
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);
245 candidate = ArrayElementRace.check(candidate, ti, ainsn, ei, idx);
249 if (candidate != null && candidate.isRace()){
259 //----------- our VMListener interface
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
269 public void choiceGeneratorSet(VM vm, ChoiceGenerator<?> newCG) {
271 if (newCG instanceof ThreadChoiceFromSet) {
272 ThreadInfo[] threads = ((ThreadChoiceFromSet)newCG).getAllThreadChoices();
278 public void executeInstruction (VM vm, ThreadInfo ti, Instruction insnToExecute) {
280 // we're done, report as quickly as possible
281 //ti.skipInstruction();
282 ti.breakTransition("dataRace");