Adding reachability graph for past executions.
authorrtrimana <rtrimana@uci.edu>
Fri, 1 May 2020 22:47:12 +0000 (15:47 -0700)
committerrtrimana <rtrimana@uci.edu>
Fri, 1 May 2020 22:47:12 +0000 (15:47 -0700)
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index 6ba35e7..4645d2c 100644 (file)
@@ -82,6 +82,7 @@ public class DPORStateReducer extends ListenerAdapter {
   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;      // Record fields that are accessed
   private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
   private HashMap<Integer, Integer> stateToChoiceCounterMap;      // Maps state IDs to the choice counter
+  private HashMap<Integer, ReachabilityGraph> stateToRGraph;      // Maps state IDs to a ReachabilityGraph
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -251,6 +252,7 @@ public class DPORStateReducer extends ListenerAdapter {
         // 1) if we have seen this state or this state contains cycles that involve all events, and
         // 2) after the current CG is advanced at least once
         if (terminateCurrentExecution() && choiceCounter > 0) {
+          saveExecutionInfo();
           exploreNextBacktrackPoints(vm, icsCG);
         } else {
           numOfTransitions++;
@@ -385,6 +387,26 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
+  // This class stores a compact representation of a reachability graph for past executions
+  private class ReachabilityGraph {
+    private ArrayList<BacktrackPoint> pastBacktrackPointList;
+    private HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap;
+
+    public ReachabilityGraph(ArrayList<BacktrackPoint> btrackPointList,
+                             HashMap<Integer, ReadWriteSet> rwFieldsMap) {
+      pastBacktrackPointList = btrackPointList;
+      pastReadWriteFieldsMap = rwFieldsMap;
+    }
+
+    public ArrayList<BacktrackPoint> getPastBacktrackPointList() {
+      return pastBacktrackPointList;
+    }
+
+    public HashMap<Integer, ReadWriteSet> getPastReadWriteFieldsMap() {
+      return pastReadWriteFieldsMap;
+    }
+  }
+
   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
@@ -476,6 +498,7 @@ public class DPORStateReducer extends ListenerAdapter {
     doneBacktrackSet = new HashSet<>();
     readWriteFieldsMap = new HashMap<>();
     stateToChoiceCounterMap = new HashMap<>();
+    stateToRGraph = new HashMap<>();
     // Booleans
     isEndOfExecution = false;
   }
@@ -630,9 +653,8 @@ public class DPORStateReducer extends ListenerAdapter {
     // for the original set {0, 1, 2, 3}
     Integer[] newChoiceList = new Integer[refChoices.length];
     // Put the conflicting event numbers first and reverse the order
-    int actualCurrCho = currentChoice % refChoices.length;
     // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method
-    newChoiceList[0] = choices[actualCurrCho];
+    newChoiceList[0] = backtrackPointList.get(currentChoice).getChoice();
     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++) {
@@ -722,10 +744,9 @@ public class DPORStateReducer extends ListenerAdapter {
 
   private boolean isConflictFound(int eventCounter, int currentChoice) {
 
-    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] == backtrackPointList.get(eventCounter).getChoice()) {
+            backtrackPointList.get(currentChoice).getChoice() == backtrackPointList.get(eventCounter).getChoice()) {
       return false;
     }
     // Current R/W set
@@ -826,12 +847,13 @@ public class DPORStateReducer extends ListenerAdapter {
       choiceCounter = 0;
       choices = icsCG.getAllChoices();
       refChoices = copyChoices(choices);
-      // Clearing data structures
-      conflictPairMap.clear();
-      readWriteFieldsMap.clear();
-      stateToEventMap.clear();
+      // Clear data structures
+      backtrackPointList = new ArrayList<>();
+      conflictPairMap = new HashMap<>();
+      readWriteFieldsMap = new HashMap<>();
+      stateToChoiceCounterMap = new HashMap<>();
+      stateToEventMap = new HashMap<>();
       isEndOfExecution = false;
-      backtrackPointList.clear();
     }
   }
 
@@ -861,20 +883,87 @@ public class DPORStateReducer extends ListenerAdapter {
     // 3) at least 2 choices/events have been explored (choiceCounter > 1),
     // 4) the matched state has been encountered in the current execution, and
     // 5) state > 0 (state 0 is for boolean CG)
-    if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 &&
-            currVisitedStates.contains(stateId) && (stateId > 0)) {
-      // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
-      int conflictChoice = stateToChoiceCounterMap.get(stateId);
-      int currentChoice = choiceCounter - 1;
-      // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
-      while (conflictChoice < currentChoice) {
-        for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) {
-          if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
-            createBacktrackingPoint(conflictChoice, eventCounter);
-          }
+    if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && (stateId > 0)) {
+      if (currVisitedStates.contains(stateId)) {
+        // Update the backtrack sets in the cycle
+        updateBacktrackSetsInCycle(stateId);
+      } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
+        // Update the backtrack sets in a previous execution
+        updateBacktrackSetsInPreviousExecution(stateId);
+      }
+    }
+  }
+
+  // Save the information from this execution for future reachability analysis
+  private void saveExecutionInfo() {
+    Set<Integer> states = stateToChoiceCounterMap.keySet();
+    ReachabilityGraph reachabilityGraph = new
+            ReachabilityGraph(backtrackPointList, readWriteFieldsMap);
+    // Map all the states visited in this execution to the same ReachabilityGraph object for fast access
+    for(Integer state : states) {
+      if (!prevVisitedStates.contains(state)) {
+        stateToRGraph.put(state, reachabilityGraph);
+      }
+    }
+  }
+
+  // Update the backtrack sets in the cycle
+  private void updateBacktrackSetsInCycle(int stateId) {
+    // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
+    int conflictChoice = stateToChoiceCounterMap.get(stateId);
+    int currentChoice = choiceCounter - 1;
+    // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
+    while (conflictChoice < currentChoice) {
+      for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) {
+        if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
+          createBacktrackingPoint(conflictChoice, eventCounter);
+        }
+      }
+      conflictChoice++;
+    }
+  }
+
+  private int getPastConflictChoice(int stateId, ArrayList<BacktrackPoint> pastBacktrackPointList) {
+    // Iterate and find the first occurrence of the state ID
+    // It is guaranteed that a choice should be found because the state ID is in the list
+    int pastConfChoice = 0;
+    for(int i = 0; i<pastBacktrackPointList.size(); i++) {
+      BacktrackPoint backtrackPoint = pastBacktrackPointList.get(i);
+      int stId = backtrackPoint.getStateId();
+      if (stId == stateId) {
+        pastConfChoice = i;
+        break;
+      }
+    }
+    return pastConfChoice;
+  }
+
+  // Update the backtrack sets in a previous execution
+  private void updateBacktrackSetsInPreviousExecution(int stateId) {
+    // Find the right ReachabilityGraph object that contains the stateId
+    ReachabilityGraph rGraph = stateToRGraph.get(stateId);
+    // Find the choice/event that marks the start of the subtrace from the previous execution
+    ArrayList<BacktrackPoint> pastBacktrackPointList = rGraph.getPastBacktrackPointList();
+    HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rGraph.getPastReadWriteFieldsMap();
+    int pastConfChoice = getPastConflictChoice(stateId, pastBacktrackPointList);
+    int conflictChoice = choiceCounter;
+    // Iterate from the starting point until the end of the past execution trace
+    while (pastConfChoice < pastBacktrackPointList.size() - 1) {  // BacktrackPoint list always has a surplus of 1
+      // Get the info of the event from the past execution trace
+      BacktrackPoint confBtrackPoint = pastBacktrackPointList.get(pastConfChoice);
+      ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
+      // Append this event to the current list and map
+      backtrackPointList.add(confBtrackPoint);
+      readWriteFieldsMap.put(choiceCounter, rwSet);
+      for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) {
+        if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
+          createBacktrackingPoint(conflictChoice, eventCounter);
         }
-        conflictChoice++;
       }
+      // Remove this event to replace it with a new one
+      backtrackPointList.remove(backtrackPointList.size() - 1);
+      readWriteFieldsMap.remove(choiceCounter);
+      pastConfChoice++;
     }
   }
 }