Cleaning up: checking source code for (potential) bugs.
authorrtrimana <rtrimana@uci.edu>
Tue, 15 Dec 2020 17:38:17 +0000 (09:38 -0800)
committerrtrimana <rtrimana@uci.edu>
Tue, 15 Dec 2020 17:38:17 +0000 (09:38 -0800)
src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java

index ebc903e..7cfab4d 100755 (executable)
@@ -83,7 +83,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   // Statistics
   private int numOfTransitions;
 
-  public DPORStateReducerSummary(Config config, JPF jpf) {
+  public DPORStateReducerWithSummary(Config config, JPF jpf) {
     verboseMode = config.getBoolean("printout_state_transition", false);
     stateReductionMode = config.getBoolean("activate_state_reduction", true);
     if (verboseMode) {
@@ -622,7 +622,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   // -- PRIVATE CLASSES RELATED TO SUMMARY
   // This class stores the main summary of states
   // 1) Main mapping between state ID and state summary
-  // 2) State summary is a mapping between events and their respective R/W sets
+  // 2) State summary is a mapping between events (i.e., event choices) and their respective R/W sets
   private class MainSummary {
     private HashMap<Integer, HashMap<Integer, ReadWriteSet>> mainSummary;
 
@@ -630,12 +630,12 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       mainSummary = new HashMap<>();
     }
 
-    public Set<Integer> getEventsAtStateId(int stateId) {
+    public Set<Integer> getEventChoicesAtStateId(int stateId) {
       HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
       return stateSummary.keySet();
     }
 
-    public ReadWriteSet getRWSetForEventAtState(int choice, int stateId) {
+    public ReadWriteSet getRWSetForEventChoiceAtState(int choice, int stateId) {
       HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
       return stateSummary.get(choice);
     }
@@ -652,7 +652,8 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
           writeMap.remove(writeField);
         }
       }
-      // Then add everything into the recorded map because these will be traversed
+      // Then add the rest (fields in rwSet but not in recordedRWSet)
+      // 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();
@@ -665,28 +666,29 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
           readMap.remove(readField);
         }
       }
-      // Then add everything into the recorded map because these will be traversed
+      // Then add the rest (fields in rwSet but not in recordedRWSet)
+      // into the recorded map because these will be traversed
       recordedReadMap.putAll(readMap);
 
       return rwSet;
     }
 
