New algorithm implementation; without pushing forward hb transaction; untested/undebu...
authorrtrimana <rtrimana@uci.edu>
Fri, 5 Jun 2020 20:45:40 +0000 (13:45 -0700)
committerrtrimana <rtrimana@uci.edu>
Fri, 5 Jun 2020 20:45:40 +0000 (13:45 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index bc42a46..f503dfa 100644 (file)
@@ -34,19 +34,9 @@ import java.util.*;
 import java.util.logging.Logger;
 import java.io.IOException;
 
-// TODO: Fix for Groovy's model-checking
-// TODO: This is a setter to change the values of the ChoiceGenerator to implement POR
 /**
- * Simple tool to log state changes.
- *
- * This DPOR implementation is augmented by the algorithm presented in this SPIN paper:
- * http://spinroot.com/spin/symposia/ws08/spin2008_submission_33.pdf
- *
- * The algorithm is presented on page 11 of the paper. Basically, we have a graph G
- * (i.e., visible operation dependency graph).
- * This DPOR implementation actually fixes the algorithm in the SPIN paper that does not
- * consider cases where a state could be matched early. In this new algorithm/implementation,
- * each run is terminated iff:
+ * This a DPOR implementation for event-driven applications with loops that create cycles of state matching
+ * In this new DPOR algorithm/implementation, each run is terminated iff:
  * - we find a state that matches a state in a previous run, or
  * - we have a matched state in the current run that consists of cycles that contain all choices/events.
  */
@@ -80,7 +70,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
   private HashMap<Integer, Integer> stateToChoiceCounterMap;      // Maps state IDs to the choice counter
-  private HashMap<Integer, ArrayList<Execution>> rGraph;          // Create a reachability graph for past executions
+  private HashMap<Integer, HashSet<TransitionEvent>> rGraph;      // Reachability graph for past executions
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -151,6 +141,8 @@ public class DPORStateReducer extends ListenerAdapter {
               " which is " + detail + " Transition: " + transition + "\n");
     }
     if (stateReductionMode) {
+      // Only add a transition into R-Graph when it advances the state
+      addTransitionToRGRaph();
       updateStateInfo(search);
     }
   }
@@ -245,7 +237,9 @@ public class DPORStateReducer extends ListenerAdapter {
         // If this is a new CG then we need to update data structures
         resetStatesForNewExecution(icsCG, vm);
         // If we don't see a fair scheduling of events/choices then we have to enforce it
-        fairSchedulingAndBacktrackPoint(icsCG, vm);
+        fairSchedulingAndTransition(icsCG, vm);
+        // Update backtrack set of an executed event (transition): one transition before this one
+        updateBacktrackSet(currentExecution, choiceCounter - 1);
         // Explore the next backtrack point: 
         // 1) if we have seen this state or this state contains cycles that involve all events, and
         // 2) after the current CG is advanced at least once
@@ -288,16 +282,6 @@ public class DPORStateReducer extends ListenerAdapter {
             // Handle the read/write accesses that occur through iterators
             analyzeReadWriteAccesses(executedInsn, ti, currentChoice);
           }
-          // Analyze conflicts from next instructions
-          if (nextInsn instanceof JVMFieldInstruction) {
-            // Skip the constructor because it is called once and does not have shared access with other objects
-            if (!nextInsn.getMethodInfo().getName().equals("<init>")) {
-              String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
-              if (!isFieldExcluded(fieldClass)) {
-                findFirstConflictAndCreateBacktrackPoint(currentChoice, nextInsn, fieldClass);
-              }
-            }
-          }
         }
       }
     }
@@ -310,67 +294,44 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // This class compactly stores backtrack execution:
   // 1) backtrack choice list, and
