private int hiStateId; // Maximum state Id
private HashMap<Integer, HashSet<TransitionEvent>> graph; // Reachable transitions from past executions
// TODO: THIS IS THE ACCESS SUMMARY
- private HashMap<Integer, HashMap<Integer, ReadWriteSet>> graphSummary;
- private HashMap<Integer, HashMap<Integer, TransitionEvent>> eventSummary;
+ private HashMap<Integer, HashMap<Integer, SummaryNode>> graphSummary;
public RGraph() {
hiStateId = 0;
graph = new HashMap<>();
graphSummary = new HashMap<>();
- eventSummary = new HashMap<>();
}
public void addReachableTransition(int stateId, TransitionEvent transition) {
return reachableTransitions;
}
- public HashMap<Integer, TransitionEvent> getReachableSummaryTransitions(int stateId) {
- return eventSummary.get(stateId);
- }
-
- public HashMap<Integer, ReadWriteSet> getReachableSummaryRWSets(int stateId) {
+ public HashMap<Integer, SummaryNode> getReachableTransitionsSummary(int stateId) {
return graphSummary.get(stateId);
}
public ReadWriteSet recordTransitionSummary(int stateId, TransitionEvent transition, ReadWriteSet rwSet) {
// Record transition into graphSummary
// TransitionMap maps event (choice) number to a R/W set
- HashMap<Integer, ReadWriteSet> transitionMap;
+ HashMap<Integer, SummaryNode> transitionSummary;
if (graphSummary.containsKey(stateId)) {
- transitionMap = graphSummary.get(stateId);
+ transitionSummary = graphSummary.get(stateId);
} else {
- transitionMap = new HashMap<>();
- graphSummary.put(stateId, transitionMap);
+ transitionSummary = new HashMap<>();
+ graphSummary.put(stateId, transitionSummary);
}
int choice = transition.getChoice();
- ReadWriteSet recordedRWSet;
+ SummaryNode summaryNode;
// Insert transition into the map if we haven't had this event number recorded
- if (!transitionMap.containsKey(choice)) {
- recordedRWSet = rwSet.getCopy();
- transitionMap.put(choice, recordedRWSet);
- // Insert the actual TransitionEvent object into the map
- HashMap<Integer, TransitionEvent> eventMap = new HashMap<>();
- eventMap.put(choice, transition);
- eventSummary.put(stateId, eventMap);
+ if (!transitionSummary.containsKey(choice)) {
+ summaryNode = new SummaryNode(transition, rwSet.getCopy());
+ transitionSummary.put(choice, summaryNode);
} else {
- recordedRWSet = transitionMap.get(choice);
+ summaryNode = transitionSummary.get(choice);
// Perform union and subtraction between the recorded and the given R/W sets
- rwSet = performUnion(recordedRWSet, rwSet);
+ rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet);
}
return rwSet;
}
}
}
+ // This class provides a data structure to store TransitionEvent and ReadWriteSet for a summary
+ private class SummaryNode {
+ private TransitionEvent transitionEvent;
+ private ReadWriteSet readWriteSet;
+
+ public SummaryNode(TransitionEvent transEvent, ReadWriteSet rwSet) {
+ transitionEvent = transEvent;
+ readWriteSet = rwSet;
+ }
+
+ public TransitionEvent getTransitionEvent() {
+ return transitionEvent;
+ }
+
+ public ReadWriteSet getReadWriteSet() {
+ return readWriteSet;
+ }
+ }
+
// This class compactly stores transitions:
// 1) CG,
// 2) state ID,
private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
Execution conflictExecution, int conflictChoice,
ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
+ TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
+ // TODO: THIS IS THE ACCESS SUMMARY
+ // Record this transition into rGraph summary
+ currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), currTrans, currRWSet);
// Halt when we have found the first read/write conflicts for all memory locations
if (currRWSet.isEmpty()) {
return;
}
- TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
- // Halt when we have visited this transition (in a cycle)
if (visited.contains(currTrans)) {
return;
}
newConflictChoice = conflictChoice;
newConflictExecution = conflictExecution;
}
- // TODO: THIS IS THE ACCESS SUMMARY
- // Record this transition into rGraph summary
- int stateId = predecessor.getExecution().getExecutionTrace().get(predecessorChoice).getStateId();
- currRWSet = rGraph.recordTransitionSummary(stateId, currTrans, currRWSet);
// Continue performing DFS if conflict is not found
updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
currRWSet, visited);
private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) {
// Collect all the reachable transitions from R-Graph
- HashMap<Integer, TransitionEvent> reachableTransitions = rGraph.getReachableSummaryTransitions(stateId);
- HashMap<Integer, ReadWriteSet> reachableRWSets = rGraph.getReachableSummaryRWSets(stateId);
- for(Map.Entry<Integer, TransitionEvent> transition : reachableTransitions.entrySet()) {
- TransitionEvent reachableTransition = transition.getValue();
+ HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionsSummary(stateId);
+ for(Map.Entry<Integer, SummaryNode> transition : reachableTransitions.entrySet()) {
+ TransitionEvent reachableTransition = transition.getValue().getTransitionEvent();
Execution conflictExecution = reachableTransition.getExecution();
int conflictChoice = reachableTransition.getChoiceCounter();
// Copy ReadWriteSet object
- ReadWriteSet currRWSet = reachableRWSets.get(transition.getKey());
+ ReadWriteSet currRWSet = transition.getValue().getReadWriteSet();
currRWSet = currRWSet.getCopy();
// Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
HashSet<TransitionEvent> visited = new HashSet<>();