src/main/gov/nasa/jpf/listener/DPORStateReducer.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 package gov.nasa.jpf.listener;
  19
  20 import gov.nasa.jpf.Config;
  21 import gov.nasa.jpf.JPF;
  22 import gov.nasa.jpf.ListenerAdapter;
  23 import gov.nasa.jpf.search.Search;
  24 import gov.nasa.jpf.jvm.bytecode.*;
  25 import gov.nasa.jpf.vm.*;
  26 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
  27 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
  28 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  29 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
  30
  31 import java.io.PrintWriter;
  32 import java.util.*;
  33
  34 // TODO: Fix for Groovy's model-checking
  35 // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
  36 /**
  37  * Simple tool to log state changes.
  38  *
  39  * This DPOR implementation is augmented by the algorithm presented in this SPIN paper:
  40  * http://spinroot.com/spin/symposia/ws08/spin2008_submission_33.pdf
  41  *
  42  * The algorithm is presented on page 11 of the paper. Basically, we create a graph G
  43  * (i.e., visible operation dependency graph)
  44  * that maps inter-related threads/sub-programs that trigger state changes.
  45  * The key to this approach is that we evaluate graph G in every iteration/recursion to
  46  * only update the backtrack sets of the threads/sub-programs that are reachable in graph G
  47  * from the currently running thread/sub-program.
  48  */
  49 public class DPORStateReducer extends ListenerAdapter {
  50
  51   // Information printout fields for verbose mode
  52   private boolean verboseMode;
  53   private boolean stateReductionMode;
  54   private final PrintWriter out;
  55   private String detail;
  56   private int depth;
  57   private int id;
  58   private Transition transition;
  59
  60   // DPOR-related fields
  61   private Integer[] choices;
  62   private Integer[] refChoices;
  63   private int choiceCounter;
  64   private int maxEventChoice;
  65   // Record CGs for backtracking points
  66   private List<IntChoiceFromSet> cgList;
  67   // Data structure to track the events seen by each state to track cycles (containing all events) for termination
  68   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
  69   private HashSet<Integer> justVisitedStates; // States just visited in the previous choice/event
  70   private HashSet<Integer> prevVisitedStates; // States visited in the previous execution
  71   private HashSet<Integer> currVisitedStates; // States being visited in the current execution
  72   // Data structure to analyze field Read/Write accesses
  73   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;
  74   private HashMap<Integer, HashSet<Integer>> conflictPairMap;
  75
  76   // Boolean states
  77   private boolean isBooleanCGFlipped;
  78
  79   public DPORStateReducer(Config config, JPF jpf) {
  80     verboseMode = config.getBoolean("printout_state_transition", false);
  81     stateReductionMode = config.getBoolean("activate_state_reduction", true);
  82     if (verboseMode) {
  83       out = new PrintWriter(System.out, true);
  84     } else {
  85       out = null;
  86     }
  87     // DPOR-related
  88     choices = null;
  89     refChoices = null;
  90     choiceCounter = 0;
  91     maxEventChoice = 0;
  92     cgList = new ArrayList<>();
  93     stateToEventMap = new HashMap<>();
  94     justVisitedStates = new HashSet<>();
  95     prevVisitedStates = new HashSet<>();
  96     currVisitedStates = new HashSet<>();
  97     readWriteFieldsMap = new HashMap<>();
  98     conflictPairMap = new HashMap<>();
  99     // Booleans
 100     isBooleanCGFlipped = false;
 101   }
 102
 103   @Override
 104   public void stateRestored(Search search) {
 105     if (verboseMode) {
 106       id = search.getStateId();
 107       depth = search.getDepth();
 108       transition = search.getTransition();
 109       detail = null;
 110       out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
 111               " and depth: " + depth + "\n");
 112     }
 113   }
 114
 115   @Override
 116   public void searchStarted(Search search) {
 117     if (verboseMode) {
 118       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
 119     }
 120   }
 121
 122   @Override
 123   public void stateAdvanced(Search search) {
 124     if (verboseMode) {
 125       id = search.getStateId();
 126       depth = search.getDepth();
 127       transition = search.getTransition();
 128       if (search.isNewState()) {
 129         detail = "new";
 130       } else {
 131         detail = "visited";
 132       }
 133
 134       if (search.isEndState()) {
 135         out.println("\n==> DEBUG: This is the last state!\n");
 136         detail += " end";
 137       }
 138       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
 139               " which is " + detail + " Transition: " + transition + "\n");
 140     }
 141     if (stateReductionMode) {
 142       updateStateInfo(search);
 143     }
 144   }
 145
 146   @Override
 147   public void stateBacktracked(Search search) {
 148     if (verboseMode) {
 149       id = search.getStateId();
 150       depth = search.getDepth();
 151       transition = search.getTransition();
 152       detail = null;
 153
 154       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
 155               " and depth: " + depth + "\n");
 156     }
 157     if (stateReductionMode) {
 158       updateStateInfo(search);
 159     }
 160   }
 161
 162   @Override
 163   public void searchFinished(Search search) {
 164     if (verboseMode) {
 165       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 166     }
 167   }
 168
 169   @Override
 170   public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
 171     if (stateReductionMode) {
 172       // Initialize with necessary information from the CG
 173       if (nextCG instanceof IntChoiceFromSet) {
 174         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
 175         // Check if CG has been initialized, otherwise initialize it
 176         Integer[] cgChoices = icsCG.getAllChoices();
 177         // Record the events (from choices)
 178         if (choices == null) {
 179           choices = cgChoices;
 180           // Make a copy of choices as reference
 181           refChoices = copyChoices(choices);
 182           // Record the max event choice (the last element of the choice array)
 183           maxEventChoice = choices[choices.length - 1];
 184         }
 185         // Use a modulo since choiceCounter is going to keep increasing
 186         int choiceIndex = choiceCounter % choices.length;
 187         icsCG.advance(choices[choiceIndex]);
 188         // Index the ChoiceGenerator to set backtracking points
 189         cgList.add(icsCG);
 190       }
 191     }
 192   }
 193
 194   @Override
 195   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 196
 197     if (stateReductionMode) {
 198       // Check the boolean CG and if it is flipped, we are resetting the analysis
 199 //      if (currentCG instanceof BooleanChoiceGenerator) {
 200 //        if (!isBooleanCGFlipped) {
 201 //          isBooleanCGFlipped = true;
 202 //        } else {
 203 //          initializeStateReduction();
 204 //        }
 205 //      }
 206       // Check every choice generated and ensure fair scheduling!
 207       if (currentCG instanceof IntChoiceFromSet) {
 208         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
 209         // If we don't see a fair scheduling of events/choices then we have to enforce it
 210         checkAndEnforceFairScheduling(icsCG);
 211         // Map state to event
 212         mapStateToEvent(icsCG.getNextChoice());
 213         // Check if we have seen this state or this state contains cycles that involve all events
 214         if (terminateCurrentExecution()) {
 215           exploreNextBacktrackSets(icsCG);
 216         }
 217         justVisitedStates.clear();
 218         choiceCounter++;
 219       }
 220     }
 221   }
 222
 223   @Override
 224   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 225     if (stateReductionMode) {
 226       // Has to be initialized and a integer CG
 227       ChoiceGenerator<?> cg = vm.getChoiceGenerator();
 228       if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
 229         int currentChoice = choiceCounter - 1;  // Accumulative choice w.r.t the current trace
 230         //if (getCurrentChoice(vm) < 0) { // If choice is -1 then skip
 231         if (currentChoice < 0) { // If choice is -1 then skip
 232           return;
 233         }
 234         // Record accesses from executed instructions
 235         if (executedInsn instanceof JVMFieldInstruction) {
 236           // Analyze only after being initialized
 237           String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
 238           // We don't care about libraries
 239           if (!isFieldExcluded(fieldClass)) {
 240             analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
 241           }
 242         } else if (executedInsn instanceof INVOKEINTERFACE) {
 243           // Handle the read/write accesses that occur through iterators
 244           analyzeReadWriteAccesses(executedInsn, ti, currentChoice);
 245         }
 246         // Analyze conflicts from next instructions
 247         if (nextInsn instanceof JVMFieldInstruction) {
 248           // Skip the constructor because it is called once and does not have shared access with other objects
 249           if (!nextInsn.getMethodInfo().getName().equals("<init>")) {
 250             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
 251             if (!isFieldExcluded(fieldClass)) {
 252               // Check for conflict (go backward from current choice and get the first conflict)
 253               for (int evtCntr = currentChoice - 1; evtCntr >= 0; evtCntr--) {
 254                 if (!readWriteFieldsMap.containsKey(evtCntr)) { // Skip if this event does not have any Read/Write set
 255                   continue;
 256                 }
 257                 ReadWriteSet rwSet = readWriteFieldsMap.get(evtCntr);
 258                 int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
 259                 // Check for conflicts with Write fields for both Read and Write instructions
 260                 if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
 261                       rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
 262                      (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
 263                       rwSet.readFieldObjectId(fieldClass) == currObjId)) {
 264                   // Check and record a backtrack set for just once!
 265                   if (successfullyRecordConflictPair(currentChoice, evtCntr)) {
 266                     // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
 267 //                    if (vm.isNewState() || isReachableInVODGraph(refChoices[currentChoice], refChoices[currentChoice-1])) {
 268 //                      createBacktrackChoiceList(currentChoice, eventNumber);
 269 //                    }
 270                   }
 271                 }
 272               }
 273             }
 274           }
 275         }
 276       }
 277     }
 278   }
 279
 280
 281   // == HELPERS
 282   // -- INNER CLASS
 283   // This class compactly stores Read and Write field sets
 284   // We store the field name and its object ID
 285   // Sharing the same field means the same field name and object ID
 286   private class ReadWriteSet {
 287     private HashMap<String, Integer> readSet;
 288     private HashMap<String, Integer> writeSet;
 289
 290     public ReadWriteSet() {
 291       readSet = new HashMap<>();
 292       writeSet = new HashMap<>();
 293     }
 294
 295     public void addReadField(String field, int objectId) {
 296       readSet.put(field, objectId);
 297     }
 298
 299     public void addWriteField(String field, int objectId) {
 300       writeSet.put(field, objectId);
 301     }
 302
 303     public boolean readFieldExists(String field) {
 304       return readSet.containsKey(field);
 305     }
 306
 307     public boolean writeFieldExists(String field) {
 308       return writeSet.containsKey(field);
 309     }
 310
 311     public int readFieldObjectId(String field) {
 312       return readSet.get(field);
 313     }
 314
 315     public int writeFieldObjectId(String field) {
 316       return writeSet.get(field);
 317     }
 318   }
 319
 320   // -- CONSTANTS
 321   private final static String DO_CALL_METHOD = "doCall";
 322   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
 323   private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"};
 324   private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST =
 325           // Groovy library created fields
 326           {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__",
 327           // Infrastructure
 328           "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList",
 329           "eventList", "valueList", "settings", "printToConsole", "app1", "app2"};
 330   private final static String[] EXCLUDED_FIELDS_STARTS_WITH_LIST =
 331           // Java and Groovy libraries
 332           { "java", "org", "sun", "com", "gov", "groovy"};
 333   private final static String[] EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"};
 334   private final static String GET_PROPERTY_METHOD =
 335           "invokeinterface org.codehaus.groovy.runtime.callsite.CallSite.callGetProperty";
 336   private final static String GROOVY_CALLSITE_LIB = "org.codehaus.groovy.runtime.callsite";
 337   private final static String JAVA_INTEGER = "int";
 338   private final static String JAVA_STRING_LIB = "java.lang.String";
 339
 340   // -- FUNCTIONS
 341   private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) {
 342     // Check the next choice and if the value is not the same as the expected then force the expected value
 343     int choiceIndex = choiceCounter % refChoices.length;
 344     int nextChoice = icsCG.getNextChoice();
 345     if (refChoices[choiceIndex] != nextChoice) {
 346       int expectedChoice = refChoices[choiceIndex];
 347       int currCGIndex = icsCG.getNextChoiceIndex();
 348       if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) {
 349         icsCG.setChoice(currCGIndex, expectedChoice);
 350       }
 351     }
 352   }
 353
 354   private Integer[] copyChoices(Integer[] choicesToCopy) {
 355
 356     Integer[] copyOfChoices = new Integer[choicesToCopy.length];
 357     System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length);
 358     return copyOfChoices;
 359   }
 360
 361   // --- Functions related to cycle detection
 362
 363   // Detect cycles in the current execution/trace
 364   // We terminate the execution iff:
 365   // (1) the state has been visited in the current execution
 366   // (2) the state has one or more cycles that involve all the events
 367   // With simple approach we only need to check for a re-visited state.
 368   // Basically, we have to check that we have executed all events between two occurrences of such state.
 369   private boolean containsCyclesWithAllEvents(int stId) {
 370
 371     // False if the state ID hasn't been recorded
 372     if (!stateToEventMap.containsKey(stId)) {
 373       return false;
 374     }
 375     HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
 376     // Check if this set contains all the event choices
 377     // If not then this is not the terminating condition
 378     for(int i=0; i<=maxEventChoice; i++) {
 379       if (!visitedEvents.contains(i)) {
 380         return false;
 381       }
 382     }
 383     return true;
 384   }
 385
 386   private void mapStateToEvent(int nextChoiceValue) {
 387     // Update all states with this event/choice
 388     // This means that all past states now see this transition
 389     Set<Integer> stateSet = stateToEventMap.keySet();
 390     for(Integer stateId : stateSet) {
 391       HashSet<Integer> eventSet = stateToEventMap.get(stateId);
 392       eventSet.add(nextChoiceValue);
 393     }
 394   }
 395
 396   private boolean terminateCurrentExecution() {
 397     // We need to check all the states that have just been visited
 398     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
 399     for(Integer stateId : justVisitedStates) {
 400       if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
 401         return true;
 402       }
 403     }
 404     return false;
 405   }
 406
 407   private void updateStateInfo(Search search) {
 408     // Update the state variables
 409     // Line 19 in the paper page 11 (see the heading note above)
 410     int stateId = search.getStateId();
 411     currVisitedStates.add(stateId);
 412     // Insert state ID into the map if it is new
 413     if (!stateToEventMap.containsKey(stateId)) {
 414       HashSet<Integer> eventSet = new HashSet<>();
 415       stateToEventMap.put(stateId, eventSet);
 416     }
 417     justVisitedStates.add(stateId);
 418   }
 419
 420   // --- Functions related to Read/Write access analysis on shared fields
 421
 422   // Analyze Read/Write accesses that are directly invoked on fields
 423   private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) {
 424     // Do the analysis to get Read and Write accesses to fields
 425     ReadWriteSet rwSet = getReadWriteSet(currentChoice);
 426     int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef();
 427     // Record the field in the map
 428     if (executedInsn instanceof WriteInstruction) {
 429       // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
 430       for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
 431         if (fieldClass.startsWith(str)) {
 432           return;
 433         }
 434       }
 435       rwSet.addWriteField(fieldClass, objectId);
 436     } else if (executedInsn instanceof ReadInstruction) {
 437       rwSet.addReadField(fieldClass, objectId);
 438     }
 439   }
 440
 441   // Analyze Read accesses that are indirect (performed through iterators)
 442   // These accesses are marked by certain bytecode instructions, e.g., INVOKEINTERFACE
 443   private void analyzeReadWriteAccesses(Instruction instruction, ThreadInfo ti, int currentChoice) {
 444     // Get method name
 445     INVOKEINTERFACE insn = (INVOKEINTERFACE) instruction;
 446     if (insn.toString().startsWith(GET_PROPERTY_METHOD) &&
 447             insn.getMethodInfo().getName().equals(DO_CALL_METHOD)) {
 448       // Extract info from the stack frame
 449       StackFrame frame = ti.getTopFrame();
 450       int[] frameSlots = frame.getSlots();
 451       // Get the Groovy callsite library at index 0
 452       ElementInfo eiCallsite = VM.getVM().getHeap().get(frameSlots[0]);
 453       if (!eiCallsite.getClassInfo().getName().startsWith(GROOVY_CALLSITE_LIB)) {
 454         return;
 455       }
 456       // Get the iterated object whose property is accessed
 457       ElementInfo eiAccessObj = VM.getVM().getHeap().get(frameSlots[1]);
 458       // We exclude library classes (they start with java, org, etc.) and some more
 459       String objClassName = eiAccessObj.getClassInfo().getName();
 460       if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName) ||
 461           excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName)) {
 462         return;
 463       }
 464       // Extract fields from this object and put them into the read write
 465       int numOfFields = eiAccessObj.getNumberOfFields();
 466       for(int i=0; i<numOfFields; i++) {
 467         FieldInfo fieldInfo = eiAccessObj.getFieldInfo(i);
 468         if (fieldInfo.getType().equals(JAVA_STRING_LIB) || fieldInfo.getType().equals(JAVA_INTEGER)) {
 469           String fieldClass = fieldInfo.getFullName();
 470           ReadWriteSet rwSet = getReadWriteSet(currentChoice);
 471           int objectId = fieldInfo.getClassInfo().getClassObjectRef();
 472           // Record the field in the map
 473           rwSet.addReadField(fieldClass, objectId);
 474         }
 475       }
 476     }
 477   }
 478
 479   private boolean excludeThisForItContains(String[] excludedStrings, String className) {
 480     for (String excludedField : excludedStrings) {
 481       if (className.contains(excludedField)) {
 482         return true;
 483       }
 484     }
 485     return false;
 486   }
 487
 488   private boolean excludeThisForItEndsWith(String[] excludedStrings, String className) {
 489     for (String excludedField : excludedStrings) {
 490       if (className.endsWith(excludedField)) {
 491         return true;
 492       }
 493     }
 494     return false;
 495   }
 496
 497   private boolean excludeThisForItStartsWith(String[] excludedStrings, String className) {
 498     for (String excludedField : excludedStrings) {
 499       if (className.startsWith(excludedField)) {
 500         return true;
 501       }
 502     }
 503     return false;
 504   }
 505
 506   private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {
 507     // Save all the visited states when starting a new execution of trace
 508     prevVisitedStates.addAll(currVisitedStates);
 509     currVisitedStates.clear();
 510
 511   }
 512
 513   private int getCurrentChoice(VM vm) {
 514     ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
 515     // This is the main event CG
 516     if (currentCG instanceof IntChoiceFromSet) {
 517       return ((IntChoiceFromSet) currentCG).getNextChoiceIndex();
 518     } else {
 519       // This is the interval CG used in device handlers
 520       ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
 521       return ((IntChoiceFromSet) parentCG).getNextChoiceIndex();
 522     }
 523   }
 524
 525   private ReadWriteSet getReadWriteSet(int currentChoice) {
 526     // Do the analysis to get Read and Write accesses to fields
 527     ReadWriteSet rwSet;
 528     // We already have an entry
 529     if (readWriteFieldsMap.containsKey(currentChoice)) {
 530       rwSet = readWriteFieldsMap.get(currentChoice);
 531     } else { // We need to create a new entry
 532       rwSet = new ReadWriteSet();
 533       readWriteFieldsMap.put(currentChoice, rwSet);
 534     }
 535     return rwSet;
 536   }
 537
 538   private boolean isFieldExcluded(String field) {
 539     // Check against "starts-with", "ends-with", and "contains" list
 540     if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) ||
 541             excludeThisForItEndsWith(EXCLUDED_FIELDS_ENDS_WITH_LIST, field) ||
 542             excludeThisForItContains(EXCLUDED_FIELDS_CONTAINS_LIST, field)) {
 543       return true;
 544     }
 545
 546     return false;
 547   }
 548
 549   private boolean successfullyRecordConflictPair(int currentEvent, int eventNumber) {
 550     HashSet<Integer> conflictSet;
 551     if (!conflictPairMap.containsKey(currentEvent)) {
 552       conflictSet = new HashSet<>();
 553       conflictPairMap.put(currentEvent, conflictSet);
 554     } else {
 555       conflictSet = conflictPairMap.get(currentEvent);
 556     }
 557     // If this conflict has been recorded before, we return false because
 558     // we don't want to service this backtrack point twice
 559     if (conflictSet.contains(eventNumber)) {
 560       return false;
 561     }
 562     // If it hasn't been recorded, then do otherwise
 563     conflictSet.add(eventNumber);
 564     return true;
 565   }
 566 }