Fixing a bug: misunderstood how the VOD graph is supposed to be generated; we basical...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 632edea45df8511f5b6881a9e364e44a7c589a6a..f034f0998da06b9cfb9bd4d34583f9d9874cafa9 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -74,10 +74,12 @@ public class DPORStateReducer extends ListenerAdapter {
   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 already constructed
+  private HashMap<Integer,Integer> newStateEventMap;              // Record event producing a new state ID
   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 currChoiceValue;
   private int prevChoiceValue;
   private HashMap<Integer, HashSet<Integer>> vodGraphMap; // Visible operation dependency graph (VOD graph)
 
@@ -216,8 +218,6 @@ public class DPORStateReducer extends ListenerAdapter {
         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(vm, icsCG);
@@ -265,7 +265,7 @@ public class DPORStateReducer extends ListenerAdapter {
                   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)) {
+                    if (vm.isNewState() || isReachableInVODGraph(currentChoice, vm)) {
                       createBacktrackingPoint(currentChoice, eventCounter);
                     }
                   }
@@ -375,6 +375,8 @@ public class DPORStateReducer extends ListenerAdapter {
         icsCG.setChoice(currCGIndex, expectedChoice);
       }
     }
+    // Update current choice
+    currChoiceValue = refChoices[choiceIndex];
     // Record state ID and choice/event as backtrack point
     int stateId = vm.getStateId();
     backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));
@@ -432,8 +434,10 @@ public class DPORStateReducer extends ListenerAdapter {
     backtrackPointList = new ArrayList<>();
     conflictPairMap = new HashMap<>();
     doneBacktrackSet = new HashSet<>();
+    newStateEventMap = new HashMap<>();
     readWriteFieldsMap = new HashMap<>();
     // VOD graph
+    currChoiceValue = 0;
     prevChoiceValue = -1;
     vodGraphMap = new HashMap<>();
     // Booleans
@@ -472,6 +476,8 @@ public class DPORStateReducer extends ListenerAdapter {
       stateToEventMap.put(stateId, eventSet);
     }
     justVisitedStates.add(stateId);
+    // Update the VOD graph when there is a new state
+    updateVODGraph(search.getVM());
   }
 
   // --- Functions related to Read/Write access analysis on shared fields
@@ -774,23 +780,26 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // --- 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)
-  //private boolean isReachableInVODGraph(int checkedChoice, int referenceChoice) {
-  private boolean isReachableInVODGraph(int currentChoice) {
-    // Extract previous and current events
+  // This method checks whether a choice/event (transition) is reachable from the choice/event that produces
+  // the state right before this state in the VOD graph
+  // We use a BFS algorithm for this purpose
+  private boolean isReachableInVODGraph(int currentChoice, VM vm) {
+    // Current event
     int choiceIndex = currentChoice % refChoices.length;
-    int prevChoIndex = (currentChoice - 1) % refChoices.length;
     int currEvent = refChoices[choiceIndex];
-    int prevEvent = refChoices[prevChoIndex];
-    // Record visited choices as we search in the graph
-    HashSet<Integer> visitedChoice = new HashSet<>();
-    visitedChoice.add(prevEvent);
-    LinkedList<Integer> nodesToVisit = new LinkedList<>();
-    // If the state doesn't advance as the threads/sub-programs are executed (basically there is no new state),
-    // there is a chance that the graph doesn't have new nodes---thus this check will return a null.
+    // Previous event
+    int stateId = vm.getStateId();  // A state that has been seen
+    int prevEvent = newStateEventMap.get(stateId);
+    // Only start traversing the graph if prevEvent has an outgoing edge
     if (vodGraphMap.containsKey(prevEvent)) {
+      // Record visited choices as we search in the graph
+      HashSet<Integer> visitedChoice = new HashSet<>();
+      visitedChoice.add(prevEvent);
+      // Get the first nodes to visit (the neighbors of prevEvent)
+      LinkedList<Integer> nodesToVisit = new LinkedList<>();
       nodesToVisit.addAll(vodGraphMap.get(prevEvent));
-      while(!nodesToVisit.isEmpty()) {
+      // Traverse the graph using BFS
+      while (!nodesToVisit.isEmpty()) {
         int choice = nodesToVisit.removeFirst();
         if (choice == currEvent) {
           return true;
@@ -816,18 +825,23 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
-  private void updateVODGraph(int currChoiceValue) {
-    // Update the graph when we have the current choice value
-    HashSet<Integer> choiceSet;
-    if (vodGraphMap.containsKey(prevChoiceValue)) {
-      // If the key already exists, just retrieve it
-      choiceSet = vodGraphMap.get(prevChoiceValue);
-    } else {
-      // Create a new entry
-      choiceSet = new HashSet<>();
-      vodGraphMap.put(prevChoiceValue, choiceSet);
+  private void updateVODGraph(VM vm) {
+    // Do this only if it is a new state
+    if (vm.isNewState()) {
+      // Update the graph when we have the current choice value
+      HashSet<Integer> choiceSet;
+      if (vodGraphMap.containsKey(prevChoiceValue)) {
+        // If the key already exists, just retrieve it
+        choiceSet = vodGraphMap.get(prevChoiceValue);
+      } else {
+        // Create a new entry
+        choiceSet = new HashSet<>();
+        vodGraphMap.put(prevChoiceValue, choiceSet);
+      }
+      choiceSet.add(currChoiceValue);
+      prevChoiceValue = currChoiceValue;
+      // Map this state ID to the event (transition) that produces it
+      newStateEventMap.put(vm.getStateId(), currChoiceValue);
     }
-    choiceSet.add(currChoiceValue);
-    prevChoiceValue = currChoiceValue;
   }
 }