Reimplementing DPOR Phase 3: Architecting the subsequent executions (backtrack points...
authorrtrimana <rtrimana@uci.edu>
Fri, 3 Apr 2020 23:13:34 +0000 (16:13 -0700)
committerrtrimana <rtrimana@uci.edu>
Fri, 3 Apr 2020 23:13:34 +0000 (16:13 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index 8c6a1d6..feb51c7 100644 (file)
@@ -69,12 +69,13 @@ public class DPORStateReducer extends ListenerAdapter {
   private HashSet<Integer> prevVisitedStates; // States visited in the previous execution
   private HashMap<Integer, HashSet<Integer>> stateToEventMap;
   // Data structure to analyze field Read/Write accesses and conflicts
-  private HashMap<Integer, LinkedList<Integer[]>> backtrackMap; // Track created backtracking points
-  private Stack<BacktrackPoint> btrckPtsStack;                  // Stack that stores backtracking points
-  private List<IntChoiceFromSet> cgList;                        // Record CGs for backtracking points
-  private HashSet<IntChoiceFromSet> btrckCGSet;                 // Set that records all the backtrack CGs
-  private HashMap<Integer, HashSet<Integer>> conflictPairMap;   // Record conflicting events
-  private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;    // Record fields that are accessed
+  private HashMap<Integer, LinkedList<Integer[]>> backtrackMap;       // Track created backtracking points
+  private PriorityQueue<Integer> backtrackStateQ;                     // Heap that returns the latest state
+  private ArrayList<IntChoiceFromSet> cgList;                         // Record CGs for backtracking points
+  private HashMap<Integer, IntChoiceFromSet> cgMap;                   // Maps state IDs to CGs
+  private HashMap<Integer, HashSet<Integer>> conflictPairMap;         // Record conflicting events
+//  private HashSet<IntChoiceFromSet> activeBacktrackCGs;               // Record active backtrack CGs
+  private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;          // Record fields that are accessed
 
   // Visible operation dependency graph implementation (SPIN paper) related fields
   private int prevChoiceValue;
@@ -82,6 +83,8 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // Boolean states
   private boolean isBooleanCGFlipped;
+  private boolean isFirstResetDone;
+  private boolean isEndOfExecution;
 
   public DPORStateReducer(Config config, JPF jpf) {
     verboseMode = config.getBoolean("printout_state_transition", false);
@@ -103,16 +106,19 @@ public class DPORStateReducer extends ListenerAdapter {
     stateToEventMap = new HashMap<>();
     // Backtracking
     backtrackMap = new HashMap<>();
-    btrckPtsStack = new Stack<>();
-    btrckCGSet = new HashSet<>();
+    backtrackStateQ = new PriorityQueue<>();
     cgList = new ArrayList<>();
+    cgMap = new HashMap<>();
     conflictPairMap = new HashMap<>();
+//    activeBacktrackCGs = new HashSet<>();
     readWriteFieldsMap = new HashMap<>();
     // VOD graph
     prevChoiceValue = -1;
     vodGraphMap = new HashMap<>();
     // Booleans
     isBooleanCGFlipped = false;
+    isEndOfExecution = false;
+    isFirstResetDone = false;
   }
 
   @Override
@@ -187,23 +193,28 @@ public class DPORStateReducer extends ListenerAdapter {
       // Initialize with necessary information from the CG
       if (nextCG instanceof IntChoiceFromSet) {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
-        // Check if CG has been initialized, otherwise initialize it
-        Integer[] cgChoices = icsCG.getAllChoices();
-        // Record the events (from choices)
-        if (choices == null) {
-          choices = cgChoices;
-          // Make a copy of choices as reference
-          refChoices = copyChoices(choices);
-          // Record the max event choice (the last element of the choice array)
-          maxEventChoice = choices[choices.length - 1];
+        if (!isEndOfExecution) {
+          // Check if CG has been initialized, otherwise initialize it
+          Integer[] cgChoices = icsCG.getAllChoices();
+          // Record the events (from choices)
+          if (choices == null) {
+            choices = cgChoices;
+            // Make a copy of choices as reference
+            refChoices = copyChoices(choices);
+            // Record the max event choice (the last element of the choice array)
+            maxEventChoice = choices[choices.length - 1];
+          }
+          icsCG.setNewValues(choices);
+          icsCG.reset();
+          // Use a modulo since choiceCounter is going to keep increasing
+          int choiceIndex = choiceCounter % choices.length;
+          icsCG.advance(choices[choiceIndex]);
+          // Index the ChoiceGenerator to set backtracking points
+          cgList.add(icsCG);
+        } else {
+          // Set done all CGs while transitioning to a new execution
+          icsCG.setDone();
         }
-        icsCG.setNewValues(choices);
-        icsCG.reset();
-        // Use a modulo since choiceCounter is going to keep increasing
-        int choiceIndex = choiceCounter % choices.length;
-        icsCG.advance(choices[choiceIndex]);
-        // Index the ChoiceGenerator to set backtracking points
-        cgList.add(icsCG);
       }
     }
   }
@@ -223,6 +234,8 @@ public class DPORStateReducer extends ListenerAdapter {
       // Check every choice generated and ensure fair scheduling!
       if (currentCG instanceof IntChoiceFromSet) {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
+        // If this is a new CG then we need to update data structures
+        resetStatesForNewExecution(icsCG);
         // If we don't see a fair scheduling of events/choices then we have to enforce it
         checkAndEnforceFairScheduling(icsCG);
         // Map state to event
@@ -231,7 +244,7 @@ public class DPORStateReducer extends ListenerAdapter {
         updateVODGraph(icsCG.getNextChoice());
         // Check if we have seen this state or this state contains cycles that involve all events
         if (terminateCurrentExecution()) {
-          exploreNextBacktrackSets(icsCG);
+          exploreNextBacktrackPoints(icsCG, vm);
         }
         justVisitedStates.clear();
         choiceCounter++;
@@ -242,40 +255,43 @@ public class DPORStateReducer extends ListenerAdapter {
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
-      // Has to be initialized and a integer CG
-      ChoiceGenerator<?> cg = vm.getChoiceGenerator();
-      if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
-        int currentChoice = choiceCounter - 1;  // Accumulative choice w.r.t the current trace
-        if (currentChoice < 0) { // If choice is -1 then skip
-          return;
-        }
-        currentChoice = checkAndAdjustChoice(currentChoice, vm);
-        // Record accesses from executed instructions
-        if (executedInsn instanceof JVMFieldInstruction) {
-          // Analyze only after being initialized
-          String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
-          // We don't care about libraries
-          if (!isFieldExcluded(fieldClass)) {
-            analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
+      if (!isEndOfExecution) {
+        // Has to be initialized and a integer CG
+        ChoiceGenerator<?> cg = vm.getChoiceGenerator();
+        if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
+          int currentChoice = choiceCounter - 1;  // Accumulative choice w.r.t the current trace
+          if (currentChoice < 0) { // If choice is -1 then skip
+            return;
           }
-        } else if (executedInsn instanceof INVOKEINTERFACE) {
-          // 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();
+          currentChoice = checkAndAdjustChoice(currentChoice, vm);
+          // Record accesses from executed instructions
+          if (executedInsn instanceof JVMFieldInstruction) {
+            // Analyze only after being initialized
+            String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName();
+            // We don't care about libraries
             if (!isFieldExcluded(fieldClass)) {
-              // Check for conflict (go backward from current choice and get the first conflict)
-              for (int eventCounter = currentChoice - 1; eventCounter >= 0; eventCounter--) {
-                // Check for conflicts with Write fields for both Read and Write instructions
-                // Check and record a backtrack set for just once!
-                if (isConflictFound(nextInsn, eventCounter, fieldClass) && isNewConflict(currentChoice, eventCounter)) {
-                  // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
-                  if (vm.isNewState() || isReachableInVODGraph(currentChoice)) {
-                    createBacktrackingPoint(currentChoice, eventCounter);
+              analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice);
+            }
+          } else if (executedInsn instanceof INVOKEINTERFACE) {
+            // 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)) {
+                // Check for conflict (go backward from current choice and get the first conflict)
+                for (int eventCounter = currentChoice - 1; eventCounter >= 0; eventCounter--) {
+                  // Check for conflicts with Write fields for both Read and Write instructions
+                  // Check and record a backtrack set for just once!
+                  if (isConflictFound(nextInsn, eventCounter, currentChoice, fieldClass) &&
+                      isNewConflict(currentChoice, eventCounter)) {
+                    // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
+                    if (vm.isNewState() || isReachableInVODGraph(currentChoice)) {
+                      createBacktrackingPoint(currentChoice, eventCounter);
+                    }
                   }
                 }
               }
@@ -449,6 +465,26 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // --- Functions related to Read/Write access analysis on shared fields
 
+  private void addNewBacktrackPoint(IntChoiceFromSet backtrackCG, Integer[] newChoiceList) {
+    int stateId = backtrackCG.getStateId();
+    // Insert backtrack point to the right state ID
+    LinkedList<Integer[]> backtrackList;
+    if (backtrackMap.containsKey(stateId)) {
+      backtrackList = backtrackMap.get(stateId);
+    } else {
+      backtrackList = new LinkedList<>();
+    }
+    backtrackList.addFirst(newChoiceList);
+    // Add CG for this state ID if there isn't one yet
+    if (!cgMap.containsKey(stateId)) {
+      cgMap.put(stateId, backtrackCG);
+    }
+    // Add to priority queue
+    if (!backtrackStateQ.contains(stateId)) {
+      backtrackStateQ.add(stateId);
+    }
+  }
+
   // Analyze Read/Write accesses that are directly invoked on fields
   private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) {
     // Do the analysis to get Read and Write accesses to fields
@@ -540,10 +576,8 @@ public class DPORStateReducer extends ListenerAdapter {
     }
     // Record the backtracking point in the stack as well
     IntChoiceFromSet backtrackCG = cgList.get(confEvtNum);
-    BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
-    btrckPtsStack.push(backtrackPoint);
-    // Also record the CG in the set
-    btrckCGSet.add(backtrackCG);
+    //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
+    addNewBacktrackPoint(backtrackCG, newChoiceList);
   }
 
   private boolean excludeThisForItContains(String[] excludedStrings, String className) {
@@ -573,31 +607,19 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
-  // TODO: THIS METHOD IS STILL UNTESTED AT THIS POINT
-  private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {
-    // We try to update the CG with a backtrack list if the state has been visited multiple times
+  private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG, VM vm) {
+    // We can start exploring the next backtrack point after the current CG is advanced at least once
     if (icsCG.getNextChoiceIndex() > 0) {
-      if (btrckPtsStack.empty()) {
-        // TODO: PROBABLY NEED TO DO CONTEXT SWITCHING HERE
+      if (backtrackMap.isEmpty()) {
+        // This means we are reaching the end of our execution: no more backtracking points to explore
         return;
       }
-      BacktrackPoint backtrackPoint = btrckPtsStack.pop();
-      Integer[] choiceList = backtrackPoint.getBacktrackChoices();
-      IntChoiceFromSet backtrackCG = backtrackPoint.getBacktrackCG();
-      // Deploy the new choice list for this CG
-      backtrackCG.setNewValues(choiceList);
-      backtrackCG.reset();
-      // Clear unused CGs
-      for(IntChoiceFromSet cg : cgList) {
-        if (!btrckCGSet.contains(cg)) {
-          cg.setDone();
-        }
-      }
-      cgList.clear();
-      btrckCGSet.clear();
+      setNextBacktrackPoint(icsCG);
       // Save all the visited states when starting a new execution of trace
       prevVisitedStates.addAll(currVisitedStates);
       currVisitedStates.clear();
+      // This marks a transitional period to the new CG
+      isEndOfExecution = true;
     }
   }
 
@@ -626,9 +648,11 @@ public class DPORStateReducer extends ListenerAdapter {
     return rwSet;
   }
 
-  private boolean isConflictFound(Instruction nextInsn, int eventCounter, String fieldClass) {
-    // Skip if this event does not have any Read/Write set
-    if (!readWriteFieldsMap.containsKey(eventCounter)) {
+  private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) {
+    int actualEvtCntr = eventCounter % refChoices.length;
+    int actualCurrCho = currentChoice % refChoices.length;
+    // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
+    if (!readWriteFieldsMap.containsKey(eventCounter) || (actualEvtCntr == actualCurrCho)) {
       return false;
     }
     ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter);
@@ -672,6 +696,71 @@ public class DPORStateReducer extends ListenerAdapter {
     return true;
   }
 
+  private void resetStatesForNewExecution(IntChoiceFromSet icsCG) {
+    if (choices == null || choices != icsCG.getAllChoices()) {
+      // Reset state variables
+      choiceCounter = 0;
+      choices = icsCG.getAllChoices();
+      refChoices = copyChoices(choices);
+      // Clearing data structures
+      backtrackMap.clear();
+      conflictPairMap.clear();
+      readWriteFieldsMap.clear();
+      stateToEventMap.clear();
+      isEndOfExecution = false;
+    }
+  }
+
+  private IntChoiceFromSet setBacktrackCG(int stateId) {
+    // Set a backtrack CG based on a state ID
+    IntChoiceFromSet backtrackCG = cgMap.get(stateId);
+    LinkedList<Integer[]> backtrackChoices = backtrackMap.get(stateId);
+    backtrackCG.setNewValues(backtrackChoices.removeLast());  // Get the last from the queue
+    backtrackCG.reset();
+    // Remove from the queue if we don't have more backtrack points for that state
+    if (backtrackChoices.isEmpty()) {
+      cgMap.remove(stateId);
+      backtrackMap.remove(stateId);
+      backtrackStateQ.remove(stateId);
+    }
+    return backtrackCG;
+  }
+
+  private void setNextBacktrackPoint(IntChoiceFromSet icsCG) {
+
+    HashSet<IntChoiceFromSet> backtrackCGs = new HashSet<>(cgMap.values());
+    if (!isFirstResetDone) {
+      // Reset the last CG of every LinkedList in the map and set done everything else
+      for (Integer stateId : cgMap.keySet()) {
+        setBacktrackCG(stateId);
+      }
+//      activeBacktrackCGs.addAll(cgMap.values());
+      isFirstResetDone = true;
+    } else {
+      // Check if we still have backtrack points for the current CG
+      int currStateId = icsCG.getStateId();
+      if (backtrackMap.containsKey(currStateId)) {
+        setBacktrackCG(currStateId);
+      } else {
+//        activeBacktrackCGs.remove(icsCG);
+        // We try to reset new CGs (if we do have) when we are running out of active CGs
+        if (!backtrackStateQ.isEmpty()) {
+          // Reset the next CG with the latest state
+          int hiStateId = backtrackStateQ.peek();
+          IntChoiceFromSet backtrackCG = setBacktrackCG(hiStateId);
+//          activeBacktrackCGs.add(backtrackCG);
+        }
+      }
+    }
+    // Clear unused CGs
+    for(IntChoiceFromSet cg : cgList) {
+      if (!backtrackCGs.contains(cg)) {
+        cg.setDone();
+      }
+    }
+    cgList.clear();
+  }
+
   // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper
 
   // This method checks whether a choice is reachable in the VOD graph from a reference choice (BFS algorithm)