Initial implementation of more efficient traversal with graph summary; pretty much...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
index 876d34fd1ae45479ebfe36db0eb66dda2ecdc62f..bb617af63c656f8efa9992e5938705c36f51f178 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java
@@ -392,13 +392,19 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
   private class RGraph {
     private int hiStateId;                                     // Maximum state Id
     private HashMap<Integer, HashSet<TransitionEvent>> graph;  // Reachable transitions from past executions
+    // TODO: THIS IS THE ACCESS SUMMARY
+    private HashMap<Integer, HashMap<Integer, ReadWriteSet>> graphSummary;
+    private HashMap<Integer, HashMap<Integer, TransitionEvent>> eventSummary;
 
     public RGraph() {
       hiStateId = 0;
       graph = new HashMap<>();
+      graphSummary = new HashMap<>();
+      eventSummary = new HashMap<>();
     }
 
     public void addReachableTransition(int stateId, TransitionEvent transition) {
+      // Record transition into graph
       HashSet<TransitionEvent> transitionSet;
       if (graph.containsKey(stateId)) {
         transitionSet = graph.get(stateId);
@@ -438,6 +444,73 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       }
       return reachableTransitions;
     }
+
+    public HashMap<Integer, TransitionEvent> getReachableSummaryTransitions(int stateId) {
+      return eventSummary.get(stateId);
+    }
+
+    public HashMap<Integer, ReadWriteSet> getReachableSummaryRWSets(int stateId) {
+      return graphSummary.get(stateId);
+    }
+
+    private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
+      // Combine the same write accesses and record in the recordedRWSet
+      HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
+      HashMap<String, Integer> writeMap = rwSet.getWriteMap();
+      for(Map.Entry<String, Integer> entry : recordedWriteMap.entrySet()) {
+        String writeField = entry.getKey();
+        // Remove the entry from rwSet if both field and object ID are the same
+        if (writeMap.containsKey(writeField) &&
+                (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
+          writeMap.remove(writeField);
+        }
+      }
+      // Then add everything into the recorded map because these will be traversed
+      recordedWriteMap.putAll(writeMap);
+      // Combine the same read accesses and record in the recordedRWSet
+      HashMap<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
+      HashMap<String, Integer> readMap = rwSet.getReadMap();
+      for(Map.Entry<String, Integer> entry : recordedReadMap.entrySet()) {
+        String readField = entry.getKey();
+        // Remove the entry from rwSet if both field and object ID are the same
+        if (readMap.containsKey(readField) &&
+                (readMap.get(readField) == recordedReadMap.get(readField))) {
+          readMap.remove(readField);
+        }
+      }
+      // Then add everything into the recorded map because these will be traversed
+      recordedReadMap.putAll(readMap);
+
+      return rwSet;
+    }
+
+    public ReadWriteSet recordTransitionSummary(int stateId, TransitionEvent transition, ReadWriteSet rwSet) {
+      // Record transition into graphSummary
+      // TransitionMap maps event (choice) number to a R/W set
+      HashMap<Integer, ReadWriteSet> transitionMap;
+      if (graphSummary.containsKey(stateId)) {
+        transitionMap = graphSummary.get(stateId);
+      } else {
+        transitionMap = new HashMap<>();
+        graphSummary.put(stateId, transitionMap);
+      }
+      int choice = transition.getChoice();
+      ReadWriteSet recordedRWSet;
+      // Insert transition into the map if we haven't had this event number recorded
+      if (!transitionMap.containsKey(choice)) {
+        recordedRWSet = rwSet.getCopy();
+        transitionMap.put(choice, recordedRWSet);
+        // Insert the actual TransitionEvent object into the map
+        HashMap<Integer, TransitionEvent> eventMap = new HashMap<>();
+        eventMap.put(choice, transition);
+        eventSummary.put(stateId, eventMap);
+      } else {
+        recordedRWSet = transitionMap.get(choice);
+        // Perform union and subtraction between the recorded and the given R/W sets
+        rwSet = performUnion(recordedRWSet, rwSet);
+      }
+      return rwSet;
+    }
   }
 
   // This class compactly stores Read and Write field sets
@@ -1162,6 +1235,10 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
         newConflictChoice = conflictChoice;
         newConflictExecution = conflictExecution;
       }
+      // TODO: THIS IS THE ACCESS SUMMARY
+      // Record this transition into rGraph summary
+      int stateId = predecessor.getExecution().getExecutionTrace().get(predecessorChoice).getStateId();
+      currRWSet = rGraph.recordTransitionSummary(stateId, currTrans, currRWSet);
       // Continue performing DFS if conflict is not found
       updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
               currRWSet, visited);
@@ -1173,7 +1250,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
 
   // --- Functions related to the reachability analysis when there is a state match
 
-  private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
+  /*private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
     // Perform this analysis only when:
     // 1) this is not during a switch to a new execution,
     // 2) at least 2 choices/events have been explored (choiceCounter > 1),
@@ -1199,5 +1276,40 @@ public class DPORStateReducerEfficient extends ListenerAdapter {
       int currentChoice = transition.getChoiceCounter();
       updateBacktrackSet(execution, currentChoice);
     }
+  }*/
+
+  // TODO: THIS IS THE ACCESS SUMMARY
+  private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
+    // Perform this analysis only when:
+    // 1) this is not during a switch to a new execution,
+    // 2) at least 2 choices/events have been explored (choiceCounter > 1),
+    // 3) state > 0 (state 0 is for boolean CG)
+    if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
+      if (currVisitedStates.contains(stateId) || prevVisitedStates.contains(stateId)) {
+        // Update reachable transitions in the graph with a predecessor
+        HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
+        for(TransitionEvent transition : reachableTransitions) {
+          transition.recordPredecessor(currentExecution, choiceCounter - 1);
+        }
+        updateBacktrackSetsFromPreviousExecution(currentExecution, choiceCounter - 1, stateId);
+      }
+    }
+  }
+
+  private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) {
+    // Collect all the reachable transitions from R-Graph
+    HashMap<Integer, TransitionEvent> reachableTransitions = rGraph.getReachableSummaryTransitions(stateId);
+    HashMap<Integer, ReadWriteSet> reachableRWSets = rGraph.getReachableSummaryRWSets(stateId);
+    for(Map.Entry<Integer, TransitionEvent> transition : reachableTransitions.entrySet()) {
+      TransitionEvent reachableTransition = transition.getValue();
+      Execution conflictExecution = reachableTransition.getExecution();
+      int conflictChoice = reachableTransition.getChoiceCounter();
+      // Copy ReadWriteSet object
+      ReadWriteSet currRWSet = reachableRWSets.get(transition.getKey());
+      currRWSet = currRWSet.getCopy();
+      // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
+      HashSet<TransitionEvent> visited = new HashSet<>();
+      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
+    }
   }
 }