// 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) {
// -- 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<Integer, HashMap<Integer, ReadWriteSet>> mainSummary;
mainSummary = new HashMap<>();
}
- public Set<Integer> getEventsAtStateId(int stateId) {
+ public Set<Integer> getEventChoicesAtStateId(int stateId) {
HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
return stateSummary.keySet();
}
- public ReadWriteSet getRWSetForEventAtState(int choice, int stateId) {
+ public ReadWriteSet getRWSetForEventChoiceAtState(int choice, int stateId) {
HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
return stateSummary.get(choice);
}
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<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
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<Integer, ReadWriteSet> 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;
HashSet<Integer> 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
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<TransitionEvent> 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]) {
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<TransitionEvent> conflictTrace = conflictExecution.getExecutionTrace();
HashMap<Integer, ReadWriteSet> 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) ||
- eventChoice == conflictTrace.get(conflictChoice).getChoice()) {
- reachableEvent == conflictTrace.get(conflictChoice).getChoice()) {
++ if (!confRWFieldsMap.containsKey(conflictChoice) || eventChoice == conflictTrace.get(conflictChoice).getChoice()) {
return false;
}
// R/W set of choice/event that may have a potential conflict
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<TransitionEvent> 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;
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),
// Update the backtrack sets from previous executions
private void updateBacktrackSetsFromGraph(int stateId, Execution currExecution, int currChoice) {
// Get events/choices at this state ID
- Set<Integer> eventsAtStateId = mainSummary.getEventsAtStateId(stateId);
+ Set<Integer> 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<TransitionEvent> visited = new HashSet<>();
// Update the backtrack sets recursively
projects / jpf-core.git / commitdiff