Committing a version that almost works: bug to fix is that when an execution finishes...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index fe879895529b018884d09ca9450e040ea615fe3f..643350aaf6ca834f5ea78fb39bd530787ac007cb 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -69,13 +69,14 @@ 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 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 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
 
   // Visible operation dependency graph implementation (SPIN paper) related fields
   private int prevChoiceValue;
@@ -212,6 +213,10 @@ 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);
         // If we don't see a fair scheduling of events/choices then we have to enforce it
@@ -222,7 +227,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()) {
-          exploreNextBacktrackPoints(icsCG);
+          exploreNextBacktrackPoints(icsCG, vm);
         }
         justVisitedStates.clear();
         choiceCounter++;
@@ -230,6 +235,19 @@ 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) {
@@ -419,6 +437,7 @@ 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<>();
@@ -561,6 +580,29 @@ public class DPORStateReducer extends ListenerAdapter {
     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
@@ -616,21 +658,18 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
-  private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG) {
+  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 (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 = 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 && cgMap.keySet().contains(currStateId)) {
-          hiStateId = currStateId;
-        }
-        setBacktrackCG(hiStateId, backtrackCGs);
+        int hiStateId = getHighestStateId(icsCG, vm);
+        IntChoiceFromSet backtrackCG = setBacktrackCG(hiStateId, backtrackCGs);
+        currBacktrackCG = backtrackCG;
       }
       // Clear unused CGs
       for (BacktrackPoint backtrackPoint : backtrackPointList) {
@@ -660,6 +699,24 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
+  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;
@@ -755,7 +812,7 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  private void setBacktrackCG(int stateId, HashSet<IntChoiceFromSet> backtrackCGs) {
+  private IntChoiceFromSet setBacktrackCG(int stateId, HashSet<IntChoiceFromSet> backtrackCGs) {
     // 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
@@ -765,14 +822,10 @@ public class DPORStateReducer extends ListenerAdapter {
       }
     }
     LinkedList<Integer[]> backtrackChoices = backtrackMap.get(stateId);
-    backtrackCG.setNewValues(backtrackChoices.removeLast());  // Get the last from the queue
+    backtrackCG.setNewValues(backtrackChoices.peekLast());  // 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;
   }
 
   // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper