src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.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.jvm.bytecode.INVOKEINTERFACE;
  24 import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
  25 import gov.nasa.jpf.search.Search;
  26 import gov.nasa.jpf.vm.*;
  27 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
  28 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
  29 import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
  30 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
  31
  32 import java.io.FileWriter;
  33 import java.io.IOException;
  34 import java.io.PrintWriter;
  35 import java.util.*;
  36 import java.util.logging.Logger;
  37
  38 /**
  39  * This a DPOR implementation for event-driven applications with loops that create cycles of state matching
  40  * In this new DPOR algorithm/implementation, each run is terminated iff:
  41  * - we find a state that matches a state in a previous run, or
  42  * - we have a matched state in the current run that consists of cycles that contain all choices/events.
  43  */
  44 public class DPORStateReducerWithSummary extends ListenerAdapter {
  45
  46   // Information printout fields for verbose mode
  47   private boolean verboseMode;
  48   private boolean stateReductionMode;
  49   private final PrintWriter out;
  50   private PrintWriter fileWriter;
  51   private String detail;
  52   private int depth;
  53   private int id;
  54   private Transition transition;
  55
  56   // DPOR-related fields
  57   // Basic information
  58   private Integer[] choices;
  59   private Integer[] refChoices; // Second reference to a copy of choices (choices may be modified for fair scheduling)
  60   private int choiceCounter;
  61   private int maxEventChoice;
  62   // Data structure to track the events seen by each state to track cycles (containing all events) for termination
  63   private HashMap<Integer,Integer> currVisitedStates; // States visited in the current execution (maps to frequency)
  64   private HashSet<Integer> justVisitedStates;   // States just visited in the previous choice/event
  65   private HashSet<Integer> prevVisitedStates;   // States visited in the previous execution
  66   private HashSet<ClassInfo> nonRelevantClasses;// Class info objects of non-relevant classes
  67   private HashSet<FieldInfo> nonRelevantFields; // Field info objects of non-relevant fields
  68   private HashSet<FieldInfo> relevantFields;    // Field info objects of relevant fields
  69   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
  70   // Data structure to analyze field Read/Write accesses and conflicts
  71   private HashMap<Integer, LinkedList<BacktrackExecution>> backtrackMap;  // Track created backtracking points
  72   private PriorityQueue<Integer> backtrackStateQ;                 // Heap that returns the latest state
  73   private Execution currentExecution;                             // Holds the information about the current execution
  74   private HashMap<Integer, HashSet<Integer>> doneBacktrackMap;    // Record state ID and trace already constructed
  75   private MainSummary mainSummary;                                // Main summary (M) for state ID, event, and R/W set
  76   private HashMap<Integer, PredecessorInfo> stateToPredInfo;      // Predecessor info indexed by state ID
  77   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
  78   private RGraph rGraph;                                          // R-Graph for past executions
  79
  80   // Boolean states
  81   private boolean isBooleanCGFlipped;
  82   private boolean isEndOfExecution;
  83
  84   // Statistics
  85   private int numOfTransitions;
  86
  87   public DPORStateReducerWithSummary(Config config, JPF jpf) {
  88     verboseMode = config.getBoolean("printout_state_transition", false);
  89     stateReductionMode = config.getBoolean("activate_state_reduction", true);
  90     if (verboseMode) {
  91       out = new PrintWriter(System.out, true);
  92     } else {
  93       out = null;
  94     }
  95     String outputFile = config.getString("file_output");
  96     if (!outputFile.isEmpty()) {
  97       try {
  98         fileWriter = new PrintWriter(new FileWriter(outputFile, true), true);
  99       } catch (IOException e) {
 100       }
 101     }
 102     isBooleanCGFlipped = false;
 103     mainSummary = new MainSummary();
 104                 numOfTransitions = 0;
 105                 nonRelevantClasses = new HashSet<>();
 106                 nonRelevantFields = new HashSet<>();
 107                 relevantFields = new HashSet<>();
 108     restorableStateMap = new HashMap<>();
 109     stateToPredInfo = new HashMap<>();
 110     initializeStatesVariables();
 111   }
 112
 113   @Override
 114   public void stateRestored(Search search) {
 115     if (verboseMode) {
 116       id = search.getStateId();
 117       depth = search.getDepth();
 118       transition = search.getTransition();
 119       detail = null;
 120       out.println("\n==> DEBUG: The state is restored to state with id: " + id + " -- Transition: " + transition +
 121               " and depth: " + depth + "\n");
 122     }
 123   }
 124
 125   @Override
 126   public void searchStarted(Search search) {
 127     if (verboseMode) {
 128       out.println("\n==> DEBUG: ----------------------------------- search started" + "\n");
 129     }
 130   }
 131
 132   @Override
 133   public void stateAdvanced(Search search) {
 134     if (verboseMode) {
 135       id = search.getStateId();
 136       depth = search.getDepth();
 137       transition = search.getTransition();
 138       if (search.isNewState()) {
 139         detail = "new";
 140       } else {
 141         detail = "visited";
 142       }
 143
 144       if (search.isEndState()) {
 145         out.println("\n==> DEBUG: This is the last state!\n");
 146         detail += " end";
 147       }
 148       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
 149               " which is " + detail + " Transition: " + transition + "\n");
 150     }
 151     if (stateReductionMode) {
 152       updateStateInfo(search);
 153     }
 154   }
 155
 156   @Override
 157   public void stateBacktracked(Search search) {
 158     if (verboseMode) {
 159       id = search.getStateId();
 160       depth = search.getDepth();
 161       transition = search.getTransition();
 162       detail = null;
 163
 164       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
 165               " and depth: " + depth + "\n");
 166     }
 167     if (stateReductionMode) {
 168       updateStateInfo(search);
 169     }
 170   }
 171
 172   static Logger log = JPF.getLogger("report");
 173
 174   @Override
 175   public void searchFinished(Search search) {
 176     if (verboseMode) {
 177       out.println("\n==> DEBUG: ----------------------------------- search finished");
 178       out.println("\n==> DEBUG: State reduction mode  : " + stateReductionMode);
 179       out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
 180       out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
 181
 182       fileWriter.println("==> DEBUG: State reduction mode  : " + stateReductionMode);
 183       fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
 184       fileWriter.println();
 185       fileWriter.close();
 186     }
 187   }
 188
 189   @Override
 190   public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
 191     if (stateReductionMode) {
 192       // Initialize with necessary information from the CG
 193       if (nextCG instanceof IntChoiceFromSet) {
 194         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
 195         // Tell JPF that we are performing DPOR
 196         icsCG.setDpor();
 197         if (!isEndOfExecution) {
 198           // Check if CG has been initialized, otherwise initialize it
 199           Integer[] cgChoices = icsCG.getAllChoices();
 200           // Record the events (from choices)
 201           if (choices == null) {
 202             choices = cgChoices;
 203             // Make a copy of choices as reference
 204             refChoices = copyChoices(choices);
 205             // Record the max event choice (the last element of the choice array)
 206             maxEventChoice = choices[choices.length - 1];
 207           }
 208           icsCG.setNewValues(choices);
 209           icsCG.reset();
 210           // Use a modulo since choiceCounter is going to keep increasing
 211           int choiceIndex = choiceCounter % choices.length;
 212           icsCG.advance(choices[choiceIndex]);
 213         } else {
 214           // Set done all CGs while transitioning to a new execution
 215           icsCG.setDone();
 216         }
 217       }
 218     }
 219   }
 220
 221   @Override
 222   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 223     if (stateReductionMode) {
 224       // Check the boolean CG and if it is flipped, we are resetting the analysis
 225       if (currentCG instanceof BooleanChoiceGenerator) {
 226         if (!isBooleanCGFlipped) {
 227           isBooleanCGFlipped = true;
 228         } else {
 229           // Allocate new objects for data structure when the boolean is flipped from "false" to "true"
 230           initializeStatesVariables();
 231         }
 232       }
 233       // Check every choice generated and ensure fair scheduling!
 234       if (currentCG instanceof IntChoiceFromSet) {
 235         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
 236         // If this is a new CG then we need to update data structures
 237         resetStatesForNewExecution(icsCG, vm);
 238         // If we don't see a fair scheduling of events/choices then we have to enforce it
 239         ensureFairSchedulingAndSetupTransition(icsCG, vm);
 240         // Update backtrack set of an executed event (transition): one transition before this one
 241         updateBacktrackSet(currentExecution, choiceCounter - 1);
 242         // Explore the next backtrack point:
 243         // 1) if we have seen this state or this state contains cycles that involve all events, and
 244         // 2) after the current CG is advanced at least once
 245         if (choiceCounter > 0 && terminateCurrentExecution()) {
 246           exploreNextBacktrackPoints(vm, icsCG);
 247         } else {
 248           numOfTransitions++;
 249         }
 250         // Map state to event
 251         mapStateToEvent(icsCG.getNextChoice());
 252         justVisitedStates.clear();
 253         choiceCounter++;
 254       }
 255     } else {
 256       numOfTransitions++;
 257     }
 258   }
 259
 260   @Override
 261   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
 262     if (stateReductionMode) {
 263       if (!isEndOfExecution) {
 264         // Has to be initialized and it is a integer CG
 265         ChoiceGenerator<?> cg = vm.getChoiceGenerator();
 266         if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
 267           int currentChoice = choiceCounter - 1;  // Accumulative choice w.r.t the current trace
 268           if (currentChoice < 0) { // If choice is -1 then skip
 269             return;
 270           }
 271           currentChoice = checkAndAdjustChoice(currentChoice, vm);
 272           // Record accesses from executed instructions
 273           if (executedInsn instanceof JVMFieldInstruction) {
 274             // We don't care about libraries
 275             if (!isFieldExcluded(executedInsn)) {
 276               analyzeReadWriteAccesses(executedInsn, currentChoice);
 277             }
 278           } else if (executedInsn instanceof INVOKEINTERFACE) {
 279             // Handle the read/write accesses that occur through iterators
 280             analyzeReadWriteAccesses(executedInsn, ti, currentChoice);
 281           }
 282         }
 283       }
 284     }
 285   }
 286
 287
 288   // == HELPERS
 289
 290   // -- INNER CLASSES
 291
 292   // This class compactly stores backtrack execution:
 293   // 1) backtrack choice list, and
 294   // 2) first backtrack point (linking with predecessor execution)
 295   private class BacktrackExecution {
 296     private Integer[] choiceList;
 297     private TransitionEvent firstTransition;
 298
 299     public BacktrackExecution(Integer[] choList, TransitionEvent fTransition) {
 300       choiceList = choList;
 301       firstTransition = fTransition;
 302     }
 303
 304     public Integer[] getChoiceList() {
 305       return choiceList;
 306     }
 307
 308     public TransitionEvent getFirstTransition() {
 309       return firstTransition;
 310     }
 311   }
 312
 313   // This class stores a representation of an execution
 314   // TODO: We can modify this class to implement some optimization (e.g., clock-vector)
 315   // TODO: We basically need to keep track of:
 316   // TODO:    (1) last read/write access to each memory location
 317   // TODO:    (2) last state with two or more incoming events/transitions
 318   private class Execution {
 319     private HashMap<IntChoiceFromSet, Integer> cgToChoiceMap;   // Map between CG to choice numbers for O(1) access
 320     private ArrayList<TransitionEvent> executionTrace;          // The BacktrackPoint objects of this execution
 321     private boolean isNew;                                      // Track if this is the first time it is accessed
 322     private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;  // Record fields that are accessed
 323
 324     public Execution() {
 325       cgToChoiceMap = new HashMap<>();
 326       executionTrace = new ArrayList<>();
 327       isNew = true;
 328       readWriteFieldsMap = new HashMap<>();
 329     }
 330
 331     public void addTransition(TransitionEvent newBacktrackPoint) {
 332       executionTrace.add(newBacktrackPoint);
 333     }
 334
 335     public void clearCGToChoiceMap() {
 336       cgToChoiceMap = null;
 337     }
 338
 339     public int getChoiceFromCG(IntChoiceFromSet icsCG) {
 340       return cgToChoiceMap.get(icsCG);
 341     }
 342
 343     public ArrayList<TransitionEvent> getExecutionTrace() {
 344       return executionTrace;
 345     }
 346
 347     public TransitionEvent getFirstTransition() {
 348       return executionTrace.get(0);
 349     }
 350
 351     public TransitionEvent getLastTransition() {
 352       return executionTrace.get(executionTrace.size() - 1);
 353     }
 354
 355     public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
 356       return readWriteFieldsMap;
 357     }
 358
 359     public boolean isNew() {
 360       if (isNew) {
 361         // Right after this is accessed, it is no longer new
 362         isNew = false;
 363         return true;
 364       }
 365       return false;
 366     }
 367
 368     public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
 369       cgToChoiceMap.put(icsCG, choice);
 370     }
 371   }
 372
 373   // This class compactly stores a predecessor
 374   // 1) a predecessor execution
 375   // 2) the predecessor choice in that predecessor execution
 376   private class Predecessor {
 377     private int choice;           // Predecessor choice
 378     private Execution execution;  // Predecessor execution
 379
 380     public Predecessor(int predChoice, Execution predExec) {
 381       choice = predChoice;
 382       execution = predExec;
 383     }
 384
 385     public int getChoice() {
 386       return choice;
 387     }
 388
 389     public Execution getExecution() {
 390       return execution;
 391     }
 392   }
 393
 394   // This class represents a R-Graph (in the paper it is a state transition graph R)
 395   // This implementation stores reachable transitions from and connects with past executions
 396   private class RGraph {
 397     private int hiStateId;                                     // Maximum state Id
 398     private HashMap<Integer, HashSet<TransitionEvent>> graph;  // Reachable transitions from past executions
 399
 400     public RGraph() {
 401       hiStateId = 0;
 402       graph = new HashMap<>();
 403     }
 404
 405     public void addReachableTransition(int stateId, TransitionEvent transition) {
 406       HashSet<TransitionEvent> transitionSet;
 407       if (graph.containsKey(stateId)) {
 408         transitionSet = graph.get(stateId);
 409       } else {
 410         transitionSet = new HashSet<>();
 411         graph.put(stateId, transitionSet);
 412       }
 413       // Insert into the set if it does not contain it yet
 414       if (!transitionSet.contains(transition)) {
 415         transitionSet.add(transition);
 416       }
 417       // Update highest state ID
 418       if (hiStateId < stateId) {
 419         hiStateId = stateId;
 420       }
 421     }
 422
 423     public HashSet<TransitionEvent> getReachableTransitionsAtState(int stateId) {
 424       if (!graph.containsKey(stateId)) {
 425         // This is a loop from a transition to itself, so just return the current transition
 426         HashSet<TransitionEvent> transitionSet = new HashSet<>();
 427         transitionSet.add(currentExecution.getLastTransition());
 428         return transitionSet;
 429       }
 430       return graph.get(stateId);
 431     }
 432
 433     public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
 434       HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
 435       // All transitions from states higher than the given state ID (until the highest state ID) are reachable
 436       for(int stId = stateId; stId <= hiStateId; stId++) {
 437         // We might encounter state IDs from the first round of Boolean CG
 438         // The second round of Boolean CG should consider these new states
 439         if (graph.containsKey(stId)) {
 440           reachableTransitions.addAll(graph.get(stId));
 441         }
 442       }
 443       return reachableTransitions;
 444     }
 445   }
 446
 447   // This class compactly stores Read and Write field sets
 448   // We store the field name and its object ID
 449   // Sharing the same field means the same field name and object ID
 450   private class ReadWriteSet {
 451     private HashMap<String, Integer> readMap;
 452     private HashMap<String, Integer> writeMap;
 453
 454     public ReadWriteSet() {
 455       readMap = new HashMap<>();
 456       writeMap = new HashMap<>();
 457     }
 458
 459     public void addReadField(String field, int objectId) {
 460       readMap.put(field, objectId);
 461     }
 462
 463     public void addWriteField(String field, int objectId) {
 464       writeMap.put(field, objectId);
 465     }
 466
 467     public void removeReadField(String field) {
 468       readMap.remove(field);
 469     }
 470
 471     public void removeWriteField(String field) {
 472       writeMap.remove(field);
 473     }
 474
 475     public boolean isEmpty() {
 476       return readMap.isEmpty() && writeMap.isEmpty();
 477     }
 478
 479     public ReadWriteSet getCopy() {
 480       ReadWriteSet copyRWSet = new ReadWriteSet();
 481       // Copy the maps in the set into the new object copy
 482       copyRWSet.setReadMap(new HashMap<>(this.getReadMap()));
 483       copyRWSet.setWriteMap(new HashMap<>(this.getWriteMap()));
 484       return copyRWSet;
 485     }
 486
 487     public Set<String> getReadSet() {
 488       return readMap.keySet();
 489     }
 490
 491     public Set<String> getWriteSet() {
 492       return writeMap.keySet();
 493     }
 494
 495     public boolean readFieldExists(String field) {
 496       return readMap.containsKey(field);
 497     }
 498
 499     public boolean writeFieldExists(String field) {
 500       return writeMap.containsKey(field);
 501     }
 502
 503     public int readFieldObjectId(String field) {
 504       return readMap.get(field);
 505     }
 506
 507     public int writeFieldObjectId(String field) {
 508       return writeMap.get(field);
 509     }
 510
 511     private HashMap<String, Integer> getReadMap() {
 512       return readMap;
 513     }
 514
 515     private HashMap<String, Integer> getWriteMap() {
 516       return writeMap;
 517     }
 518
 519     private void setReadMap(HashMap<String, Integer> rMap) {
 520       readMap = rMap;
 521     }
 522
 523     private void setWriteMap(HashMap<String, Integer> wMap) {
 524       writeMap = wMap;
 525     }
 526   }
 527
 528   // This class is a representation of a state.
 529   // It stores the predecessors to a state.
 530   // TODO: We also have stateToEventMap, restorableStateMap, and doneBacktrackMap that has state Id as HashMap key.
 531   private class PredecessorInfo {
 532     private HashSet<Predecessor> predecessors;  // Maps incoming events/transitions (execution and choice)
 533     private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
 534                                                 // Memorize event and choice number to not record them twice
 535
 536     public PredecessorInfo() {
 537       predecessors = new HashSet<>();
 538       recordedPredecessors = new HashMap<>();
 539     }
 540
 541     public HashSet<Predecessor> getPredecessors() {
 542       return predecessors;
 543     }
 544
 545     private boolean isRecordedPredecessor(Execution execution, int choice) {
 546       // See if we have recorded this predecessor earlier
 547       HashSet<Integer> recordedChoices;
 548       if (recordedPredecessors.containsKey(execution)) {
 549         recordedChoices = recordedPredecessors.get(execution);
 550         if (recordedChoices.contains(choice)) {
 551           return true;
 552         }
 553       } else {
 554         recordedChoices = new HashSet<>();
 555         recordedPredecessors.put(execution, recordedChoices);
 556       }
 557       // Record the choice if we haven't seen it
 558       recordedChoices.add(choice);
 559
 560       return false;
 561     }
 562
 563     public void recordPredecessor(Execution execution, int choice) {
 564       if (!isRecordedPredecessor(execution, choice)) {
 565         predecessors.add(new Predecessor(choice, execution));
 566       }
 567     }
 568   }
 569
 570   // This class compactly stores transitions:
 571   // 1) CG,
 572   // 2) state ID,
 573   // 3) choice,
 574   // 4) predecessors (for backward DFS).
 575   private class TransitionEvent {
 576     private int choice;                        // Choice chosen at this transition
 577     private int choiceCounter;                 // Choice counter at this transition
 578     private Execution execution;               // The execution where this transition belongs
 579     private int stateId;                       // State at this transition
 580     private IntChoiceFromSet transitionCG;     // CG at this transition
 581
 582     public TransitionEvent() {
 583       choice = 0;
 584       choiceCounter = 0;
 585       execution = null;
 586       stateId = 0;
 587       transitionCG = null;
 588     }
 589
 590     public int getChoice() {
 591       return choice;
 592     }
 593
 594     public int getChoiceCounter() {
 595       return choiceCounter;
 596     }
 597
 598     public Execution getExecution() {
 599       return execution;
 600     }
 601
 602     public int getStateId() {
 603       return stateId;
 604     }
 605
 606     public IntChoiceFromSet getTransitionCG() { return transitionCG; }
 607
 608     public void setChoice(int cho) {
 609       choice = cho;
 610     }
 611
 612     public void setChoiceCounter(int choCounter) {
 613       choiceCounter = choCounter;
 614     }
 615
 616     public void setExecution(Execution exec) {
 617       execution = exec;
 618     }
 619
 620     public void setStateId(int stId) {
 621       stateId = stId;
 622     }
 623
 624     public void setTransitionCG(IntChoiceFromSet cg) {
 625       transitionCG = cg;
 626     }
 627   }
 628
 629   // -- PRIVATE CLASSES RELATED TO SUMMARY
 630   // This class stores the main summary of states
 631   // 1) Main mapping between state ID and state summary
 632   // 2) State summary is a mapping between events (i.e., event choices) and their respective R/W sets
 633   private class MainSummary {
 634     private HashMap<Integer, HashMap<Integer, ReadWriteSet>> mainSummary;
 635
 636     public MainSummary() {
 637       mainSummary = new HashMap<>();
 638     }
 639
 640     public Set<Integer> getEventChoicesAtStateId(int stateId) {
 641       HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
 642       // Return a new set since this might get updated concurrently
 643       return new HashSet<>(stateSummary.keySet());
 644     }
 645
 646     public ReadWriteSet getRWSetForEventChoiceAtState(int eventChoice, int stateId) {
 647       HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
 648       return stateSummary.get(eventChoice);
 649     }
 650
 651     public Set<Integer> getStateIds() {
 652       return mainSummary.keySet();
 653     }
 654
 655     private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
 656       // Combine the same write accesses and record in the recordedRWSet
 657       HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
 658       HashMap<String, Integer> writeMap = rwSet.getWriteMap();
 659       for(Map.Entry<String, Integer> entry : recordedWriteMap.entrySet()) {
 660         String writeField = entry.getKey();
 661         // Remove the entry from rwSet if both field and object ID are the same
 662         if (writeMap.containsKey(writeField) &&
 663                 (writeMap.get(writeField).equals(recordedWriteMap.get(writeField)))) {
 664           writeMap.remove(writeField);
 665         }
 666       }
 667       // Then add the rest (fields in rwSet but not in recordedRWSet)
 668       // into the recorded map because these will be traversed
 669       recordedWriteMap.putAll(writeMap);
 670       // Combine the same read accesses and record in the recordedRWSet
 671       HashMap<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
 672       HashMap<String, Integer> readMap = rwSet.getReadMap();
 673       for(Map.Entry<String, Integer> entry : recordedReadMap.entrySet()) {
 674         String readField = entry.getKey();
 675         // Remove the entry from rwSet if both field and object ID are the same
 676         if (readMap.containsKey(readField) &&
 677                 (readMap.get(readField).equals(recordedReadMap.get(readField)))) {
 678           readMap.remove(readField);
 679         }
 680       }
 681       // Then add the rest (fields in rwSet but not in recordedRWSet)
 682       // into the recorded map because these will be traversed
 683       recordedReadMap.putAll(readMap);
 684
 685       return rwSet;
 686     }
 687
 688     public ReadWriteSet updateStateSummary(int stateId, int eventChoice, ReadWriteSet rwSet) {
 689       // If the state Id has not existed, insert the StateSummary object
 690       // If the state Id has existed, find the event choice:
 691       // 1) If the event choice has not existed, insert the ReadWriteSet object
 692       // 2) If the event choice has existed, perform union between the two ReadWriteSet objects
 693       if (!rwSet.isEmpty()) {
 694         HashMap<Integer, ReadWriteSet> stateSummary;
 695         if (!mainSummary.containsKey(stateId)) {
 696           stateSummary = new HashMap<>();
 697           stateSummary.put(eventChoice, rwSet.getCopy());
 698           mainSummary.put(stateId, stateSummary);
 699         } else {
 700           stateSummary = mainSummary.get(stateId);
 701           if (!stateSummary.containsKey(eventChoice)) {
 702             stateSummary.put(eventChoice, rwSet.getCopy());
 703           } else {
 704             rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
 705           }
 706         }
 707       }
 708       return rwSet;
 709     }
 710   }
 711
 712   // -- CONSTANTS
 713   private final static String DO_CALL_METHOD = "doCall";
 714   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
 715   private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"};
 716   private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST =
 717           // Groovy library created fields
 718           {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__",
 719           // Infrastructure
 720           "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList",
 721           "eventList", "valueList", "settings", "printToConsole", "app1", "app2"};
 722   private final static String[] EXCLUDED_FIELDS_STARTS_WITH_LIST =
 723           // Java and Groovy libraries
 724           { "java", "org", "sun", "com", "gov", "groovy"};
 725   private final static String[] EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"};
 726   private final static String GET_PROPERTY_METHOD =
 727           "invokeinterface org.codehaus.groovy.runtime.callsite.CallSite.callGetProperty";
 728   private final static String GROOVY_CALLSITE_LIB = "org.codehaus.groovy.runtime.callsite";
 729   private final static String JAVA_INTEGER = "int";
 730   private final static String JAVA_STRING_LIB = "java.lang.String";
 731
 732   // -- FUNCTIONS
 733   private Integer[] copyChoices(Integer[] choicesToCopy) {
 734
 735     Integer[] copyOfChoices = new Integer[choicesToCopy.length];
 736     System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length);
 737     return copyOfChoices;
 738   }
 739
 740   private void ensureFairSchedulingAndSetupTransition(IntChoiceFromSet icsCG, VM vm) {
 741     // Check the next choice and if the value is not the same as the expected then force the expected value
 742     int choiceIndex = choiceCounter % refChoices.length;
 743     int nextChoice = icsCG.getNextChoice();
 744     if (refChoices[choiceIndex] != nextChoice) {
 745       int expectedChoice = refChoices[choiceIndex];
 746       int currCGIndex = icsCG.getNextChoiceIndex();
 747       if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) {
 748         icsCG.setChoice(currCGIndex, expectedChoice);
 749       }
 750     }
 751     // Get state ID and associate it with this transition
 752     int stateId = vm.getStateId();
 753     TransitionEvent transition = setupTransition(icsCG, stateId, choiceIndex);
 754     // Add new transition to the current execution and map it in R-Graph
 755     for (Integer stId : justVisitedStates) {  // Map this transition to all the previously passed states
 756       rGraph.addReachableTransition(stId, transition);
 757     }
 758     currentExecution.mapCGToChoice(icsCG, choiceCounter);
 759     // Store restorable state object for this state (always store the latest)
 760     if (!restorableStateMap.containsKey(stateId)) {
 761       RestorableVMState restorableState = vm.getRestorableState();
 762       restorableStateMap.put(stateId, restorableState);
 763     }
 764   }
 765
 766   private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) {
 767     // Get a new transition
 768     TransitionEvent transition;
 769     if (currentExecution.isNew()) {
 770       // We need to handle the first transition differently because this has a predecessor execution
 771       transition = currentExecution.getFirstTransition();
 772     } else {
 773       transition = new TransitionEvent();
 774       currentExecution.addTransition(transition);
 775       addPredecessors(stateId);
 776     }
 777     transition.setExecution(currentExecution);
 778     transition.setTransitionCG(icsCG);
 779     transition.setStateId(stateId);
 780     transition.setChoice(refChoices[choiceIndex]);
 781     transition.setChoiceCounter(choiceCounter);
 782
 783     return transition;
 784   }
 785
 786   // --- Functions related to cycle detection and reachability graph
 787
 788   // Detect cycles in the current execution/trace
 789   // We terminate the execution iff:
 790   // (1) the state has been visited in the current execution
 791   // (2) the state has one or more cycles that involve all the events
 792   // With simple approach we only need to check for a re-visited state.
 793   // Basically, we have to check that we have executed all events between two occurrences of such state.
 794   private boolean completeFullCycle(int stId) {
 795     // False if the state ID hasn't been recorded
 796     if (!stateToEventMap.containsKey(stId)) {
 797       return false;
 798     }
 799     HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
 800     // Check if this set contains all the event choices
 801     // If not then this is not the terminating condition
 802     for(int i=0; i<=maxEventChoice; i++) {
 803       if (!visitedEvents.contains(i)) {
 804         return false;
 805       }
 806     }
 807     return true;
 808   }
 809
 810   private void initializeStatesVariables() {
 811     // DPOR-related
 812     choices = null;
 813     refChoices = null;
 814     choiceCounter = 0;
 815     maxEventChoice = 0;
 816     // Cycle tracking
 817     if (!isBooleanCGFlipped) {
 818       currVisitedStates = new HashMap<>();
 819       justVisitedStates = new HashSet<>();
 820       prevVisitedStates = new HashSet<>();
 821       stateToEventMap = new HashMap<>();
 822     } else {
 823       currVisitedStates.clear();
 824       justVisitedStates.clear();
 825       prevVisitedStates.clear();
 826       stateToEventMap.clear();
 827     }
 828     // Backtracking
 829     if (!isBooleanCGFlipped) {
 830       backtrackMap = new HashMap<>();
 831     } else {
 832       backtrackMap.clear();
 833     }
 834     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
 835     currentExecution = new Execution();
 836     currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
 837     if (!isBooleanCGFlipped) {
 838       doneBacktrackMap = new HashMap<>();
 839     } else {
 840       doneBacktrackMap.clear();
 841     }
 842     rGraph = new RGraph();
 843     // Booleans
 844     isEndOfExecution = false;
 845   }
 846
 847   private void mapStateToEvent(int nextChoiceValue) {
 848     // Update all states with this event/choice
 849     // This means that all past states now see this transition
 850     Set<Integer> stateSet = stateToEventMap.keySet();
 851     for(Integer stateId : stateSet) {
 852       HashSet<Integer> eventSet = stateToEventMap.get(stateId);
 853       eventSet.add(nextChoiceValue);
 854     }
 855   }
 856
 857   private boolean terminateCurrentExecution() {
 858     // We need to check all the states that have just been visited
 859     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
 860     boolean terminate = false;
 861     Set<Integer> mainStateIds = mainSummary.getStateIds();
 862     for(Integer stateId : justVisitedStates) {
 863       // We exclude states that are produced by other CGs that are not integer CG
 864       // When we encounter these states, then we should also encounter the corresponding integer CG state ID
 865       if (mainStateIds.contains(stateId)) {
 866         // We perform updates on backtrack sets for every
 867         if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
 868           updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
 869           terminate = true;
 870         }
 871         // If frequency > 1 then this means we have visited this stateId more than once in the current execution
 872         if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
 873           updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
 874         }
 875       }
 876     }
 877     return terminate;
 878   }
 879
 880   private void updateStateInfo(Search search) {
 881     // Update the state variables
 882     int stateId = search.getStateId();
 883     // Insert state ID into the map if it is new
 884     if (!stateToEventMap.containsKey(stateId)) {
 885       HashSet<Integer> eventSet = new HashSet<>();
 886       stateToEventMap.put(stateId, eventSet);
 887     }
 888     addPredecessorToRevisitedState(stateId);
 889     justVisitedStates.add(stateId);
 890     if (!prevVisitedStates.contains(stateId)) {
 891       // It is a currently visited states if the state has not been seen in previous executions
 892       int frequency = 0;
 893       if (currVisitedStates.containsKey(stateId)) {
 894         frequency = currVisitedStates.get(stateId);
 895       }
 896       currVisitedStates.put(stateId, frequency + 1);  // Increment frequency counter
 897     }
 898   }
 899
 900   // --- Functions related to Read/Write access analysis on shared fields
 901
 902   private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList, TransitionEvent conflictTransition) {
 903     // Insert backtrack point to the right state ID
 904     LinkedList<BacktrackExecution> backtrackExecList;
 905     if (backtrackMap.containsKey(stateId)) {
 906       backtrackExecList = backtrackMap.get(stateId);
 907     } else {
 908       backtrackExecList = new LinkedList<>();
 909       backtrackMap.put(stateId, backtrackExecList);
 910     }
 911     // Add the new backtrack execution object
 912     TransitionEvent backtrackTransition = new TransitionEvent();
 913     backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition));
 914     // Add to priority queue
 915     if (!backtrackStateQ.contains(stateId)) {
 916       backtrackStateQ.add(stateId);
 917     }
 918   }
 919
 920   private void addPredecessors(int stateId) {
 921     PredecessorInfo predecessorInfo;
 922     if (!stateToPredInfo.containsKey(stateId)) {
 923       predecessorInfo = new PredecessorInfo();
 924       stateToPredInfo.put(stateId, predecessorInfo);
 925     } else {  // This is a new state Id
 926       predecessorInfo = stateToPredInfo.get(stateId);
 927     }
 928     predecessorInfo.recordPredecessor(currentExecution, choiceCounter - 1);
 929   }
 930
 931   // Analyze Read/Write accesses that are directly invoked on fields
 932   private void analyzeReadWriteAccesses(Instruction executedInsn, int currentChoice) {
 933     // Get the field info
 934     FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo();
 935     // Analyze only after being initialized
 936     String fieldClass = fieldInfo.getFullName();
 937     // Do the analysis to get Read and Write accesses to fields
 938     ReadWriteSet rwSet = getReadWriteSet(currentChoice);
 939     int objectId = fieldInfo.getClassInfo().getClassObjectRef();
 940     // Record the field in the map
 941     if (executedInsn instanceof WriteInstruction) {
 942       // We first check the non-relevant fields set
 943       if (!nonRelevantFields.contains(fieldInfo)) {
 944         // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes
 945         for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) {
 946           if (fieldClass.startsWith(str)) {
 947             nonRelevantFields.add(fieldInfo);
 948             return;
 949           }
 950         }
 951       } else {
 952         // If we have this field in the non-relevant fields set then we return right away
 953         return;
 954       }
 955       rwSet.addWriteField(fieldClass, objectId);
 956     } else if (executedInsn instanceof ReadInstruction) {
 957       rwSet.addReadField(fieldClass, objectId);
 958     }
 959   }
 960
 961   // Analyze Read accesses that are indirect (performed through iterators)
 962   // These accesses are marked by certain bytecode instructions, e.g., INVOKEINTERFACE
 963   private void analyzeReadWriteAccesses(Instruction instruction, ThreadInfo ti, int currentChoice) {
 964     // Get method name
 965     INVOKEINTERFACE insn = (INVOKEINTERFACE) instruction;
 966     if (insn.toString().startsWith(GET_PROPERTY_METHOD) &&
 967             insn.getMethodInfo().getName().equals(DO_CALL_METHOD)) {
 968       // Extract info from the stack frame
 969       StackFrame frame = ti.getTopFrame();
 970       int[] frameSlots = frame.getSlots();
 971       // Get the Groovy callsite library at index 0
 972       ElementInfo eiCallsite = VM.getVM().getHeap().get(frameSlots[0]);
 973       if (!eiCallsite.getClassInfo().getName().startsWith(GROOVY_CALLSITE_LIB)) {
 974         return;
 975       }
 976       // Get the iterated object whose property is accessed
 977       ElementInfo eiAccessObj = VM.getVM().getHeap().get(frameSlots[1]);
 978       if (eiAccessObj == null) {
 979         return;
 980       }
 981       // We exclude library classes (they start with java, org, etc.) and some more
 982       ClassInfo classInfo = eiAccessObj.getClassInfo();
 983       String objClassName = classInfo.getName();
 984       // Check if this class info is part of the non-relevant classes set already
 985       if (!nonRelevantClasses.contains(classInfo)) {
 986         if (excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName) ||
 987                 excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName)) {
 988           nonRelevantClasses.add(classInfo);
 989           return;
 990         }
 991       } else {
 992         // If it is part of the non-relevant classes set then return immediately
 993         return;
 994       }
 995       // Extract fields from this object and put them into the read write
 996       int numOfFields = eiAccessObj.getNumberOfFields();
 997       for(int i=0; i<numOfFields; i++) {
 998         FieldInfo fieldInfo = eiAccessObj.getFieldInfo(i);
 999         if (fieldInfo.getType().equals(JAVA_STRING_LIB) || fieldInfo.getType().equals(JAVA_INTEGER)) {
1000           String fieldClass = fieldInfo.getFullName();
1001           ReadWriteSet rwSet = getReadWriteSet(currentChoice);
1002           int objectId = fieldInfo.getClassInfo().getClassObjectRef();
1003           // Record the field in the map
1004           rwSet.addReadField(fieldClass, objectId);
1005         }
1006       }
1007     }
1008   }
1009
1010   private int checkAndAdjustChoice(int currentChoice, VM vm) {
1011     // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator
1012     // for certain method calls in the infrastructure, e.g., eventSince()
1013     ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
1014     // This is the main event CG
1015     if (currentCG instanceof IntIntervalGenerator) {
1016       // This is the interval CG used in device handlers
1017       ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
1018       // Iterate until we find the IntChoiceFromSet CG
1019       while (!(parentCG instanceof IntChoiceFromSet)) {
1020         parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator();
1021       }
1022       // Find the choice related to the IntIntervalGenerator CG from the map
1023       currentChoice = currentExecution.getChoiceFromCG((IntChoiceFromSet) parentCG);
1024     }
1025     return currentChoice;
1026   }
1027
1028   private void createBacktrackingPoint(int eventChoice, Execution conflictExecution, int conflictChoice) {
1029     // Create a new list of choices for backtrack based on the current choice and conflicting event number
1030     // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2}
1031     // for the original set {0, 1, 2, 3}
1032
1033     // eventChoice represents the event/transaction that will be put into the backtracking set of
1034     // conflictExecution/conflictChoice
1035     Integer[] newChoiceList = new Integer[refChoices.length];
1036     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
1037     int stateId = conflictTrace.get(conflictChoice).getStateId();
1038     // Check if this trace has been done from this state
1039     if (isTraceAlreadyConstructed(eventChoice, stateId)) {
1040       return;
1041     }
1042     // Put the conflicting event numbers first and reverse the order
1043     newChoiceList[0] = eventChoice;
1044     // Put the rest of the event numbers into the array starting from the minimum to the upper bound
1045     for (int i = 0, j = 1; i < refChoices.length; i++) {
1046       if (refChoices[i] != newChoiceList[0]) {
1047         newChoiceList[j] = refChoices[i];
1048         j++;
1049       }
1050     }
1051     // Predecessor of the new backtrack point is the same as the conflict point's
1052     addNewBacktrackPoint(stateId, newChoiceList, conflictTrace.get(conflictChoice));
1053   }
1054
1055   private boolean excludeThisForItContains(String[] excludedStrings, String className) {
1056     for (String excludedField : excludedStrings) {
1057       if (className.contains(excludedField)) {
1058         return true;
1059       }
1060     }
1061     return false;
1062   }
1063
1064   private boolean excludeThisForItEndsWith(String[] excludedStrings, String className) {
1065     for (String excludedField : excludedStrings) {
1066       if (className.endsWith(excludedField)) {
1067         return true;
1068       }
1069     }
1070     return false;
1071   }
1072
1073   private boolean excludeThisForItStartsWith(String[] excludedStrings, String className) {
1074     for (String excludedField : excludedStrings) {
1075       if (className.startsWith(excludedField)) {
1076         return true;
1077       }
1078     }
1079     return false;
1080   }
1081
1082   private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
1083                 // Check if we are reaching the end of our execution: no more backtracking points to explore
1084                 // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
1085                 if (!backtrackStateQ.isEmpty()) {
1086                         // Set done all the other backtrack points
1087                         for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
1088         backtrackTransition.getTransitionCG().setDone();
1089                         }
1090                         // Reset the next backtrack point with the latest state
1091                         int hiStateId = backtrackStateQ.peek();
1092                         // Restore the state first if necessary
1093                         if (vm.getStateId() != hiStateId) {
1094                                 RestorableVMState restorableState = restorableStateMap.get(hiStateId);
1095                                 vm.restoreState(restorableState);
1096                         }
1097                         // Set the backtrack CG
1098                         IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
1099                         setBacktrackCG(hiStateId, backtrackCG);
1100                 } else {
1101                         // Set done this last CG (we save a few rounds)
1102                         icsCG.setDone();
1103                 }
1104                 // Save all the visited states when starting a new execution of trace
1105                 prevVisitedStates.addAll(currVisitedStates.keySet());
1106                 // This marks a transitional period to the new CG
1107                 isEndOfExecution = true;
1108   }
1109
1110   private boolean isConflictFound(int eventChoice, Execution conflictExecution, int conflictChoice,
1111                                   ReadWriteSet currRWSet) {
1112     // conflictExecution/conflictChoice represent a predecessor event/transaction that can potentially have a conflict
1113     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
1114     HashMap<Integer, ReadWriteSet> confRWFieldsMap = conflictExecution.getReadWriteFieldsMap();
1115     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
1116     if (!confRWFieldsMap.containsKey(conflictChoice) || eventChoice == conflictTrace.get(conflictChoice).getChoice()) {
1117       return false;
1118     }
1119     // R/W set of choice/event that may have a potential conflict
1120     ReadWriteSet confRWSet = confRWFieldsMap.get(conflictChoice);
1121     // Check for conflicts with Read and Write fields for Write instructions
1122     Set<String> currWriteSet = currRWSet.getWriteSet();
1123     for(String writeField : currWriteSet) {
1124       int currObjId = currRWSet.writeFieldObjectId(writeField);
1125       if ((confRWSet.readFieldExists(writeField) && confRWSet.readFieldObjectId(writeField) == currObjId) ||
1126           (confRWSet.writeFieldExists(writeField) && confRWSet.writeFieldObjectId(writeField) == currObjId)) {
1127         // Remove this from the write set as we are tracking per memory location
1128         currRWSet.removeWriteField(writeField);
1129         return true;
1130       }
1131     }
1132     // Check for conflicts with Write fields for Read instructions
1133     Set<String> currReadSet = currRWSet.getReadSet();
1134     for(String readField : currReadSet) {
1135       int currObjId = currRWSet.readFieldObjectId(readField);
1136       if (confRWSet.writeFieldExists(readField) && confRWSet.writeFieldObjectId(readField) == currObjId) {
1137         // Remove this from the read set as we are tracking per memory location
1138         currRWSet.removeReadField(readField);
1139         return true;
1140       }
1141     }
1142     // Return false if no conflict is found
1143     return false;
1144   }
1145
1146   private boolean isFieldExcluded(Instruction executedInsn) {
1147     // Get the field info
1148     FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo();
1149     // Check if the non-relevant fields set already has it
1150     if (nonRelevantFields.contains(fieldInfo)) {
1151       return true;
1152     }
1153     // Check if the relevant fields set already has it
1154     if (relevantFields.contains(fieldInfo)) {
1155       return false;
1156     }
1157     // Analyze only after being initialized
1158     String field = fieldInfo.getFullName();
1159     // Check against "starts-with", "ends-with", and "contains" list
1160     if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) ||
1161             excludeThisForItEndsWith(EXCLUDED_FIELDS_ENDS_WITH_LIST, field) ||
1162             excludeThisForItContains(EXCLUDED_FIELDS_CONTAINS_LIST, field)) {
1163       nonRelevantFields.add(fieldInfo);
1164       return true;
1165     }
1166     relevantFields.add(fieldInfo);
1167     return false;
1168   }
1169
1170   // Check if this trace is already constructed
1171   private boolean isTraceAlreadyConstructed(int firstChoice, int stateId) {
1172     // Concatenate state ID and only the first event in the string, e.g., "1:1 for the trace 10234 at state 1"
1173     // Check if the trace has been constructed as a backtrack point for this state
1174     // TODO: THIS IS AN OPTIMIZATION!
1175     HashSet<Integer> choiceSet;
1176     if (doneBacktrackMap.containsKey(stateId)) {
1177       choiceSet = doneBacktrackMap.get(stateId);
1178       if (choiceSet.contains(firstChoice)) {
1179         return true;
1180       }
1181     } else {
1182       choiceSet = new HashSet<>();
1183       doneBacktrackMap.put(stateId, choiceSet);
1184     }
1185     choiceSet.add(firstChoice);
1186
1187     return false;
1188   }
1189
1190   private HashSet<Predecessor> getPredecessors(int stateId) {
1191     // Get a set of predecessors for this state ID
1192     HashSet<Predecessor> predecessors;
1193     if (stateToPredInfo.containsKey(stateId)) {
1194       PredecessorInfo predecessorInfo = stateToPredInfo.get(stateId);
1195       predecessors = predecessorInfo.getPredecessors();
1196     } else {
1197       predecessors = new HashSet<>();
1198     }
1199
1200     return predecessors;
1201   }
1202
1203   private ReadWriteSet getReadWriteSet(int currentChoice) {
1204     // Do the analysis to get Read and Write accesses to fields
1205     ReadWriteSet rwSet;
1206     // We already have an entry
1207     HashMap<Integer, ReadWriteSet> currReadWriteFieldsMap = currentExecution.getReadWriteFieldsMap();
1208     if (currReadWriteFieldsMap.containsKey(currentChoice)) {
1209       rwSet = currReadWriteFieldsMap.get(currentChoice);
1210     } else { // We need to create a new entry
1211       rwSet = new ReadWriteSet();
1212       currReadWriteFieldsMap.put(currentChoice, rwSet);
1213     }
1214     return rwSet;
1215   }
1216
1217   // Reset data structure for each new execution
1218   private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) {
1219     if (choices == null || choices != icsCG.getAllChoices()) {
1220       // Reset state variables
1221       choiceCounter = 0;
1222       choices = icsCG.getAllChoices();
1223       refChoices = copyChoices(choices);
1224       // Clear data structures
1225       currVisitedStates.clear();
1226       stateToEventMap.clear();
1227       isEndOfExecution = false;
1228     }
1229   }
1230
1231   // Set a backtrack point for a particular state
1232   private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) {
1233     // Set a backtrack CG based on a state ID
1234     LinkedList<BacktrackExecution> backtrackExecutions = backtrackMap.get(stateId);
1235     BacktrackExecution backtrackExecution = backtrackExecutions.removeLast();
1236     backtrackCG.setNewValues(backtrackExecution.getChoiceList());  // Get the last from the queue
1237     backtrackCG.setStateId(stateId);
1238     backtrackCG.reset();
1239     // Update current execution with this new execution
1240     Execution newExecution = new Execution();
1241     TransitionEvent firstTransition = backtrackExecution.getFirstTransition();
1242     newExecution.addTransition(firstTransition);
1243     // Try to free some memory since this map is only used for the current execution
1244     currentExecution.clearCGToChoiceMap();
1245     currentExecution = newExecution;
1246     // Remove from the queue if we don't have more backtrack points for that state
1247     if (backtrackExecutions.isEmpty()) {
1248       backtrackMap.remove(stateId);
1249       backtrackStateQ.remove(stateId);
1250     }
1251   }
1252
1253   // Update backtrack sets
1254   // 1) recursively, and
1255   // 2) track accesses per memory location (per shared variable/field)
1256   private void updateBacktrackSet(Execution execution, int currentChoice) {
1257     // Copy ReadWriteSet object
1258     HashMap<Integer, ReadWriteSet> currRWFieldsMap = execution.getReadWriteFieldsMap();
1259     ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice);
1260     if (currRWSet == null) {
1261       return;
1262     }
1263     currRWSet = currRWSet.getCopy();
1264     // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
1265     HashSet<TransitionEvent> visited = new HashSet<>();
1266     // Conflict TransitionEvent is essentially the current TransitionEvent
1267     TransitionEvent confTrans = execution.getExecutionTrace().get(currentChoice);
1268     // Update backtrack set recursively
1269     updateBacktrackSetDFS(execution, currentChoice, confTrans.getChoice(), currRWSet, visited);
1270   }
1271
1272   private void updateBacktrackSetDFS(Execution execution, int currentChoice, int conflictEventChoice,
1273                                      ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
1274     TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
1275     // Record this transition into the state summary of main summary
1276     currRWSet = mainSummary.updateStateSummary(currTrans.getStateId(), conflictEventChoice, currRWSet);
1277     // Halt when we have visited this transition (in a cycle)
1278     if (visited.contains(currTrans)) {
1279       return;
1280     }
1281     visited.add(currTrans);
1282     // Check the predecessors only if the set is not empty
1283     if (!currRWSet.isEmpty()) {
1284       // Explore all predecessors
1285       for (Predecessor predecessor : getPredecessors(currTrans.getStateId())) {
1286         // Get the predecessor (previous conflict choice)
1287         int predecessorChoice = predecessor.getChoice();
1288         Execution predecessorExecution = predecessor.getExecution();
1289         // Push up one happens-before transition
1290         int newConflictEventChoice = conflictEventChoice;
1291         // Check if a conflict is found
1292         ReadWriteSet newCurrRWSet = currRWSet.getCopy();
1293         if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) {
1294           createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
1295           // We need to extract the pushed happens-before event choice from the predecessor execution and choice
1296           newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
1297         }
1298         // Continue performing DFS if conflict is not found
1299         updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
1300                 newCurrRWSet, visited);
1301       }
1302     }
1303   }
1304
1305   // --- Functions related to the reachability analysis when there is a state match
1306
1307   private void addPredecessorToRevisitedState(int stateId) {
1308     // Perform this analysis only when:
1309     // 1) this is not during a switch to a new execution,
1310     // 2) at least 2 choices/events have been explored (choiceCounter > 1),
1311     // 3) state > 0 (state 0 is for boolean CG)
1312     if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
1313       if ((currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) ||
1314               prevVisitedStates.contains(stateId)) {
1315         // Record a new predecessor for a revisited state
1316         addPredecessors(stateId);
1317       }
1318     }
1319   }
1320
1321   // Update the backtrack sets from previous executions
1322   private void updateBacktrackSetsFromGraph(int stateId, Execution currExecution, int currChoice) {
1323     // Get events/choices at this state ID
1324     Set<Integer> eventChoicesAtStateId = mainSummary.getEventChoicesAtStateId(stateId);
1325     for (Integer eventChoice : eventChoicesAtStateId) {
1326       // Get the ReadWriteSet object for this event at state ID
1327       ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId);
1328       // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
1329       HashSet<TransitionEvent> visited = new HashSet<>();
1330       // Update the backtrack sets recursively
1331       updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited);
1332     }
1333   }
1334 }