Changing approach: Using vm.restoreState() method to restore JPF to the desired state...
authorrtrimana <rtrimana@uci.edu>
Thu, 9 Apr 2020 07:03:43 +0000 (00:03 -0700)
committerrtrimana <rtrimana@uci.edu>
Thu, 9 Apr 2020 07:03:43 +0000 (00:03 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index 643350a..54170ea 100644 (file)
@@ -69,14 +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 IntChoiceFromSet currBacktrackCG;                      // Current backtrack CG
-  private HashMap<Integer, LinkedList<Integer[]>> backtrackMap;  // Track created backtracking points
-  private PriorityQueue<Integer> backtrackStateQ;                // Heap that returns the latest state
-  private ArrayList<BacktrackPoint> backtrackPointList;          // Record backtrack points (CG and choice)
-  private HashMap<Integer, IntChoiceFromSet> cgMap;              // Maps state IDs to CGs
-  private HashMap<Integer, HashSet<Integer>> conflictPairMap;    // Record conflicting events
-  private HashSet<String> doneBacktrackSet;                      // Record state ID and trace that are done
-  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<BacktrackPoint> backtrackPointList;           // Record backtrack points (CG, state Id, and choice)
+  private HashMap<Integer, HashSet<Integer>> conflictPairMap;     // Record conflicting events
+  private HashSet<String> doneBacktrackSet;                       // Record state ID and trace that are done
+  private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;      // Record fields that are accessed
+  private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
 
   // Visible operation dependency graph implementation (SPIN paper) related fields
   private int prevChoiceValue;
@@ -95,6 +94,7 @@ public class DPORStateReducer extends ListenerAdapter {
       out = null;
     }
     isBooleanCGFlipped = false;
+    restorableStateMap = new HashMap<>();
     initializeStatesVariables();
   }
 
