First part of boolean flip seems to be clean; need to debug the second part and figur...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 53cd5663f607d496ef980dab13f416bd8239c3fe..fe879895529b018884d09ca9450e040ea615fe3f 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -62,7 +62,6 @@ public class DPORStateReducer extends ListenerAdapter {
   private Integer[] choices;
   private Integer[] refChoices; // Second reference to a copy of choices (choices may be modified for fair scheduling)
   private int choiceCounter;
   private Integer[] choices;
   private Integer[] refChoices; // Second reference to a copy of choices (choices may be modified for fair scheduling)
   private int choiceCounter;

-  private int lastCGStateId;    // Record the state of the currently active CG

   private int maxEventChoice;
   // Data structure to track the events seen by each state to track cycles (containing all events) for termination
   private HashSet<Integer> currVisitedStates; // States being visited in the current execution
   private int maxEventChoice;
   // Data structure to track the events seen by each state to track cycles (containing all events) for termination
   private HashSet<Integer> currVisitedStates; // States being visited in the current execution


@@ -84,7 +83,6 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // Boolean states
   private boolean isBooleanCGFlipped;
 
   // Boolean states
   private boolean isBooleanCGFlipped;

-  private boolean isFirstResetDone;

   private boolean isEndOfExecution;
 
   public DPORStateReducer(Config config, JPF jpf) {
   private boolean isEndOfExecution;
 
   public DPORStateReducer(Config config, JPF jpf) {


@@ -224,7 +222,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()) {
         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(icsCG);

         }
         justVisitedStates.clear();
         choiceCounter++;
         }
         justVisitedStates.clear();
         choiceCounter++;


@@ -414,7 +412,6 @@ public class DPORStateReducer extends ListenerAdapter {
     choices = null;
     refChoices = null;
     choiceCounter = 0;
     choices = null;
     refChoices = null;
     choiceCounter = 0;

-    lastCGStateId = 0;

     maxEventChoice = 0;
     // Cycle tracking
     currVisitedStates = new HashSet<>();
     maxEventChoice = 0;
     // Cycle tracking
     currVisitedStates = new HashSet<>();


@@ -434,7 +431,6 @@ public class DPORStateReducer extends ListenerAdapter {
     vodGraphMap = new HashMap<>();
     // Booleans
     isEndOfExecution = false;
     vodGraphMap = new HashMap<>();
     // Booleans
     isEndOfExecution = false;

-    isFirstResetDone = false;

   }
 
   private void mapStateToEvent(int nextChoiceValue) {
   }
 
   private void mapStateToEvent(int nextChoiceValue) {


@@ -620,13 +616,30 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
     return false;
   }
 

-  private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG, VM vm) {
+  private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG) {

     // We can start exploring the next backtrack point after the current CG is advanced at least once
     if (icsCG.getNextChoiceIndex() > 0) {
     // We can start exploring the next backtrack point after the current CG is advanced at least once
     if (icsCG.getNextChoiceIndex() > 0) {

+      HashSet<IntChoiceFromSet> backtrackCGs = new HashSet<>(cgMap.values());

       // Check if we are reaching the end of our execution: no more backtracking points to explore
       // Check if we are reaching the end of our execution: no more backtracking points to explore

-      if (!backtrackMap.isEmpty()) {
-        setNextBacktrackPoint(icsCG);
+      // 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);
+      }
+      // Clear unused CGs
+      for (BacktrackPoint backtrackPoint : backtrackPointList) {
+        IntChoiceFromSet cg = backtrackPoint.getBacktrackCG();
+        if (!backtrackCGs.contains(cg)) {
+          cg.setDone();
+        }

       }
       }

+      backtrackPointList.clear();

       // Save all the visited states when starting a new execution of trace
       prevVisitedStates.addAll(currVisitedStates);
       currVisitedStates.clear();
       // Save all the visited states when starting a new execution of trace
       prevVisitedStates.addAll(currVisitedStates);
       currVisitedStates.clear();


@@ -661,10 +674,11 @@ public class DPORStateReducer extends ListenerAdapter {
   }
 
   private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) {
   }
 
   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)
     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) || choices[actualCurrCho] == choices[actualEvtCntr]) {
+    if (!readWriteFieldsMap.containsKey(eventCounter) ||
+         choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) {

       return false;
     }
     ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter);
       return false;
     }
     ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter);


@@ -731,7 +745,6 @@ public class DPORStateReducer extends ListenerAdapter {
       choiceCounter = 0;
       choices = icsCG.getAllChoices();
       refChoices = copyChoices(choices);
       choiceCounter = 0;
       choices = icsCG.getAllChoices();
       refChoices = copyChoices(choices);

-      lastCGStateId = icsCG.getStateId();

       // Clearing data structures
       conflictPairMap.clear();
       readWriteFieldsMap.clear();
       // Clearing data structures
       conflictPairMap.clear();
       readWriteFieldsMap.clear();


@@ -742,9 +755,15 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

-  private void setBacktrackCG(int stateId) {
+  private void setBacktrackCG(int stateId, HashSet<IntChoiceFromSet> backtrackCGs) {

     // Set a backtrack CG based on a state ID
     IntChoiceFromSet backtrackCG = cgMap.get(stateId);
     // 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.removeLast());  // Get the last from the queue
     backtrackCG.reset();
     LinkedList<Integer[]> backtrackChoices = backtrackMap.get(stateId);
     backtrackCG.setNewValues(backtrackChoices.removeLast());  // Get the last from the queue
     backtrackCG.reset();


@@ -756,38 +775,6 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

-  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);
-      }
-      isFirstResetDone = true;
-    } else {
-      // Check if we still have backtrack points for the last state after the last backtrack
-      if (backtrackMap.containsKey(lastCGStateId)) {
-        setBacktrackCG(lastCGStateId);
-      } else {
-        // 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();
-          setBacktrackCG(hiStateId);
-        }
-      }
-    }
-    // Clear unused CGs
-    for(BacktrackPoint backtrackPoint : backtrackPointList) {
-      IntChoiceFromSet cg = backtrackPoint.getBacktrackCG();
-      if (!backtrackCGs.contains(cg)) {
-        cg.setDone();
-      }
-    }
-    backtrackPointList.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)
   // --- 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)