Making the implementation of updateBacktrackSetDFS closer to the paper in DPORStateRe...

[jpf-core.git] / src / main / gov / nasa / jpf / listener / DPORStateReducer.java

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index 0da718cb6e43f787387ddbd99b0fe446248dc955..5ce8c40843c30b69c5f227c4b5c8191d540fd8a0 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -20,8 +20,9 @@ package gov.nasa.jpf.listener;
 import gov.nasa.jpf.Config;
 import gov.nasa.jpf.JPF;
 import gov.nasa.jpf.ListenerAdapter;
+import gov.nasa.jpf.jvm.bytecode.INVOKEINTERFACE;
+import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
 import gov.nasa.jpf.search.Search;
-import gov.nasa.jpf.jvm.bytecode.*;
 import gov.nasa.jpf.vm.*;
 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
@@ -29,10 +30,10 @@ import gov.nasa.jpf.vm.choice.IntChoiceFromSet;
 import gov.nasa.jpf.vm.choice.IntIntervalGenerator;
 
 import java.io.FileWriter;
+import java.io.IOException;
 import java.io.PrintWriter;
 import java.util.*;
 import java.util.logging.Logger;
-import java.io.IOException;
 
 /**
  * This a DPOR implementation for event-driven applications with loops that create cycles of state matching
@@ -80,7 +81,7 @@ public class DPORStateReducer extends ListenerAdapter {
 
   // Statistics
   private int numOfTransitions;
-       
+
   public DPORStateReducer(Config config, JPF jpf) {
     verboseMode = config.getBoolean("printout_state_transition", false);
     stateReductionMode = config.getBoolean("activate_state_reduction", true);
@@ -873,6 +874,9 @@ public class DPORStateReducer extends ListenerAdapter {
     // 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}
+    
+    // execution/currentChoice represent the event/transaction that will be put into the backtracking set of
+    // conflictExecution/conflictChoice
     Integer[] newChoiceList = new Integer[refChoices.length];
     ArrayList<TransitionEvent> currentTrace = execution.getExecutionTrace();
     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
@@ -952,6 +956,7 @@ public class DPORStateReducer extends ListenerAdapter {
 
   private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice,
                                   ReadWriteSet currRWSet) {
+    // conflictExecution/conflictChoice represent a predecessor event/transaction that can potentially have a conflict
     ArrayList<TransitionEvent> executionTrace = execution.getExecutionTrace();
     ArrayList<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
     HashMap<Integer, ReadWriteSet> confRWFieldsMap = conflictExecution.getReadWriteFieldsMap();
@@ -1098,7 +1103,7 @@ public class DPORStateReducer extends ListenerAdapter {
     // TODO: The following is the call to the original version of the method
 //    updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
     // TODO: The following is the call to the version of the method with pushing up happens-before transitions
-    updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, execution, currentChoice, currRWSet, visited);
+    updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
   }
 
 //  TODO: This is the original version of the recursive method
@@ -1132,35 +1137,34 @@ public class DPORStateReducer extends ListenerAdapter {
   // TODO: This is the version of the method with pushing up happens-before transitions
   private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
                                            Execution conflictExecution, int conflictChoice,
-                                           Execution hbExecution, int hbChoice,
                                            ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
     // Halt when we have found the first read/write conflicts for all memory locations
     if (currRWSet.isEmpty()) {
       return;
     }
-    TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
+    TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
     // Halt when we have visited this transition (in a cycle)
-    if (visited.contains(confTrans)) {
+    if (visited.contains(currTrans)) {
       return;
     }
-    visited.add(confTrans);
+    visited.add(currTrans);
     // Explore all predecessors
-    for (Predecessor predecessor : confTrans.getPredecessors()) {
+    for (Predecessor predecessor : currTrans.getPredecessors()) {
       // Get the predecessor (previous conflict choice)
-      conflictChoice = predecessor.getChoice();
-      conflictExecution = predecessor.getExecution();
+      int predecessorChoice = predecessor.getChoice();
+      Execution predecessorExecution = predecessor.getExecution();
       // Push up one happens-before transition
-      int pushedChoice = hbChoice;
-      Execution pushedExecution = hbExecution;
+      int newConflictChoice = conflictChoice;
+      Execution newConflictExecution = conflictExecution;
       // Check if a conflict is found
-      if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
-        createBacktrackingPoint(pushedExecution, pushedChoice, conflictExecution, conflictChoice);
-        pushedChoice = conflictChoice;
-        pushedExecution = conflictExecution;
+      if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
+        createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
+        newConflictChoice = conflictChoice;
+        newConflictExecution = conflictExecution;
       }
       // Continue performing DFS if conflict is not found
-      updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice,
-              pushedExecution, pushedChoice, currRWSet, visited);
+      updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
+              currRWSet, visited);
     }
     // Remove the transition after being explored
     // TODO: Seems to cause a lot of loops---commented out for now