-    public ReadWriteSet updateStateSummary(int stateId, int choice, ReadWriteSet rwSet) {
+    public ReadWriteSet updateStateSummary(int stateId, int eventChoice, ReadWriteSet rwSet) {
       // If the state Id has not existed, insert the StateSummary object
-      // If the state Id has existed, find the choice:
-      // 1) If the choice has not existed, insert the ReadWriteSet object
-      // 2) If the choice has existed, perform union between the two ReadWriteSet objects
+      // If the state Id has existed, find the event choice:
+      // 1) If the event choice has not existed, insert the ReadWriteSet object
+      // 2) If the event choice has existed, perform union between the two ReadWriteSet objects
       HashMap<Integer, ReadWriteSet> stateSummary;
       if (!mainSummary.containsKey(stateId)) {
         stateSummary = new HashMap<>();
-        stateSummary.put(choice, rwSet.getCopy());
+        stateSummary.put(eventChoice, rwSet.getCopy());
         mainSummary.put(stateId, stateSummary);
       } else {
         stateSummary = mainSummary.get(stateId);
-        if (!stateSummary.containsKey(choice)) {
-          stateSummary.put(choice, rwSet.getCopy());
+        if (!stateSummary.containsKey(eventChoice)) {
+          stateSummary.put(eventChoice, rwSet.getCopy());
         } else {
-          rwSet = performUnion(stateSummary.get(choice), rwSet);
+          rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
         }
       }
       return rwSet;
@@ -849,7 +851,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       HashSet<Integer> eventSet = new HashSet<>();
       stateToEventMap.put(stateId, eventSet);
     }
-    addPredecessorToRevisitedState(search.getVM(), stateId);
+    addPredecessorToRevisitedState(stateId);
     justVisitedStates.add(stateId);
     if (!prevVisitedStates.contains(stateId)) {
       // It is a currently visited states if the state has not been seen in previous executions
@@ -979,22 +981,22 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     return currentChoice;
   }
 
-  private void createBacktrackingPoint(int currentChoice, Execution conflictExecution, int conflictChoice) {
+  private void createBacktrackingPoint(int eventChoice, Execution conflictExecution, int conflictChoice) {
     // Create a new list of choices for backtrack based on the current choice and conflicting event number
     // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2}
     // for the original set {0, 1, 2, 3}
     
-    // currentChoice represent the event/transaction that will be put into the backtracking set of
+    // eventChoice represent the event/transaction that will be put into the backtracking set of
     // conflictExecution/conflictChoice
     Integer[] newChoiceList = new Integer[refChoices.length];
     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
     int stateId = conflictTrace.get(conflictChoice).getStateId();
     // Check if this trace has been done from this state
-    if (isTraceAlreadyConstructed(currentChoice, stateId)) {
+    if (isTraceAlreadyConstructed(eventChoice, stateId)) {
       return;
     }
     // Put the conflicting event numbers first and reverse the order
-    newChoiceList[0] = currentChoice;
+    newChoiceList[0] = eventChoice;
     // Put the rest of the event numbers into the array starting from the minimum to the upper bound
     for (int i = 0, j = 1; i < refChoices.length; i++) {
       if (refChoices[i] != newChoiceList[0]) {
@@ -1061,14 +1063,14 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
                isEndOfExecution = true;
   }
 
-  private boolean isConflictFound(int reachableEvent, Execution conflictExecution, int conflictChoice,
+  private boolean isConflictFound(int eventChoice, Execution conflictExecution, int conflictChoice,
                                   ReadWriteSet currRWSet) {
     // conflictExecution/conflictChoice represent a predecessor event/transaction that can potentially have a conflict
     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
     HashMap<Integer, ReadWriteSet> confRWFieldsMap = conflictExecution.getReadWriteFieldsMap();
     // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
     if (!confRWFieldsMap.containsKey(conflictChoice) ||
-            reachableEvent == conflictTrace.get(conflictChoice).getChoice()) {
+            eventChoice == conflictTrace.get(conflictChoice).getChoice()) {
       return false;
     }
     // R/W set of choice/event that may have a potential conflict
@@ -1211,15 +1213,15 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
     updateBacktrackSetDFS(execution, currentChoice, confTrans.getChoice(), currRWSet, visited);
   }
 
-  private void updateBacktrackSetDFS(Execution execution, int currentChoice, int conflictEvent,
+  private void updateBacktrackSetDFS(Execution execution, int currentChoice, int conflictEventChoice,
                                      ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
     }
     TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
-    // Record this transition into rGraph summary
-    currRWSet = mainSummary.updateStateSummary(currTrans.getStateId(), currTrans.getChoice(), currRWSet);
+    // Record this transition into the state summary of main summary
+    currRWSet = mainSummary.updateStateSummary(currTrans.getStateId(), conflictEventChoice, currRWSet);
     // Halt when we have visited this transition (in a cycle)
     if (visited.contains(currTrans)) {
       return;
@@ -1231,21 +1233,22 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
       int predecessorChoice = predecessor.getChoice();
       Execution predecessorExecution = predecessor.getExecution();
       // Push up one happens-before transition
-      int newConflictEvent = conflictEvent;
+      int newConflictEventChoice = conflictEventChoice;
       // Check if a conflict is found
-      if (isConflictFound(conflictEvent, predecessorExecution, predecessorChoice, currRWSet)) {
-        createBacktrackingPoint(conflictEvent, predecessorExecution, predecessorChoice);
-        newConflictEvent = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+      if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, currRWSet)) {
+        createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
+        // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+        newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
       }
       // Continue performing DFS if conflict is not found
-      updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEvent,
+      updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
               currRWSet, visited);
     }
   }
 
   // --- Functions related to the reachability analysis when there is a state match
 
-  private void addPredecessorToRevisitedState(VM vm, int stateId) {
+  private void addPredecessorToRevisitedState(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),
@@ -1265,10 +1268,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter {
   // Update the backtrack sets from previous executions
   private void updateBacktrackSetsFromGraph(int stateId, Execution currExecution, int currChoice) {
     // Get events/choices at this state ID
-    Set<Integer> eventsAtStateId = mainSummary.getEventsAtStateId(stateId);
+    Set<Integer> eventsAtStateId = mainSummary.getEventChoicesAtStateId(stateId);
     for (Integer event : eventsAtStateId) {
       // Get the ReadWriteSet object for this event at state ID
-      ReadWriteSet rwSet = mainSummary.getRWSetForEventAtState(event, stateId);
+      ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(event, stateId);
       // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
       HashSet<TransitionEvent> visited = new HashSet<>();
       // Update the backtrack sets recursively