From 4e993c925c92846b87cdae46a59194352c1e8a60 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Tue, 8 Sep 2020 11:22:47 -0700 Subject: [PATCH] Making the implementation of updateBacktrackSetDFS closer to the paper in DPORStateReducer.java. --- .../nasa/jpf/listener/DPORStateReducer.java | 42 ++++++++++--------- 1 file changed, 23 insertions(+), 19 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 0da718c..5ce8c40 100644 --- 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 currentTrace = execution.getExecutionTrace(); ArrayList 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 executionTrace = execution.getExecutionTrace(); ArrayList conflictTrace = conflictExecution.getExecutionTrace(); HashMap 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 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 -- 2.34.1