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

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 72fc44e6c67f8ec4a48cfa8dd141a2ab043c33c3..fe879895529b018884d09ca9450e040ea615fe3f 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -60,9 +60,8 @@ public class DPORStateReducer extends ListenerAdapter {
   // DPOR-related fields
   // Basic information
   private Integer[] choices;
   // DPOR-related fields
   // Basic information
   private Integer[] choices;

-  private Integer[] refChoices;
+  private Integer[] refChoices; // Second reference to a copy of choices (choices may be modified for fair scheduling)

   private int choiceCounter;
   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


@@ -72,7 +71,7 @@ public class DPORStateReducer extends ListenerAdapter {
   // 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
   // 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<IntChoiceFromSet> cgList;                         // Record CGs for backtracking points
+  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, 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


@@ -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) {


@@ -188,7 +186,8 @@ public class DPORStateReducer extends ListenerAdapter {
           int choiceIndex = choiceCounter % choices.length;
           icsCG.advance(choices[choiceIndex]);
           // Index the ChoiceGenerator to set backtracking points
           int choiceIndex = choiceCounter % choices.length;
           icsCG.advance(choices[choiceIndex]);
           // Index the ChoiceGenerator to set backtracking points

-          cgList.add(icsCG);
+          BacktrackPoint backtrackPoint = new BacktrackPoint(icsCG, choices[choiceIndex]);
+          backtrackPointList.add(backtrackPoint);

         } else {
           // Set done all CGs while transitioning to a new execution
           icsCG.setDone();
         } else {
           // Set done all CGs while transitioning to a new execution
           icsCG.setDone();


@@ -223,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++;


@@ -326,19 +325,19 @@ public class DPORStateReducer extends ListenerAdapter {
   // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices
   private class BacktrackPoint {
     private IntChoiceFromSet backtrackCG; // CG to backtrack from
   // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices
   private class BacktrackPoint {
     private IntChoiceFromSet backtrackCG; // CG to backtrack from

-    private Integer[] backtrackChoices;   // Choices to set for this backtrack CG
+    private int choice;                   // Choice chosen at this backtrack point

 
 

-    public BacktrackPoint(IntChoiceFromSet cg, Integer[] choices) {
+    public BacktrackPoint(IntChoiceFromSet cg, int cho) {

       backtrackCG = cg;
       backtrackCG = cg;

-      backtrackChoices = choices;
+      choice = cho;

     }
 
     public IntChoiceFromSet getBacktrackCG() {
       return backtrackCG;
     }
 
     }
 
     public IntChoiceFromSet getBacktrackCG() {
       return backtrackCG;
     }
 

-    public Integer[] getBacktrackChoices() {
-      return backtrackChoices;
+    public int getChoice() {
+      return choice;

     }
   }
 
     }
   }
 


@@ -413,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<>();


@@ -423,7 +421,7 @@ public class DPORStateReducer extends ListenerAdapter {
     // Backtracking
     backtrackMap = new HashMap<>();
     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
     // Backtracking
     backtrackMap = new HashMap<>();
     backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());

-    cgList = new ArrayList<>();
+    backtrackPointList = new ArrayList<>();

     cgMap = new HashMap<>();
     conflictPairMap = new HashMap<>();
     doneBacktrackSet = new HashSet<>();
     cgMap = new HashMap<>();
     conflictPairMap = new HashMap<>();
     doneBacktrackSet = new HashSet<>();


@@ -433,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) {


@@ -572,10 +569,9 @@ public class DPORStateReducer extends ListenerAdapter {
     Integer[] newChoiceList = new Integer[refChoices.length];
     // Put the conflicting event numbers first and reverse the order
     int actualCurrCho = currentChoice % refChoices.length;
     Integer[] newChoiceList = new Integer[refChoices.length];
     // Put the conflicting event numbers first and reverse the order
     int actualCurrCho = currentChoice % refChoices.length;

-    int actualConfEvtNum = confEvtNum % refChoices.length;
-    // We use the actual choices here in case they have been modified/adjusted
+    // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method

     newChoiceList[0] = choices[actualCurrCho];
     newChoiceList[0] = choices[actualCurrCho];

-    newChoiceList[1] = choices[actualConfEvtNum];
+    newChoiceList[1] = backtrackPointList.get(confEvtNum).getChoice();

     // 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]) {
     // 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]) {


@@ -583,8 +579,8 @@ public class DPORStateReducer extends ListenerAdapter {
         j++;
       }
     }
         j++;
       }
     }

-    // Record the backtracking point in the stack as well
-    IntChoiceFromSet backtrackCG = cgList.get(confEvtNum);
+    // Get the backtrack CG for this backtrack point
+    IntChoiceFromSet backtrackCG = backtrackPointList.get(confEvtNum).getBacktrackCG();

     // Check if this trace has been done starting from this state
     if (isTraceConstructed(newChoiceList, backtrackCG)) {
       return;
     // Check if this trace has been done starting from this state
     if (isTraceConstructed(newChoiceList, backtrackCG)) {
       return;


@@ -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,20 +745,25 @@ 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();
       stateToEventMap.clear();
       isEndOfExecution = false;
       // Clearing data structures
       conflictPairMap.clear();
       readWriteFieldsMap.clear();
       stateToEventMap.clear();
       isEndOfExecution = false;

-                       // Adding this CG as the first CG for this execution
-                       cgList.add(icsCG);
+      // Adding this CG as the first backtrack point for this execution
+      backtrackPointList.add(new BacktrackPoint(icsCG, choices[0]));

     }
   }
 
     }
   }
 

-  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,37 +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(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)
   // --- 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)