}
}
- public ReadWriteSet recordTransitionSummary(TransitionEvent transition, ReadWriteSet rwSet) {
+ public ReadWriteSet recordTransitionSummary(TransitionEvent transition, ReadWriteSet rwSet, boolean refresh) {
// Record transition into reachability summary
// TransitionMap maps event (choice) number to a R/W set
int choice = transition.getChoice();
SummaryNode summaryNode;
// Insert transition into the map if we haven't had this event number recorded
- if (!transitionSummary.containsKey(choice)) {
+ if (!transitionSummary.containsKey(choice) || refresh) {
summaryNode = new SummaryNode(transition, rwSet.getCopy());
transitionSummary.put(choice, summaryNode);
} else {
// Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
HashSet<TransitionEvent> visited = new HashSet<>();
// Update backtrack set recursively
- updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
+ updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited, false);
}
// Recursive method to perform backward DFS to traverse the graph
private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
Execution conflictExecution, int conflictChoice,
- ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
+ ReadWriteSet currRWSet, HashSet<TransitionEvent> visited,
+ boolean refresh) {
TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
if (visited.contains(currTrans)) {
return;
visited.add(currTrans);
TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
// Record this transition into rGraph summary
- currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet);
+ currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet, refresh);
// Halt when we have found the first read/write conflicts for all memory locations
if (currRWSet.isEmpty()) {
return;
}
// Continue performing DFS if conflict is not found
updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
- currRWSet, visited);
+ currRWSet, visited, refresh);
}
- // 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) {
// Perform this analysis only when:
// 1) this is not during a switch to a new execution,
currRWSet = currRWSet.getCopy();
// Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
HashSet<TransitionEvent> visited = new HashSet<>();
- updateBacktrackSetRecursive(currentExecution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
+ updateBacktrackSetRecursive(currentExecution, currentChoice, conflictExecution,
+ conflictChoice, currRWSet, visited, true);
}
}
}