X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=82f3db8bd94a50b0aa290d00f1a50458cf15fd36;hp=ef0994cbdeba690d46c526b1016c54a488bc09dc;hb=461ece5d48c8a96e967b2670802406d1d4157df3;hpb=42c68a0ac3563a679987c53ce282d6807cd3d9d6 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java old mode 100644 new mode 100755 index ef0994c..82f3db8 --- 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,11 +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.lang.reflect.Field; 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 @@ -60,7 +60,7 @@ public class DPORStateReducer extends ListenerAdapter { private int choiceCounter; private int maxEventChoice; // Data structure to track the events seen by each state to track cycles (containing all events) for termination - private HashSet currVisitedStates; // States being visited in the current execution + private HashMap currVisitedStates; // States visited in the current execution (maps to frequency) private HashSet justVisitedStates; // States just visited in the previous choice/event private HashSet prevVisitedStates; // States visited in the previous execution private HashSet nonRelevantClasses;// Class info objects of non-relevant classes @@ -71,7 +71,7 @@ public class DPORStateReducer extends ListenerAdapter { private HashMap> backtrackMap; // Track created backtracking points private PriorityQueue backtrackStateQ; // Heap that returns the latest state private Execution currentExecution; // Holds the information about the current execution - private HashSet doneBacktrackSet; // Record state ID and trace already constructed + private HashMap> doneBacktrackMap; // Record state ID and trace already constructed private HashMap restorableStateMap; // Maps state IDs to the restorable state object private RGraph rGraph; // R-Graph for past executions @@ -80,9 +80,8 @@ public class DPORStateReducer extends ListenerAdapter { private boolean isEndOfExecution; // Statistics - private int numOfConflicts; private int numOfTransitions; - + public DPORStateReducer(Config config, JPF jpf) { verboseMode = config.getBoolean("printout_state_transition", false); stateReductionMode = config.getBoolean("activate_state_reduction", true); @@ -99,7 +98,6 @@ public class DPORStateReducer extends ListenerAdapter { } } isBooleanCGFlipped = false; - numOfConflicts = 0; numOfTransitions = 0; nonRelevantClasses = new HashSet<>(); nonRelevantFields = new HashSet<>(); @@ -171,19 +169,13 @@ public class DPORStateReducer extends ListenerAdapter { @Override public void searchFinished(Search search) { - if (stateReductionMode) { - // Number of conflicts = first trace + subsequent backtrack points - numOfConflicts += 1 + doneBacktrackSet.size(); - } if (verboseMode) { out.println("\n==> DEBUG: ----------------------------------- search finished"); out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode); - out.println("\n==> DEBUG: Number of conflicts : " + numOfConflicts); out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions); out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n"); fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode); - fileWriter.println("==> DEBUG: Number of conflicts : " + numOfConflicts); fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions); fileWriter.println(); fileWriter.close(); @@ -196,6 +188,8 @@ public class DPORStateReducer extends ListenerAdapter { // Initialize with necessary information from the CG if (nextCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG; + // Tell JPF that we are performing DPOR + icsCG.setDpor(); if (!isEndOfExecution) { // Check if CG has been initialized, otherwise initialize it Integer[] cgChoices = icsCG.getAllChoices(); @@ -228,8 +222,6 @@ public class DPORStateReducer extends ListenerAdapter { if (!isBooleanCGFlipped) { isBooleanCGFlipped = true; } else { - // Number of conflicts = first trace + subsequent backtrack points - numOfConflicts = 1 + doneBacktrackSet.size(); // Allocate new objects for data structure when the boolean is flipped from "false" to "true" initializeStatesVariables(); } @@ -352,6 +344,10 @@ public class DPORStateReducer extends ListenerAdapter { return executionTrace.get(0); } + public TransitionEvent getLastTransition() { + return executionTrace.get(executionTrace.size() - 1); + } + public HashMap getReadWriteFieldsMap() { return readWriteFieldsMap; } @@ -421,6 +417,12 @@ public class DPORStateReducer extends ListenerAdapter { } public HashSet getReachableTransitionsAtState(int stateId) { + if (!graph.containsKey(stateId)) { + // This is a loop from a transition to itself, so just return the current transition + HashSet transitionSet = new HashSet<>(); + transitionSet.add(currentExecution.getLastTransition()); + return transitionSet; + } return graph.get(stateId); } @@ -428,7 +430,11 @@ public class DPORStateReducer extends ListenerAdapter { HashSet reachableTransitions = new HashSet<>(); // All transitions from states higher than the given state ID (until the highest state ID) are reachable for(int stId = stateId; stId <= hiStateId; stId++) { - reachableTransitions.addAll(graph.get(stId)); + // We might encounter state IDs from the first round of Boolean CG + // The second round of Boolean CG should consider these new states + if (graph.containsKey(stId)) { + reachableTransitions.addAll(graph.get(stId)); + } } return reachableTransitions; } @@ -525,6 +531,8 @@ public class DPORStateReducer extends ListenerAdapter { private int choiceCounter; // Choice counter at this transition private Execution execution; // The execution where this transition belongs private HashSet predecessors; // Maps incoming events/transitions (execution and choice) + private HashMap> recordedPredecessors; + // Memorize event and choice number to not record them twice private int stateId; // State at this transition private IntChoiceFromSet transitionCG; // CG at this transition @@ -533,6 +541,7 @@ public class DPORStateReducer extends ListenerAdapter { choiceCounter = 0; execution = null; predecessors = new HashSet<>(); + recordedPredecessors = new HashMap<>(); stateId = 0; transitionCG = null; } @@ -559,8 +568,28 @@ public class DPORStateReducer extends ListenerAdapter { public IntChoiceFromSet getTransitionCG() { return transitionCG; } + private boolean isRecordedPredecessor(Execution execution, int choice) { + // See if we have recorded this predecessor earlier + HashSet recordedChoices; + if (recordedPredecessors.containsKey(execution)) { + recordedChoices = recordedPredecessors.get(execution); + if (recordedChoices.contains(choice)) { + return true; + } + } else { + recordedChoices = new HashSet<>(); + recordedPredecessors.put(execution, recordedChoices); + } + // Record the choice if we haven't seen it + recordedChoices.add(choice); + + return false; + } + public void recordPredecessor(Execution execution, int choice) { - predecessors.add(new Predecessor(choice, execution)); + if (!isRecordedPredecessor(execution, choice)) { + predecessors.add(new Predecessor(choice, execution)); + } } public void setChoice(int cho) { @@ -636,8 +665,10 @@ public class DPORStateReducer extends ListenerAdapter { } currentExecution.mapCGToChoice(icsCG, choiceCounter); // Store restorable state object for this state (always store the latest) - RestorableVMState restorableState = vm.getRestorableState(); - restorableStateMap.put(stateId, restorableState); + if (!restorableStateMap.containsKey(stateId)) { + RestorableVMState restorableState = vm.getRestorableState(); + restorableStateMap.put(stateId, restorableState); + } } private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) { @@ -691,7 +722,7 @@ public class DPORStateReducer extends ListenerAdapter { choiceCounter = 0; maxEventChoice = 0; // Cycle tracking - currVisitedStates = new HashSet<>(); + currVisitedStates = new HashMap<>(); justVisitedStates = new HashSet<>(); prevVisitedStates = new HashSet<>(); stateToEventMap = new HashMap<>(); @@ -700,7 +731,7 @@ public class DPORStateReducer extends ListenerAdapter { backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); currentExecution = new Execution(); currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point - doneBacktrackSet = new HashSet<>(); + doneBacktrackMap = new HashMap<>(); rGraph = new RGraph(); // Booleans isEndOfExecution = false; @@ -719,12 +750,19 @@ public class DPORStateReducer extends ListenerAdapter { private boolean terminateCurrentExecution() { // We need to check all the states that have just been visited // Often a transition (choice/event) can result into forwarding/backtracking to a number of states + boolean terminate = false; for(Integer stateId : justVisitedStates) { + // We perform updates on backtrack sets for every if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) { - return true; + updateBacktrackSetsFromGraph(stateId); + terminate = true; + } + // If frequency > 1 then this means we have visited this stateId more than once + if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) { + updateBacktrackSetsFromGraph(stateId); } } - return false; + return terminate; } private void updateStateInfo(Search search) { @@ -735,11 +773,15 @@ public class DPORStateReducer extends ListenerAdapter { HashSet eventSet = new HashSet<>(); stateToEventMap.put(stateId, eventSet); } - analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); + addPredecessorToRevisitedState(search.getVM(), stateId); justVisitedStates.add(stateId); if (!prevVisitedStates.contains(stateId)) { // It is a currently visited states if the state has not been seen in previous executions - currVisitedStates.add(stateId); + int frequency = 0; + if (currVisitedStates.containsKey(stateId)) { + frequency = currVisitedStates.get(stateId); + } + currVisitedStates.put(stateId, frequency + 1); // Increment frequency counter } } @@ -866,6 +908,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(); @@ -938,13 +983,14 @@ public class DPORStateReducer extends ListenerAdapter { icsCG.setDone(); } // Save all the visited states when starting a new execution of trace - prevVisitedStates.addAll(currVisitedStates); + prevVisitedStates.addAll(currVisitedStates.keySet()); // This marks a transitional period to the new CG isEndOfExecution = true; } 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(); @@ -1021,19 +1067,20 @@ public class DPORStateReducer extends ListenerAdapter { // Check if this trace is already constructed private boolean isTraceAlreadyConstructed(int firstChoice, int stateId) { // Concatenate state ID and only the first event in the string, e.g., "1:1 for the trace 10234 at state 1" - // TODO: THIS IS AN OPTIMIZATION! - // This is the optimized version because after we execute, e.g., the trace 1:10234, we don't need to try - // another trace that starts with event 1 at state 1, e.g., the trace 1:13024 - // The second time this event 1 is explored, it will generate the same state as the first one - StringBuilder sb = new StringBuilder(); - sb.append(stateId); - sb.append(':'); - sb.append(firstChoice); // Check if the trace has been constructed as a backtrack point for this state - if (doneBacktrackSet.contains(sb.toString())) { - return true; + // TODO: THIS IS AN OPTIMIZATION! + HashSet choiceSet; + if (doneBacktrackMap.containsKey(stateId)) { + choiceSet = doneBacktrackMap.get(stateId); + if (choiceSet.contains(firstChoice)) { + return true; + } + } else { + choiceSet = new HashSet<>(); + doneBacktrackMap.put(stateId, choiceSet); } - doneBacktrackSet.add(sb.toString()); + choiceSet.add(firstChoice); + return false; } @@ -1045,7 +1092,7 @@ public class DPORStateReducer extends ListenerAdapter { choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); // Clear data structures - currVisitedStates = new HashSet<>(); + currVisitedStates = new HashMap<>(); stateToEventMap = new HashMap<>(); isEndOfExecution = false; } @@ -1087,98 +1134,63 @@ public class DPORStateReducer extends ListenerAdapter { // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle HashSet visited = new HashSet<>(); // Update backtrack set recursively - // 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 -// private void updateBacktrackSetRecursive(Execution execution, int currentChoice, -// Execution conflictExecution, int conflictChoice, -// 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); -// // Halt when we have visited this transition (in a cycle) -// if (visited.contains(confTrans)) { -// return; -// } -// visited.add(confTrans); -// // Explore all predecessors -// for (Predecessor predecessor : confTrans.getPredecessors()) { -// // Get the predecessor (previous conflict choice) -// conflictChoice = predecessor.getChoice(); -// conflictExecution = predecessor.getExecution(); -// // Check if a conflict is found -// if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) { -// createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice); -// } -// // Continue performing DFS if conflict is not found -// updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited); -// } -// } - - // 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 = predecessorChoice; + newConflictExecution = predecessorExecution; } // 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 - visited.remove(confTrans); } // --- Functions related to the reachability analysis when there is a state match - private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { + private void addPredecessorToRevisitedState(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)) { + if ((currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) || + prevVisitedStates.contains(stateId)) { // Update reachable transitions in the graph with a predecessor HashSet reachableTransitions = rGraph.getReachableTransitionsAtState(stateId); - for(TransitionEvent transition : reachableTransitions) { + for (TransitionEvent transition : reachableTransitions) { transition.recordPredecessor(currentExecution, choiceCounter - 1); } - updateBacktrackSetsFromPreviousExecution(stateId); } } } // Update the backtrack sets from previous executions - private void updateBacktrackSetsFromPreviousExecution(int stateId) { + private void updateBacktrackSetsFromGraph(int stateId) { // Collect all the reachable transitions from R-Graph HashSet reachableTransitions = rGraph.getReachableTransitions(stateId); for(TransitionEvent transition : reachableTransitions) {