// Explore the next backtrack point:
// 1) if we have seen this state or this state contains cycles that involve all events, and
// 2) after the current CG is advanced at least once
- if (terminateCurrentExecution() && choiceCounter > 0) {
+ if (choiceCounter > 0 && terminateCurrentExecution()) {
exploreNextBacktrackPoints(vm, icsCG);
} else {
numOfTransitions++;
// 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(eventChoice, rwSet.getCopy());
- mainSummary.put(stateId, stateSummary);
- } else {
- stateSummary = mainSummary.get(stateId);
- if (!stateSummary.containsKey(eventChoice)) {
+ if (!rwSet.isEmpty()) {
+ HashMap<Integer, ReadWriteSet> stateSummary;
+ if (!mainSummary.containsKey(stateId)) {
+ stateSummary = new HashMap<>();
stateSummary.put(eventChoice, rwSet.getCopy());
+ mainSummary.put(stateId, stateSummary);
} else {
- rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
+ stateSummary = mainSummary.get(stateId);
+ if (!stateSummary.containsKey(eventChoice)) {
+ stateSummary.put(eventChoice, rwSet.getCopy());
+ } else {
+ rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
+ }
}
}
return rwSet;
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 the state summary of main summary
currRWSet = mainSummary.updateStateSummary(currTrans.getStateId(), conflictEventChoice, currRWSet);
return;
}
visited.add(currTrans);
+ // Halt if the set is empty
+ if (currRWSet.isEmpty()) {
+ return;
+ }
// Explore all predecessors
for (Predecessor predecessor : currTrans.getPredecessors()) {
// Get the predecessor (previous conflict choice)
// 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
- updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet, visited);
+ updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet.getCopy(), visited);
}
}
}