X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;h=7cfab4d541b99d03572874320c5d161f487c9616;hp=ebc903e17439e9c8877702a0bf892146985ac003;hb=6ea412a2a11e413620d5f133e1ba2484d04f374e;hpb=2e076991b2c61a9a1257d6b51a1a5f12b3463a01 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java index ebc903e..7cfab4d 100755 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java @@ -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> mainSummary; @@ -630,12 +630,12 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { mainSummary = new HashMap<>(); } - public Set getEventsAtStateId(int stateId) { + public Set getEventChoicesAtStateId(int stateId) { HashMap stateSummary = mainSummary.get(stateId); return stateSummary.keySet(); } - public ReadWriteSet getRWSetForEventAtState(int choice, int stateId) { + public ReadWriteSet getRWSetForEventChoiceAtState(int choice, int stateId) { HashMap 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 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 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 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 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 conflictTrace = conflictExecution.getExecutionTrace(); HashMap 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 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 eventsAtStateId = mainSummary.getEventsAtStateId(stateId); + Set 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 visited = new HashSet<>(); // Update the backtrack sets recursively