Refactoring; Finding cycles without traversing the entire state graph.
authorrtrimana <rtrimana@uci.edu>
Sat, 21 Mar 2020 04:34:59 +0000 (21:34 -0700)
committerrtrimana <rtrimana@uci.edu>
Sat, 21 Mar 2020 04:34:59 +0000 (21:34 -0700)
src/main/gov/nasa/jpf/listener/StateReducer.java

index 532076b..3af3205 100644 (file)
@@ -91,6 +91,8 @@ public class StateReducer extends ListenerAdapter {
 
   // Reference to the state graph in the ConflictTracker class
   private HashMap<Integer, ConflictTracker.Node> stateGraph;
+  private HashMap<Integer, HashSet<Integer>> stateToEventMap;
+  // Map state to event
   // Visited states in the previous and current executions/traces for terminating condition
   private HashSet<Integer> prevVisitedStates;
   private HashSet<Integer> currVisitedStates;
@@ -119,6 +121,7 @@ public class StateReducer extends ListenerAdapter {
     unusedCG = new HashSet<>();
     // TODO: We are assuming that the StateReducer is always used together with the ConflictTracker
     stateGraph = ConflictTracker.nodes;
+    stateToEventMap = new HashMap<>();
     prevVisitedStates = new HashSet<>();
     currVisitedStates = new HashSet<>();
     initializeStateReduction();
@@ -161,6 +164,39 @@ public class StateReducer extends ListenerAdapter {
     }
   }
 
+  private IntChoiceFromSet setNewCG(IntChoiceFromSet icsCG) {
+    icsCG.setNewValues(choices);
+    icsCG.reset();
+    // Use a modulo since choiceCounter is going to keep increasing
+    int choiceIndex = choiceCounter % (choices.length - 1);
+    icsCG.advance(choices[choiceIndex]);
+    return icsCG;
+  }
+
+  private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) {
+    if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
+      // Update the choices of the first CG and add '-1'
+      if (choices == null) {
+        // Initialize backtrack set that stores all the explored backtrack lists
+        maxUpperBound = cgChoices.length;
+        // All the choices are always the same so we only need to update it once
+        choices = new Integer[cgChoices.length + 1];
+        System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length);
+        choices[choices.length - 1] = -1;
+        String firstChoiceListString = buildStringFromChoiceList(choices);
+        backtrackSet.add(firstChoiceListString);
+      }
+      IntChoiceFromSet setCG = setNewCG(icsCG);
+      cgMap.put(setCG, choices[choiceCounter]);
+    } else {
+      // We repeat the same trace if a state match is not found yet
+      IntChoiceFromSet setCG = setNewCG(icsCG);
+      unusedCG.add(setCG);
+    }
+    //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0;
+    choiceCounter++;
+  }
+
   @Override
   public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
     if (stateReductionMode) {
@@ -176,35 +212,7 @@ public class StateReducer extends ListenerAdapter {
         }
         // Record the subsequent Integer CGs only until we hit the upper bound
         if (!isResetAfterAnalysis) {
-          if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) {
-            // Update the choices of the first CG and add '-1'
-            if (choices == null) {
-              // Initialize backtrack set that stores all the explored backtrack lists
-              maxUpperBound = cgChoices.length;
-              // All the choices are always the same so we only need to update it once
-              choices = new Integer[cgChoices.length + 1];
-              System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length);
-              choices[choices.length - 1] = -1;
-              String firstChoiceListString = buildStringFromChoiceList(choices);
-              backtrackSet.add(firstChoiceListString);
-            }
-            icsCG.setNewValues(choices);
-            icsCG.reset();
-            // Advance the current Integer CG
-            // This way we explore all the event numbers in the first pass
-            icsCG.advance(choices[choiceCounter]);
-            cgMap.put(icsCG, choices[choiceCounter]);
-          } else {
-            // We repeat the same trace if a state match is not found yet
-            icsCG.setNewValues(choices);
-            icsCG.reset();
-            // Use a modulo since choiceCounter is going to keep increasing
-            int choiceIndex = choiceCounter % (choices.length - 1);
-            icsCG.advance(choices[choiceIndex]);
-            unusedCG.add(icsCG);
-          }
-          //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0;
-          choiceCounter++;
+          initializeChoiceGenerators(icsCG, cgChoices);
         } else {
           // Set new CGs to done so that the search algorithm explores the existing CGs
           icsCG.setDone();
@@ -249,13 +257,13 @@ public class StateReducer extends ListenerAdapter {
   // We terminate the execution iff:
   // (1) the state has been visited in the current execution
   // (2) the state has one or more cycles that involve all the events
+  // With simple approach we only need to check for a re-visited state.
+  // Basically, we have to check that we have executed all events between two occurrences of such state.
   private boolean containsCyclesWithAllEvents(int stId) {
 
     HashSet<ConflictTracker.Node> visitingStates = new HashSet<>();
-    HashSet<Integer> visitedEvents = new HashSet<>();
+    HashSet<Integer> visitedEvents = stateToEventMap.get(stId);
     boolean containsCyclesWithAllEvts = false;
-    ConflictTracker.Node currNode = stateGraph.get(stId);
-    dfsFindCycles(currNode, visitingStates, visitedEvents, new HashSet<>());
     if (checkIfAllEventsInvolved(visitedEvents)) {
       containsCyclesWithAllEvts = true;
     }
@@ -263,22 +271,41 @@ public class StateReducer extends ListenerAdapter {
     return containsCyclesWithAllEvts;
   }
 
-  private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<ConflictTracker.Node> visitingStates,
-                             HashSet<Integer> visitedEvents, HashSet<Integer> visitingEvents) {
-
-    // Stop when there is a cycle and record all the events
-    if (visitingStates.contains(currNode)) {
-      visitedEvents.addAll(visitingEvents);
-    } else {
-      visitingStates.add(currNode);
-      for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
-        visitingEvents.add(edge.getEventNumber());
-        dfsFindCycles(edge.getDst(), visitingStates, visitedEvents, visitingEvents);
-        visitingEvents.remove(edge.getEventNumber());
-      }
-      visitingStates.remove(currNode);
-    }
-  }
+  // TODO: The following is a full-blown graph traversal that we can do if we need to in the future
+  // Detect cycles in the current execution/trace
+  // We terminate the execution iff:
+  // (1) the state has been visited in the current execution
+  // (2) the state has one or more cycles that involve all the events
+//  private boolean containsCyclesWithAllEvents(int stId) {
+//
+//    HashSet<ConflictTracker.Node> visitingStates = new HashSet<>();
+//    HashSet<Integer> visitedEvents = new HashSet<>();
+//    boolean containsCyclesWithAllEvts = false;
+//    ConflictTracker.Node currNode = stateGraph.get(stId);
+//    dfsFindCycles(currNode, visitingStates, visitedEvents, new HashSet<>());
+//    if (checkIfAllEventsInvolved(visitedEvents)) {
+//      containsCyclesWithAllEvts = true;
+//    }
+//
+//    return containsCyclesWithAllEvts;
+//  }
+//
+//  private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<ConflictTracker.Node> visitingStates,
+//                             HashSet<Integer> visitedEvents, HashSet<Integer> visitingEvents) {
+//
+//    // Stop when there is a cycle and record all the events
+//    if (visitingStates.contains(currNode)) {
+//      visitedEvents.addAll(visitingEvents);
+//    } else {
+//      visitingStates.add(currNode);
+//      for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
+//        visitingEvents.add(edge.getEventNumber());
+//        dfsFindCycles(edge.getDst(), visitingStates, visitedEvents, visitingEvents);
+//        visitingEvents.remove(edge.getEventNumber());
+//      }
+//      visitingStates.remove(currNode);
+//    }
+//  }
 
   private boolean checkIfAllEventsInvolved(HashSet<Integer> visitedEvents) {
 
@@ -299,6 +326,46 @@ public class StateReducer extends ListenerAdapter {
     currVisitedStates.clear();
   }
 
+  private void updateChoices(IntChoiceFromSet icsCG) {
+    if (choices == null || choices != icsCG.getAllChoices()) {
+      currCG = icsCG;
+      choices = icsCG.getAllChoices();
+      // Reset a few things for the sub-graph
+      conflictPairMap.clear();
+      readWriteFieldsMap.clear();
+      choiceCounter = 0;
+    }
+  }
+
+  private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {
+    // Traverse the sub-graphs
+    if (isResetAfterAnalysis) {
+      // Advance choice counter for sub-graphs
+      choiceCounter++;
+      // Do this for every CG after finishing each backtrack list
+      // We try to update the CG with a backtrack list if the state has been visited multiple times
+      if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
+        int event = cgMap.get(icsCG);
+        LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
+        if (choiceLists != null && choiceLists.peekFirst() != null) {
+          Integer[] choiceList = choiceLists.removeFirst();
+          // Deploy the new choice list for this CG
+          icsCG.setNewValues(choiceList);
+          icsCG.reset();
+        } else {
+          // Set done if this was the last backtrack list
+          icsCG.setDone();
+        }
+        saveVisitedStates();
+      }
+    } else {
+      // Update and reset the CG if needed (do this for the first time after the analysis)
+      // Start backtracking if this is a visited state and it is not a repeating state
+      resetAllCGs();
+      isResetAfterAnalysis = true;
+    }
+  }
+
   @Override
   public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
 
@@ -316,42 +383,10 @@ public class StateReducer extends ListenerAdapter {
       if (currentCG instanceof IntChoiceFromSet) {
         IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
         // Update the current pointer to the current set of choices
-        if (choices == null || choices != icsCG.getAllChoices()) {
-          currCG = icsCG;
-          choices = icsCG.getAllChoices();
-          // Reset a few things for the sub-graph
-          conflictPairMap.clear();
-          readWriteFieldsMap.clear();
-          choiceCounter = 0;
-        }
+        updateChoices(icsCG);
         // Check if we have seen this state or this state contains cycles that involve all events
         if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
-          // Traverse the sub-graphs
-          if (isResetAfterAnalysis) {
-            // Advance choice counter for sub-graphs
-            choiceCounter++;
-            // Do this for every CG after finishing each backtrack list
-            // We try to update the CG with a backtrack list if the state has been visited multiple times
-            if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) {
-              int event = cgMap.get(icsCG);
-              LinkedList<Integer[]> choiceLists = backtrackMap.get(event);
-              if (choiceLists != null && choiceLists.peekFirst() != null) {
-                Integer[] choiceList = choiceLists.removeFirst();
-                // Deploy the new choice list for this CG
-                icsCG.setNewValues(choiceList);
-                icsCG.reset();
-              } else {
-                // Set done if this was the last backtrack list
-                icsCG.setDone();
-              }
-              saveVisitedStates();
-            }
-          } else {
-            // Update and reset the CG if needed (do this for the first time after the analysis)
-            // Start backtracking if this is a visited state and it is not a repeating state
-            resetAllCGs();
-            isResetAfterAnalysis = true;
-          }
+          exploreNextBacktrackSets(icsCG);
         }
         // Update the VOD graph always with the latest
         updateVODGraph(icsCG.getNextChoice());
@@ -379,6 +414,28 @@ public class StateReducer extends ListenerAdapter {
     choiceSet.add(currChoice);
   }
 
+  private void mapStateToEvent(Search search) {
+    // Insert state ID and event choice into the map
+    HashSet<Integer> eventSet;
+    if (stateToEventMap.containsKey(stateId)) {
+      eventSet = stateToEventMap.get(stateId);
+    } else {
+      eventSet = new HashSet<>();
+      stateToEventMap.put(stateId, eventSet);
+    }
+    eventSet.add(prevChoiceValue);
+  }
+
+  private void updateStateInfo(Search search) {
+    if (stateReductionMode) {
+      // Update the state variables
+      // Line 19 in the paper page 11 (see the heading note above)
+      stateId = search.getStateId();
+      currVisitedStates.add(stateId);
+      mapStateToEvent(search);
+    }
+  }
+
   @Override
   public void stateAdvanced(Search search) {
     if (debugMode) {
@@ -398,11 +455,7 @@ public class StateReducer extends ListenerAdapter {
       out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth +
               " which is " + detail + " Transition: " + transition + "\n");
     }
-    if (stateReductionMode) {
-      // Update the state ID variables
-      stateId = search.getStateId();
-      currVisitedStates.add(stateId);
-    }
+    updateStateInfo(search);
   }
 
   @Override
@@ -413,14 +466,10 @@ public class StateReducer extends ListenerAdapter {
       transition = search.getTransition();
       detail = null;
 
-      // Update the state variables
-      // Line 19 in the paper page 11 (see the heading note above)
-      stateId = search.getStateId();
-      currVisitedStates.add(stateId);
-
       out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition +
               " and depth: " + depth + "\n");
     }
+    updateStateInfo(search);
   }
 
   @Override
@@ -680,11 +729,11 @@ public class StateReducer extends ListenerAdapter {
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
     if (stateReductionMode) {
       if (isInitialized) {
-        if (choiceCounter <= 0 || choiceCounter > choices.length - 1) {
+        int currentChoice = (choiceCounter % (choices.length - 1)) - 1;
+        if (currentChoice < 0) {
           // We do not compute the conflicts for the choice '-1'
           return;
         }
-        int currentChoice = choiceCounter - 1;
         // Record accesses from executed instructions
         if (executedInsn instanceof JVMFieldInstruction) {
           // Analyze only after being initialized