X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=a0abd98c66033b353d880917c36cce2ab59b6a61;hb=35a177a2fce7cc83df80e5878b4a2e095f873597;hp=5ce8c40843c30b69c5f227c4b5c8191d540fd8a0;hpb=4e993c925c92846b87cdae46a59194352c1e8a60;p=jpf-core.git 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 5ce8c40..a0abd98 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -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 @@ -531,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 @@ -539,6 +541,7 @@ public class DPORStateReducer extends ListenerAdapter { choiceCounter = 0; execution = null; predecessors = new HashSet<>(); + recordedPredecessors = new HashMap<>(); stateId = 0; transitionCG = null; } @@ -565,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) { @@ -699,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<>(); @@ -727,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) { - if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) { - return true; + // We only flip the value of terminate once ... + if (!terminate && prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) { + 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) { @@ -743,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 } } @@ -949,7 +983,7 @@ 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; } @@ -1058,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; } @@ -1100,41 +1134,9 @@ 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, 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, ReadWriteSet currRWSet, HashSet visited) { @@ -1159,39 +1161,36 @@ public class DPORStateReducer extends ListenerAdapter { // Check if a conflict is found if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) { createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice); - newConflictChoice = conflictChoice; - newConflictExecution = conflictExecution; + newConflictChoice = predecessorChoice; + newConflictExecution = predecessorExecution; } // Continue performing DFS if conflict is not found 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 - //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) {