-  // 2) backtrack execution
+  // 2) first backtrack point (linking with predecessor execution)
   private class BacktrackExecution {
     private Integer[] choiceList;
-    private Execution execution;
+    private TransitionEvent firstTransition;
 
-    public BacktrackExecution(Integer[] choList, Execution exec) {
+    public BacktrackExecution(Integer[] choList, TransitionEvent fTransition) {
       choiceList = choList;
-      execution = exec;
+      firstTransition = fTransition;
     }
 
     public Integer[] getChoiceList() {
       return choiceList;
     }
 
-    public Execution getExecution() {
-      return execution;
-    }
-  }
-
-  // This class compactly stores backtrack points:
-  // 1) backtrack state ID, and
-  // 2) backtracking choices
-  private class BacktrackPoint {
-    private IntChoiceFromSet backtrackCG; // CG at this backtrack point
-    private int stateId;                  // State at this backtrack point
-    private int choice;                   // Choice chosen at this backtrack point
-
-    public BacktrackPoint(IntChoiceFromSet cg, int stId, int cho) {
-      backtrackCG = cg;
-      stateId = stId;
-      choice = cho;
-    }
-
-    public IntChoiceFromSet getBacktrackCG() { return backtrackCG; }
-
-    public int getStateId() {
-      return stateId;
-    }
-
-    public int getChoice() {
-      return choice;
+    public TransitionEvent getFirstTransition() {
+      return firstTransition;
     }
   }
 
   // This class stores a representation of the execution graph node
+  // TODO: We can modify this class to implement some optimization (e.g., clock-vector)
+  // TODO: We basically need to keep track of:
+  // TODO:    (1) last read/write access to each memory location
+  // TODO:    (2) last state with two or more incoming events (transitions)
   private class Execution {
     private HashMap<IntChoiceFromSet, Integer> cgToChoiceMap;   // Map between CG to choice numbers for O(1) access
-    private ArrayList<BacktrackPoint> executionTrace;           // The BacktrackPoint objects of this execution
-    private int parentChoice;                                   // The parent's choice that leads to this execution
-    private Execution parent;                                   // Store the parent for backward DFS to find conflicts
+    private ArrayList<TransitionEvent> executionTrace;           // The BacktrackPoint objects of this execution
     private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;  // Record fields that are accessed
+    private HashMap<Integer, TransitionEvent> stateToTransitionMap;  // For O(1) access to backtrack point
 
     public Execution() {
       cgToChoiceMap = new HashMap<>();
       executionTrace = new ArrayList<>();
-      parentChoice = -1;
-      parent = null;
       readWriteFieldsMap = new HashMap<>();
+      stateToTransitionMap = new HashMap<>();
     }
 
-    public void addBacktrackPoint(BacktrackPoint newBacktrackPoint) {
+    public void addTransition(TransitionEvent newBacktrackPoint) {
       executionTrace.add(newBacktrackPoint);
     }
 
@@ -378,36 +339,133 @@ public class DPORStateReducer extends ListenerAdapter {
       cgToChoiceMap = null;
     }
 
-    public ArrayList<BacktrackPoint> getExecutionTrace() {
-      return executionTrace;
+    public TransitionEvent getTransitionFromState(int stateId) {
+      if (stateToTransitionMap.containsKey(stateId)) {
+        return stateToTransitionMap.get(stateId);
+      }
+      return null;
     }
 
     public int getChoiceFromCG(IntChoiceFromSet icsCG) {
       return cgToChoiceMap.get(icsCG);
     }
 
-    public int getParentChoice() {
-      return parentChoice;
-    }
-
-    public Execution getParent() {
-      return parent;
+    public ArrayList<TransitionEvent> getExecutionTrace() {
+      return executionTrace;
     }
 
     public HashMap<Integer, ReadWriteSet> getReadWriteFieldsMap() {
       return readWriteFieldsMap;
     }
 
+    public TransitionEvent getFirstTransition() {
+      return executionTrace.get(0);
+    }
+
+    public TransitionEvent getLastTransition() {
+      return executionTrace.get(executionTrace.size() - 1);
+    }
+
+    public boolean isNew() {
+      return executionTrace.size() == 1;
+    }
+
     public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) {
       cgToChoiceMap.put(icsCG, choice);
     }
 
-    public void setParentChoice(int parChoice) {
-      parentChoice = parChoice;
+    public void mapStateToTransition(int stateId, TransitionEvent backtrackPoint) {
+      stateToTransitionMap.put(stateId, backtrackPoint);
+    }
+  }
+
+  // This class compactly stores a predecessor
+  // 1) a predecessor execution
+  // 2) the predecessor choice in that predecessor execution
+  private class Predecessor {
+    private int predecessorChoice;           // Predecessor choice
+    private Execution predecessorExecution;  // Predecessor execution
+
+    public Predecessor(int predChoice, Execution predExec) {
+      predecessorChoice = predChoice;
+      predecessorExecution = predExec;
+    }
+
+    public int getPredecessorChoice() {
+      return predecessorChoice;
+    }
+
+    public Execution getPredecessorExecution() {
+      return predecessorExecution;
+    }
+  }
+
+  // This class compactly stores backtrack points:
+  // 1) CG,
+  // 2) state ID,
+  // 3) choice,
+  // 4) predecessors (for backward DFS).
+  private class TransitionEvent {
+    private IntChoiceFromSet transitionCG;     // CG at this transition
+    private int stateId;                       // State at this transition
+    private int choice;                        // Choice chosen at this transition
+    private Execution execution;               // The execution where this transition belongs
+    private int choiceCounter;                 // Choice counter at this transition
+    private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
+
+    public TransitionEvent() {
+      transitionCG = null;
+      stateId = -1;
+      choice = -1;
+      execution = null;
+      choiceCounter = -1;
+      predecessors = new HashSet<>();
+    }
+
+    public void setTransitionCG(IntChoiceFromSet cg) {
+      transitionCG = cg;
+    }
+
+    public void setStateId(int stId) {
+      stateId = stId;
     }
 
-    public void setParent(Execution par) {
-      parent = par;
+    public void setChoice(int cho) {
+      choice = cho;
+    }
+
+    public void setChoiceCounter(int choCounter) {
+      choiceCounter = choCounter;
+    }
+
+    public IntChoiceFromSet getTransitionCG() { return transitionCG; }
+
+    public int getStateId() {
+      return stateId;
+    }
+
+    public int getChoice() {
+      return choice;
+    }
+
+    public int getChoiceCounter() {
+      return choiceCounter;
+    }
+
+    public void setExecution(Execution exec) {
+      execution = exec;
+    }
+
+    public Execution getExecution() {
+      return execution;
+    }
+
+    public HashSet<Predecessor> getPredecessors() {
+      return predecessors;
+    }
+
+    public void recordPredecessor(Execution execution, int choice) {
+      predecessors.add(new Predecessor(choice, execution));
     }
   }
 
@@ -415,44 +473,80 @@ public class DPORStateReducer extends ListenerAdapter {
   // We store the field name and its object ID
   // Sharing the same field means the same field name and object ID
   private class ReadWriteSet {
-    private HashMap<String, Integer> readSet;
-    private HashMap<String, Integer> writeSet;
+    private HashMap<String, Integer> readMap;
+    private HashMap<String, Integer> writeMap;
 
     public ReadWriteSet() {
-      readSet = new HashMap<>();
-      writeSet = new HashMap<>();
+      readMap = new HashMap<>();
+      writeMap = new HashMap<>();
     }
 
     public void addReadField(String field, int objectId) {
-      readSet.put(field, objectId);
+      readMap.put(field, objectId);
     }
 
     public void addWriteField(String field, int objectId) {
-      writeSet.put(field, objectId);
+      writeMap.put(field, objectId);
+    }
+
+    public void removeReadField(String field) {
+      readMap.remove(field);
+    }
+
+    public void removeWriteField(String field) {
+      writeMap.remove(field);
+    }
+
+    public boolean isEmpty() {
+      return readMap.isEmpty() && writeMap.isEmpty();
+    }
+
+    public ReadWriteSet getCopy() {
+      ReadWriteSet copyRWSet = new ReadWriteSet();
+      // Copy the maps in the set into the new object copy
+      copyRWSet.setReadMap(new HashMap<>(this.getReadMap()));
+      copyRWSet.setWriteMap(new HashMap<>(this.getWriteMap()));
+      return copyRWSet;
     }
 
     public Set<String> getReadSet() {
-      return readSet.keySet();
+      return readMap.keySet();
     }
 
     public Set<String> getWriteSet() {
-      return writeSet.keySet();
+      return writeMap.keySet();
     }
 
     public boolean readFieldExists(String field) {
-      return readSet.containsKey(field);
+      return readMap.containsKey(field);
     }
 
     public boolean writeFieldExists(String field) {
-      return writeSet.containsKey(field);
+      return writeMap.containsKey(field);
     }
 
     public int readFieldObjectId(String field) {
-      return readSet.get(field);
+      return readMap.get(field);
     }
 
     public int writeFieldObjectId(String field) {
-      return writeSet.get(field);
+      return writeMap.get(field);
+    }
+
+    private HashMap<String, Integer> getReadMap() {
+      return readMap;
+    }
+
+    private HashMap<String, Integer> getWriteMap() {
+      return writeMap;
+    }
+
+    private void setReadMap(HashMap<String, Integer> rMap) {
+      readMap = rMap;
+    }
+
+    private void setWriteMap(HashMap<String, Integer> wMap) {
+      writeMap = wMap;
     }
   }
 
@@ -477,7 +571,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private final static String JAVA_STRING_LIB = "java.lang.String";
 
   // -- FUNCTIONS
-  private void fairSchedulingAndBacktrackPoint(IntChoiceFromSet icsCG, VM vm) {
+  private void fairSchedulingAndTransition(IntChoiceFromSet icsCG, VM vm) {
     // Check the next choice and if the value is not the same as the expected then force the expected value
     int choiceIndex = choiceCounter % refChoices.length;
     int nextChoice = icsCG.getNextChoice();
@@ -488,9 +582,25 @@ public class DPORStateReducer extends ListenerAdapter {
         icsCG.setChoice(currCGIndex, expectedChoice);
       }
     }
-    // Record state ID and choice/event as backtrack point
+    // Get state ID and associate it with this transition
     int stateId = vm.getStateId();
-    currentExecution.addBacktrackPoint(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));
+    // Get a new transition
+    TransitionEvent transition;
+    if (currentExecution.isNew()) {
+      // We need to handle the first transition differently because this has a predecessor execution
+      transition = currentExecution.getFirstTransition();
+    } else {
+      transition = new TransitionEvent();
+      transition.recordPredecessor(currentExecution, choiceCounter - 1);
+    }
+    transition.setExecution(currentExecution);
+    transition.setTransitionCG(icsCG);
+    transition.setStateId(stateId);
+    transition.setChoice(refChoices[choiceIndex]);
+    transition.setChoiceCounter(choiceCounter);
+    // Add new transition to the current execution
+    currentExecution.mapStateToTransition(stateId, transition);
+    currentExecution.addTransition(transition);
     currentExecution.mapCGToChoice(icsCG, choiceCounter);
     // Store restorable state object for this state (always store the latest)
     RestorableVMState restorableState = vm.getRestorableState();
@@ -512,7 +622,7 @@ public class DPORStateReducer extends ListenerAdapter {
   // (2) the state has one or more cycles that involve all the events
   // With simple approach we only need to check for a re-visited state.
   // Basically, we have to check that we have executed all events between two occurrences of such state.
-  private boolean containsCyclesWithAllEvents(int stId) {
+  private boolean completeFullCycle(int stId) {
 
     // False if the state ID hasn't been recorded
     if (!stateToEventMap.containsKey(stId)) {
@@ -544,6 +654,7 @@ public class DPORStateReducer extends ListenerAdapter {
     backtrackMap = new HashMap<>();
     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
     currentExecution = new Execution();
+    currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
     doneBacktrackSet = new HashSet<>();
     stateToChoiceCounterMap = new HashMap<>();
     rGraph = new HashMap<>();
@@ -561,20 +672,23 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  private void saveExecutionToRGraph(int stateId) {
-    // Save execution state into the reachability graph only if
-    // (1) It is not a revisited state from a past execution, or
-    // (2) It is just a new backtracking point
-    if (!prevVisitedStates.contains(stateId) ||
-            choiceCounter <= 1) {
-      ArrayList<Execution> reachableExecutions;
-      if (!prevVisitedStates.contains(stateId)) {
-        reachableExecutions = new ArrayList<>();
-        rGraph.put(stateId, reachableExecutions);
-      } else {
-        reachableExecutions = rGraph.get(stateId);
-      }
-      reachableExecutions.add(currentExecution);
+  // Save the current transition into R-Graph
+  // Basically the current transition is reachable from the final state of the previous transition in this execution
+  private void addTransitionToRGRaph() {
+    // Get the current transition
+    TransitionEvent currTrans = currentExecution.getLastTransition();
+    // This transition is reachable from this source state when it has advanced the state
+    int stateId = currTrans.getStateId();
+    // Add transition into R-Graph
+    HashSet<TransitionEvent> transitionSet;
+    if (rGraph.containsKey(stateId)) {
+      transitionSet = rGraph.get(stateId);
+    } else {
+      transitionSet = new HashSet<>();
+    }
+    // Insert into the set if it does not contain it yet
+    if (!transitionSet.contains(currTrans)) {
+      transitionSet.add(currTrans);
     }
   }
 
@@ -582,7 +696,7 @@ public class DPORStateReducer extends ListenerAdapter {
     // We need to check all the states that have just been visited
     // Often a transition (choice/event) can result into forwarding/backtracking to a number of states
     for(Integer stateId : justVisitedStates) {
-      if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
+      if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
         return true;
       }
     }
@@ -598,7 +712,6 @@ public class DPORStateReducer extends ListenerAdapter {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
-    saveExecutionToRGraph(stateId);
     analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
     stateToChoiceCounterMap.put(stateId, choiceCounter);
     justVisitedStates.add(stateId);
@@ -617,10 +730,9 @@ public class DPORStateReducer extends ListenerAdapter {
       backtrackMap.put(stateId, backtrackExecList);
     }
     // Add the new backtrack execution object
-    Execution newExecution = new Execution();
-    newExecution.setParent(parentExecution);
-    newExecution.setParentChoice(parentChoice);
-    backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, newExecution));
+    TransitionEvent backtrackTransition = new TransitionEvent();
+    backtrackTransition.recordPredecessor(parentExecution, parentChoice);
+    backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition));
     // Add to priority queue
     if (!backtrackStateQ.contains(stateId)) {
       backtrackStateQ.add(stateId);
@@ -705,27 +817,26 @@ public class DPORStateReducer extends ListenerAdapter {
     return currentChoice;
   }
 
-  private void createBacktrackingPoint(int backtrackChoice, int conflictChoice, Execution execution) {
+  private void createBacktrackingPoint(Execution execution, int currentChoice, int conflictChoice) {
 
     // Create a new list of choices for backtrack based on the current choice and conflicting event number
     // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2}
     // for the original set {0, 1, 2, 3}
     Integer[] newChoiceList = new Integer[refChoices.length];
     //int firstChoice = choices[actualChoice];
-    ArrayList<BacktrackPoint> pastTrace = execution.getExecutionTrace();
-    ArrayList<BacktrackPoint> currTrace = currentExecution.getExecutionTrace();
-    int btrackChoice = currTrace.get(backtrackChoice).getChoice();
+    ArrayList<TransitionEvent> pastTrace = execution.getExecutionTrace();
+    ArrayList<TransitionEvent> currTrace = currentExecution.getExecutionTrace();
+    int currChoice = currTrace.get(currentChoice).getChoice();
     int stateId = pastTrace.get(conflictChoice).getStateId();
     // Check if this trace has been done from this state
-    if (isTraceAlreadyConstructed(btrackChoice, stateId)) {
+    if (isTraceAlreadyConstructed(currChoice, stateId)) {
       return;
     }
     // Put the conflicting event numbers first and reverse the order
-    newChoiceList[0] = btrackChoice;
-    newChoiceList[1] = pastTrace.get(conflictChoice).getChoice();
+    newChoiceList[0] = currChoice;
     // Put the rest of the event numbers into the array starting from the minimum to the upper bound
-    for (int i = 0, j = 2; i < refChoices.length; i++) {
-      if (refChoices[i] != newChoiceList[0] && refChoices[i] != newChoiceList[1]) {
+    for (int i = 0, j = 1; i < refChoices.length; i++) {
+      if (refChoices[i] != newChoiceList[0]) {
         newChoiceList[j] = refChoices[i];
         j++;
       }
@@ -767,8 +878,8 @@ public class DPORStateReducer extends ListenerAdapter {
                // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
                if (!backtrackStateQ.isEmpty()) {
                        // Set done all the other backtrack points
-                       for (BacktrackPoint backtrackPoint : currentExecution.getExecutionTrace()) {
-                               backtrackPoint.getBacktrackCG().setDone();
+                       for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
+        backtrackTransition.getTransitionCG().setDone();
                        }
                        // Reset the next backtrack point with the latest state
                        int hiStateId = backtrackStateQ.peek();
@@ -790,64 +901,49 @@ public class DPORStateReducer extends ListenerAdapter {
                isEndOfExecution = true;
   }
 
-  private void findFirstConflictAndCreateBacktrackPoint(int currentChoice, Instruction nextInsn, String fieldClass) {
-    // Check for conflict (go backward from current choice and get the first conflict)
-    Execution execution = currentExecution;
-    // Choice/event we want to check for conflict against (start from actual choice)
-    int pastChoice = currentChoice;
-    // Perform backward DFS through the execution graph
-    while (true) {
-      // Get the next conflict choice
-      if (pastChoice > 0) {
-        // Case #1: check against a previous choice in the same execution for conflict
-        pastChoice = pastChoice - 1;
-      } else { // pastChoice == 0 means we are at the first BacktrackPoint of this execution path
-        // Case #2: check against a previous choice in a parent execution
-        int parentChoice = execution.getParentChoice();
-        if (parentChoice > -1) {
-          // Get the parent execution
-          execution = execution.getParent();
-          pastChoice = execution.getParentChoice();
-        } else {
-          // If parent is -1 then this is the first execution (it has no parent) and we stop here
-          break;
-        }
-      }
-      // Check if a conflict is found
-      if (isConflictFound(nextInsn, fieldClass, currentChoice, pastChoice, execution)) {
-        createBacktrackingPoint(currentChoice, pastChoice, execution);
-        break;  // Stop at the first found conflict
-      }
-    }
-  }
+  private boolean isConflictFound(Execution execution, int reachableChoice, int conflictChoice,
+                                  ReadWriteSet currRWSet) {
 
-  private boolean isConflictFound(Instruction nextInsn, String fieldClass, int currentChoice,
-                                  int pastChoice, Execution pastExecution) {
-
-    HashMap<Integer, ReadWriteSet> pastRWFieldsMap = pastExecution.getReadWriteFieldsMap();
-    ArrayList<BacktrackPoint> pastTrace = pastExecution.getExecutionTrace();
-    ArrayList<BacktrackPoint> currTrace = currentExecution.getExecutionTrace();
+    ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
+    HashMap<Integer, ReadWriteSet> execRWFieldsMap = execution.getReadWriteFieldsMap();
     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
-    if (!pastRWFieldsMap.containsKey(pastChoice) ||
-            currTrace.get(currentChoice).getChoice() == pastTrace.get(pastChoice).getChoice()) {
+    if (!execRWFieldsMap.containsKey(conflictChoice) ||
+            executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) {
       return false;
     }
-    HashMap<Integer, ReadWriteSet> currRWFieldsMap = pastExecution.getReadWriteFieldsMap();
-    ReadWriteSet rwSet = currRWFieldsMap.get(pastChoice);
-    int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
-    // Check for conflicts with Write fields for both Read and Write instructions
-    if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
-            rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
-            (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
-                    rwSet.readFieldObjectId(fieldClass) == currObjId)) {
-      return true;
+    // R/W set of choice/event that may have a potential conflict
+    ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice);
+    // Check for conflicts with Read and Write fields for Write instructions
+    Set<String> currWriteSet = currRWSet.getWriteSet();
+    for(String writeField : currWriteSet) {
+      int currObjId = currRWSet.writeFieldObjectId(writeField);
+      if (evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) {
+        // Remove this from the read set as we are tracking per memory location
+        evtRWSet.removeWriteField(writeField);
+        return true;
+      } else if (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId) {
+        // Remove this from the write set as we are tracking per memory location
+        evtRWSet.removeReadField(writeField);
+        return true;
+      }
+    }
+    // Check for conflicts with Write fields for Read instructions
+    Set<String> currReadSet = currRWSet.getReadSet();
+    for(String readField : currReadSet) {
+      int currObjId = currRWSet.readFieldObjectId(readField);
+      if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) {
+        // Remove this from the write set as we are tracking per memory location
+        evtRWSet.removeWriteField(readField);
+        return true;
+      }
     }
+    // Return false if no conflict is found
     return false;
   }
 
-  private boolean isConflictFound(int reachableChoice, int conflictChoice, Execution execution) {
+  private boolean isConflictFound(Execution execution, int reachableChoice, int conflictChoice) {
 
-    ArrayList<BacktrackPoint> executionTrace = execution.getExecutionTrace();
+    ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
     HashMap<Integer, ReadWriteSet> execRWFieldsMap = execution.getReadWriteFieldsMap();
     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
     if (!execRWFieldsMap.containsKey(conflictChoice) ||
@@ -947,12 +1043,9 @@ public class DPORStateReducer extends ListenerAdapter {
     backtrackCG.setStateId(stateId);
     backtrackCG.reset();
     // Update current execution with this new execution
-    Execution newExecution = backtrackExecution.getExecution();
-    if (newExecution.getParentChoice() == -1) {
-      // If it is -1 then that means we should start from the end of the parent trace for backward DFS
-      ArrayList<BacktrackPoint> parentTrace = newExecution.getParent().getExecutionTrace();
-      newExecution.setParentChoice(parentTrace.size() - 1);
-    }
+    Execution newExecution = new Execution();
+    TransitionEvent firstTransition = backtrackExecution.getFirstTransition();
+    newExecution.addTransition(firstTransition);
     // Try to free some memory since this map is only used for the current execution
     currentExecution.clearCGToChoiceMap();
     currentExecution = newExecution;
@@ -963,142 +1056,81 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // --- Functions related to the reachability analysis when there is a state match
+  // Update backtrack sets
+  // 1) recursively, and
+  // 2) track accesses per memory location (per shared variable/field)
+  private void updateBacktrackSet(Execution execution, int currentChoice) {
+    // Choice/event we want to check for conflict against (start from actual choice)
+    int conflictChoice = currentChoice;
+    // Copy ReadWriteSet object
+    HashMap<Integer, ReadWriteSet> currRWFieldsMap = execution.getReadWriteFieldsMap();
+    ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice).getCopy();
+    // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
+    HashSet<TransitionEvent> visited = new HashSet<>();
+    // Update backtrack set recursively
+    updateBacktrackSetRecursive(execution, currentChoice, conflictChoice, currRWSet, visited);
+  }
 
-  // TODO: OPTIMIZATION!
-  // Check and make sure that state ID and choice haven't been explored for this trace
-  private boolean isAlreadyChecked(HashSet<String> checkedStateIdAndChoice, BacktrackPoint backtrackPoint) {
-    int stateId = backtrackPoint.getStateId();
-    int choice = backtrackPoint.getChoice();
-    StringBuilder sb = new StringBuilder();
-    sb.append(stateId);
-    sb.append(':');
-    sb.append(choice);
-    // Check if the trace has been constructed as a backtrack point for this state
-    if (checkedStateIdAndChoice.contains(sb.toString())) {
-      return true;
+  private void updateBacktrackSetRecursive(Execution execution, int currentChoice, int conflictChoice,
+                                           ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
+    // Halt when we have found the first read/write conflicts for all memory locations
+    if (currRWSet.isEmpty()) {
+      return;
+    }
+    TransitionEvent confTrans = execution.getExecutionTrace().get(conflictChoice);
+    // Halt when we have visited this transition (in a cycle)
+    if (visited.contains(confTrans)) {
+      return;
+    }
+    visited.add(confTrans);
+    // Explore all predecessors
+    for (Predecessor predecessor : confTrans.getPredecessors()) {
+      // Get the predecessor (previous conflict choice)
+      conflictChoice = predecessor.getPredecessorChoice();
+      execution = predecessor.getPredecessorExecution();
+      // Check if a conflict is found
+      if (isConflictFound(execution, currentChoice, conflictChoice, currRWSet)) {
+        createBacktrackingPoint(execution, currentChoice, conflictChoice);
+      }
+      // Continue performing DFS if conflict is not found
+      updateBacktrackSetRecursive(execution, currentChoice, conflictChoice, currRWSet, visited);
     }
-    checkedStateIdAndChoice.add(sb.toString());
-    return false;
   }
 
-  // We use backtrackPointsList to analyze the reachable states/events when there is a state match:
-  // 1) Whenever there is state match, there is a cycle of events
-  // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
-  // 3) Then we create a new backtrack point for every new conflict
+  // --- Functions related to the reachability analysis when there is a state match
+
   private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
     // Perform this analysis only when:
     // 1) there is a state match,
     // 2) this is not during a switch to a new execution,
     // 3) at least 2 choices/events have been explored (choiceCounter > 1),
-    // 4) the matched state has been encountered in the current execution, and
-    // 5) state > 0 (state 0 is for boolean CG)
+    // 4) state > 0 (state 0 is for boolean CG)
     if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && (stateId > 0)) {
       if (currVisitedStates.contains(stateId)) {
-        // Update the backtrack sets in the cycle
-        updateBacktrackSetsInCycle(stateId);
+        // Get the backtrack point from the current execution
+        TransitionEvent transition = currentExecution.getTransitionFromState(stateId);
+        transition.recordPredecessor(currentExecution, choiceCounter - 1);
+        updateBacktrackSetsFromPreviousExecution(stateId);
       } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
-        // Update the backtrack sets in a previous execution
-        updateBacktrackSetsInPreviousExecutions(stateId);
-      }
-    }
-  }
-
-  // Get the start event for the past execution trace when there is a state matched from a past execution
-  private int getPastConflictChoice(int stateId, ArrayList<BacktrackPoint> pastBacktrackPointList) {
-    // Iterate and find the first occurrence of the state ID
-    // It is guaranteed that a choice should be found because the state ID is in the list
-    int pastConfChoice = 0;
-    for(int i = 0; i<pastBacktrackPointList.size(); i++) {
-      BacktrackPoint backtrackPoint = pastBacktrackPointList.get(i);
-      int stId = backtrackPoint.getStateId();
-      if (stId == stateId) {
-        pastConfChoice = i;
-        break;
-      }
-    }
-    return pastConfChoice;
-  }
-
-  // Get a sorted list of reachable state IDs starting from the input stateId
-  private ArrayList<Integer> getReachableStateIds(Set<Integer> stateIds, int stateId) {
-    // Only include state IDs equal or greater than the input stateId: these are reachable states
-    ArrayList<Integer> sortedStateIds = new ArrayList<>();
-    for(Integer stId : stateIds) {
-      if (stId >= stateId) {
-        sortedStateIds.add(stId);
-      }
-    }
-    Collections.sort(sortedStateIds);
-    return sortedStateIds;
-  }
-
-  // Update the backtrack sets in the cycle
-  private void updateBacktrackSetsInCycle(int stateId) {
-    // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
-    int reachableChoice = stateToChoiceCounterMap.get(stateId);
-    int cycleEndChoice = choiceCounter - 1;
-    // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
-    while (reachableChoice < cycleEndChoice) {
-      for (int conflictChoice = reachableChoice + 1; conflictChoice <= cycleEndChoice; conflictChoice++) {
-        if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) {
-          createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution);
-        }
-      }
-      reachableChoice++;
-    }
-  }
-
-  // Update the backtrack sets in a previous execution
-  private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId,
-                                                      HashSet<String> checkedStateIdAndChoice) {
-    // Find the choice/event that marks the start of the subtrace from the previous execution
-    ArrayList<BacktrackPoint> pastExecutionTrace = rExecution.getExecutionTrace();
-    HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap();
-    int pastConfChoice = getPastConflictChoice(stateId, pastExecutionTrace);
-    int reachableChoice = choiceCounter;
-    // Iterate from the starting point until the end of the past execution trace
-    while (pastConfChoice < pastExecutionTrace.size() - 1) {  // BacktrackPoint list always has a surplus of 1
-      // Get the info of the event from the past execution trace
-      BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);
-      if (!isAlreadyChecked(checkedStateIdAndChoice, confBtrackPoint)) {
-        ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
-        // Append this event to the current list and map
-        ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
-        HashMap<Integer, ReadWriteSet> currRWFieldsMap = currentExecution.getReadWriteFieldsMap();
-        currentTrace.add(confBtrackPoint);
-        currRWFieldsMap.put(choiceCounter, rwSet);
-        for (int conflictChoice = reachableChoice - 1; conflictChoice >= 0; conflictChoice--) {
-          if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) {
-            createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution);
-          }
+        // Update past executions with a predecessor
+        HashSet<TransitionEvent> reachableTransitions = rGraph.get(stateId);
+        for(TransitionEvent transition : reachableTransitions) {
+          Execution execution = transition.getExecution();
+          transition.recordPredecessor(execution, choiceCounter - 1);
         }
-        // Remove this event to replace it with a new one
-        currentTrace.remove(currentTrace.size() - 1);
-        currRWFieldsMap.remove(choiceCounter);
+        updateBacktrackSetsFromPreviousExecution(stateId);
       }
-      pastConfChoice++;
     }
   }
 
-  // Update the backtrack sets in previous executions
-  private void updateBacktrackSetsInPreviousExecutions(int stateId) {
-    // Don't check a past trace twice!
-    HashSet<Execution> checkedTrace = new HashSet<>();
-    // Don't check the same event twice for a revisited state
-    HashSet<String> checkedStateIdAndChoice = new HashSet<>();
-    // Get sorted reachable state IDs
-    ArrayList<Integer> reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId);
-    // Iterate from this state ID until the biggest state ID
-    for(Integer stId : reachableStateIds) {
-      // Find the right reachability graph object that contains the stateId
-      ArrayList<Execution> rExecutions = rGraph.get(stId);
-      for (Execution rExecution : rExecutions) {
-        if (!checkedTrace.contains(rExecution)) {
-          updateBacktrackSetsInPreviousExecution(rExecution, stateId, checkedStateIdAndChoice);
-          checkedTrace.add(rExecution);
-        }
-      }
+  // Update the backtrack sets from previous executions
+  private void updateBacktrackSetsFromPreviousExecution(int stateId) {
+    // Collect all the reachable transitions from R-Graph
+    HashSet<TransitionEvent> reachableTransitions = rGraph.get(stateId);
+    for(TransitionEvent transition : reachableTransitions) {
+      Execution execution = transition.getExecution();
+      int currentChoice = transition.getChoiceCounter();
+      updateBacktrackSet(execution, currentChoice);
     }
   }
 }