@@ -186,9 +186,6 @@ public class DPORStateReducer extends ListenerAdapter {
           // 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
-          BacktrackPoint backtrackPoint = new BacktrackPoint(icsCG, choices[choiceIndex]);
-          backtrackPointList.add(backtrackPoint);
         } else {
           // Set done all CGs while transitioning to a new execution
           icsCG.setDone();
@@ -213,21 +210,17 @@ public class DPORStateReducer extends ListenerAdapter {
       // Check every choice generated and ensure fair scheduling!
       if (currentCG instanceof IntChoiceFromSet) {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
-        // Check if the current CG is the CG just being reset
-        if (!checkCurrentCGIsValid(icsCG, vm)) {
-          return;
-        }
         // If this is a new CG then we need to update data structures
-        resetStatesForNewExecution(icsCG);
+        resetStatesForNewExecution(icsCG, vm);
         // If we don't see a fair scheduling of events/choices then we have to enforce it
-        checkAndEnforceFairScheduling(icsCG);
+        fairSchedulingAndBacktrackPoint(icsCG, vm);
         // Map state to event
         mapStateToEvent(icsCG.getNextChoice());
         // Update the VOD graph always with the latest
         updateVODGraph(icsCG.getNextChoice());
         // Check if we have seen this state or this state contains cycles that involve all events
         if (terminateCurrentExecution()) {
-          exploreNextBacktrackPoints(icsCG, vm);
+          exploreNextBacktrackPoints(vm, icsCG);
         }
         justVisitedStates.clear();
         choiceCounter++;
@@ -235,19 +228,6 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  private RestorableVMState restorableVMState = null;
-
-  private void restoreState(IntChoiceFromSet icsCG, VM vm) {
-
-    if (icsCG.getStateId() == 10) {
-      restorableVMState = vm.getRestorableState();
-    }
-    if (restorableVMState != null && icsCG.getStateId() < 10) {
-      //vm.restoreState(restorableVMState);
-      System.out.println();
-    }
-  }
-
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
@@ -340,18 +320,22 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices
+  // This class compactly stores backtrack points: 1) backtrack state ID, and 2) backtracking choices
   private class BacktrackPoint {
-    private IntChoiceFromSet backtrackCG; // CG to backtrack from
+    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 cho) {
+    public BacktrackPoint(IntChoiceFromSet cg, int stId, int cho) {
       backtrackCG = cg;
+      stateId = stId;
       choice = cho;
     }
 
-    public IntChoiceFromSet getBacktrackCG() {
-      return backtrackCG;
+    public IntChoiceFromSet getBacktrackCG() { return backtrackCG; }
+
+    public int getStateId() {
+      return stateId;
     }
 
     public int getChoice() {
@@ -380,7 +364,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private final static String JAVA_STRING_LIB = "java.lang.String";
 
   // -- FUNCTIONS
-  private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) {
+  private void fairSchedulingAndBacktrackPoint(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();
@@ -391,6 +375,8 @@ public class DPORStateReducer extends ListenerAdapter {
         icsCG.setChoice(currCGIndex, expectedChoice);
       }
     }
+    // Record state ID and choice/event as backtrack point
+    backtrackPointList.add(new BacktrackPoint(icsCG, vm.getStateId(), refChoices[choiceIndex]));
   }
 
   private Integer[] copyChoices(Integer[] choicesToCopy) {
@@ -437,11 +423,9 @@ public class DPORStateReducer extends ListenerAdapter {
     prevVisitedStates = new HashSet<>();
     stateToEventMap = new HashMap<>();
     // Backtracking
-    currBacktrackCG = null;
     backtrackMap = new HashMap<>();
     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
     backtrackPointList = new ArrayList<>();
-    cgMap = new HashMap<>();
     conflictPairMap = new HashMap<>();
     doneBacktrackSet = new HashSet<>();
     readWriteFieldsMap = new HashMap<>();
@@ -484,12 +468,14 @@ public class DPORStateReducer extends ListenerAdapter {
       stateToEventMap.put(stateId, eventSet);
     }
     justVisitedStates.add(stateId);
+    // Store restorable state object for this state (always store the latest)
+    RestorableVMState restorableState = search.getVM().getRestorableState();
+    restorableStateMap.put(stateId, restorableState);
   }
 
   // --- Functions related to Read/Write access analysis on shared fields
 
-  private void addNewBacktrackPoint(IntChoiceFromSet backtrackCG, Integer[] newChoiceList) {
-    int stateId = backtrackCG.getStateId();
+  private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList) {
     // Insert backtrack point to the right state ID
     LinkedList<Integer[]> backtrackList;
     if (backtrackMap.containsKey(stateId)) {
@@ -499,10 +485,6 @@ public class DPORStateReducer extends ListenerAdapter {
       backtrackMap.put(stateId, backtrackList);
     }
     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);
@@ -573,36 +555,22 @@ public class DPORStateReducer extends ListenerAdapter {
     // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator
     // for certain method calls in the infrastructure, e.g., eventSince()
     int currChoiceInd = currentChoice % refChoices.length;
-    int currChoiceFromCG = getCurrentChoice(vm);
+    int currChoiceFromCG = 0;
+    ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
+    // This is the main event CG
+    if (currentCG instanceof IntChoiceFromSet) {
+      currChoiceFromCG = currChoiceInd;
+    } else {
+      // This is the interval CG used in device handlers
+      ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
+      currChoiceFromCG = ((IntChoiceFromSet) parentCG).getNextChoiceIndex();
+    }
     if (currChoiceInd != currChoiceFromCG) {
       currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG;
     }
     return currentChoice;
   }
 
-  private boolean checkCurrentCGIsValid(IntChoiceFromSet icsCG, VM vm) {
-    // Check if the execution explored is from the last CG being reset
-    if (isEndOfExecution) {
-      if (currBacktrackCG != null && currBacktrackCG != icsCG) {
-        // If the reset CG isn't explored, try to explore another one
-        exploreNextBacktrackPoints(icsCG, vm);
-        return false;
-      } else {
-        int stateId = currBacktrackCG.getStateId();
-        LinkedList<Integer[]> backtrackChoices = backtrackMap.get(stateId);
-        backtrackChoices.removeLast();
-        // 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 true;
-      }
-    }
-    return true;
-  }
-
   private void createBacktrackingPoint(int currentChoice, int confEvtNum) {
 
     // Create a new list of choices for backtrack based on the current choice and conflicting event number
@@ -622,13 +590,13 @@ public class DPORStateReducer extends ListenerAdapter {
       }
     }
     // Get the backtrack CG for this backtrack point
-    IntChoiceFromSet backtrackCG = backtrackPointList.get(confEvtNum).getBacktrackCG();
+    int stateId = backtrackPointList.get(confEvtNum).getStateId();
     // Check if this trace has been done starting from this state
-    if (isTraceConstructed(newChoiceList, backtrackCG)) {
+    if (isTraceConstructed(newChoiceList, stateId)) {
       return;
     }
     //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
-    addNewBacktrackPoint(backtrackCG, newChoiceList);
+    addNewBacktrackPoint(stateId, newChoiceList);
   }
 
   private boolean excludeThisForItContains(String[] excludedStrings, String className) {
@@ -658,27 +626,31 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
-  private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG, VM vm) {
+  private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
 
     // We can start exploring the next backtrack point after the current CG is advanced at least once
     if (choiceCounter > 0) {
-      HashSet<IntChoiceFromSet> backtrackCGs = new HashSet<>(cgMap.values());
       // Check if we are reaching the end of our execution: no more backtracking points to explore
       // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
       if (!backtrackStateQ.isEmpty()) {
-        // Reset the next CG with the latest state
-        int hiStateId = getHighestStateId(icsCG, vm);
-        IntChoiceFromSet backtrackCG = setBacktrackCG(hiStateId, backtrackCGs);
-        currBacktrackCG = backtrackCG;
-      }
-      // Clear unused CGs
-      for (BacktrackPoint backtrackPoint : backtrackPointList) {
-        IntChoiceFromSet cg = backtrackPoint.getBacktrackCG();
-        if (!backtrackCGs.contains(cg)) {
-          cg.setDone();
+        // Set done all the other backtrack points
+        for (BacktrackPoint backtrackPoint : backtrackPointList) {
+          backtrackPoint.getBacktrackCG().setDone();
         }
+        // Reset the next backtrack point with the latest state
+        int hiStateId = backtrackStateQ.peek();
+        // Restore the state first if necessary
+        if (vm.getStateId() != hiStateId) {
+          RestorableVMState restorableState = restorableStateMap.get(hiStateId);
+          vm.restoreState(restorableState);
+        }
+        // Set the backtrack CG
+        IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
+        setBacktrackCG(hiStateId, backtrackCG);
+      } else {
+        // Set done this last CG (we save a few rounds)
+        icsCG.setDone();
       }
-      backtrackPointList.clear();
       // Save all the visited states when starting a new execution of trace
       prevVisitedStates.addAll(currVisitedStates);
       currVisitedStates.clear();
@@ -687,36 +659,6 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  private int getCurrentChoice(VM vm) {
-    ChoiceGenerator<?> currentCG = vm.getChoiceGenerator();
-    // This is the main event CG
-    if (currentCG instanceof IntChoiceFromSet) {
-      return ((IntChoiceFromSet) currentCG).getNextChoiceIndex();
-    } else {
-      // This is the interval CG used in device handlers
-      ChoiceGenerator<?> parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator();
-      return ((IntChoiceFromSet) parentCG).getNextChoiceIndex();
-    }
-  }
-
-  private int getHighestStateId(IntChoiceFromSet icsCG, VM vm) {
-    // Try to look for the highest state from the queue
-    int hiStateId = backtrackStateQ.peek();
-    // Check with the current state and if it's lower than the highest state, we defer to this lower state
-    int currStateId = icsCG.getStateId();
-    if (currStateId < hiStateId) {
-      // Find the next CG with the next highest state
-      while (!cgMap.keySet().contains(currStateId) && currStateId > 0) { // Stop at state 0
-        currStateId--;
-      }
-      if (currStateId > 0) { // If we reach this, it means that there are only CGs with higher states left
-        hiStateId = currStateId;
-      }
-    }
-
-    return hiStateId;
-  }
-
   private ReadWriteSet getReadWriteSet(int currentChoice) {
     // Do the analysis to get Read and Write accesses to fields
     ReadWriteSet rwSet;
@@ -779,9 +721,8 @@ public class DPORStateReducer extends ListenerAdapter {
     return true;
   }
 
-  private boolean isTraceConstructed(Integer[] choiceList, IntChoiceFromSet backtrackCG) {
+  private boolean isTraceConstructed(Integer[] choiceList, int stateId) {
     // Concatenate state ID and trace in a string, e.g., "1:10234"
-    int stateId = backtrackCG.getStateId();
     StringBuilder sb = new StringBuilder();
     sb.append(stateId);
     sb.append(':');
@@ -796,7 +737,7 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
-  private void resetStatesForNewExecution(IntChoiceFromSet icsCG) {
+  private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) {
     if (choices == null || choices != icsCG.getAllChoices()) {
       // Reset state variables
       choiceCounter = 0;
@@ -807,25 +748,21 @@ public class DPORStateReducer extends ListenerAdapter {
       readWriteFieldsMap.clear();
       stateToEventMap.clear();
       isEndOfExecution = false;
-      // Adding this CG as the first backtrack point for this execution
-      backtrackPointList.add(new BacktrackPoint(icsCG, choices[0]));
+      backtrackPointList.clear();
     }
   }
 
-  private IntChoiceFromSet setBacktrackCG(int stateId, HashSet<IntChoiceFromSet> backtrackCGs) {
+  private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) {
     // Set a backtrack CG based on a state ID
-    IntChoiceFromSet backtrackCG = cgMap.get(stateId);
-    // Need to reset the CGs first so that the CG last reset will be chosen next
-    for (IntChoiceFromSet cg : backtrackCGs) {
-      if (cg != backtrackCG && cg.getNextChoiceIndex() > -1) {
-        cg.reset();
-      }
-    }
     LinkedList<Integer[]> backtrackChoices = backtrackMap.get(stateId);
-    backtrackCG.setNewValues(backtrackChoices.peekLast());  // Get the last from the queue
+    backtrackCG.setNewValues(backtrackChoices.removeLast());  // Get the last from the queue
+    backtrackCG.setStateId(stateId);
     backtrackCG.reset();
-
-    return backtrackCG;
+    // Remove from the queue if we don't have more backtrack points for that state
+    if (backtrackChoices.isEmpty()) {
+      backtrackMap.remove(stateId);
+      backtrackStateQ.remove(stateId);
+    }
   }
 
   // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper
@@ -835,8 +772,9 @@ public class DPORStateReducer extends ListenerAdapter {
   private boolean isReachableInVODGraph(int currentChoice) {
     // Extract previous and current events
     int choiceIndex = currentChoice % refChoices.length;
+    int prevChoIndex = (currentChoice - 1) % refChoices.length;
     int currEvent = refChoices[choiceIndex];
-    int prevEvent = refChoices[choiceIndex - 1];
+    int prevEvent = refChoices[prevChoIndex];
     // Record visited choices as we search in the graph
     HashSet<Integer> visitedChoice = new HashSet<>();
     visitedChoice.add(prevEvent);