private class RGraph {
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, SummaryNode>> graphSummary;
public RGraph() {
hiStateId = 0;
graph = new HashMap<>();
- graphSummary = new HashMap<>();
}
public void addReachableTransition(int stateId, TransitionEvent transition) {
}
return graph.get(stateId);
}
-
-// public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
-// HashSet<TransitionEvent> reachableTransitions = new HashSet<>();
-// // All transitions from states higher than the given state ID (until the highest state ID) are reachable
-// for(int stId = stateId; stId <= hiStateId; stId++) {
-// // We might encounter state IDs from the first round of Boolean CG
-// // The second round of Boolean CG should consider these new states
-// if (graph.containsKey(stId)) {
-// reachableTransitions.addAll(graph.get(stId));
-// }
-// }
-// return reachableTransitions;
-// }
-
- public HashMap<Integer, SummaryNode> getReachableTransitionSummary(int stateId) {
- // Just return an empty map if the state ID is not recorded yet
- // This means that there is no reachable transition from this state
- if (!graphSummary.containsKey(stateId)) {
- return new HashMap<>();
- }
- return graphSummary.get(stateId);
- }
-
-// private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
-// // Combine the same write accesses and record in the recordedRWSet
-// HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
-// HashMap<String, Integer> writeMap = rwSet.getWriteMap();
-// for(Map.Entry<String, Integer> entry : recordedWriteMap.entrySet()) {
-// String writeField = entry.getKey();
-// // Remove the entry from rwSet if both field and object ID are the same
-// if (writeMap.containsKey(writeField) &&
-// (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
-// writeMap.remove(writeField);
-// }
-// }
-// // Then add everything 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();
-// HashMap<String, Integer> readMap = rwSet.getReadMap();
-// for(Map.Entry<String, Integer> entry : recordedReadMap.entrySet()) {
-// String readField = entry.getKey();
-// // Remove the entry from rwSet if both field and object ID are the same
-// if (readMap.containsKey(readField) &&
-// (readMap.get(readField) == recordedReadMap.get(readField))) {
-// readMap.remove(readField);
-// }
-// }
-// // Then add everything into the recorded map because these will be traversed
-// recordedReadMap.putAll(readMap);
-//
-// return rwSet;
-// }
-
-// 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, SummaryNode> transitionSummary;
-// if (graphSummary.containsKey(stateId)) {
-// transitionSummary = graphSummary.get(stateId);
-// } else {
-// transitionSummary = new HashMap<>();
-// graphSummary.put(stateId, transitionSummary);
-// }
-// int choice = transition.getChoice();
-// SummaryNode summaryNode;
-// // Insert transition into the map if we haven't had this event number recorded
-// if (!transitionSummary.containsKey(choice)) {
-// summaryNode = new SummaryNode(transition, rwSet.getCopy());
-// transitionSummary.put(choice, summaryNode);
-// } else {
-// summaryNode = transitionSummary.get(choice);
-// // Perform union and subtraction between the recorded and the given R/W sets
-// rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet);
-// }
-// return rwSet;
-// }
-
- public void recordTransitionSummaryAtState(int stateId, HashMap<Integer, SummaryNode> transitionSummary) {
- // Record transition summary into graphSummary
- graphSummary.put(stateId, transitionSummary);
- }
}
// This class compactly stores Read and Write field sets
private int choiceCounter; // Choice counter at this transition
private Execution execution; // The execution where this transition belongs
private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
- // TODO: THIS IS THE ACCESS SUMMARY
private HashMap<Integer, SummaryNode> transitionSummary;
// Summary of pushed transitions at the current transition
private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
String writeField = entry.getKey();
// Remove the entry from rwSet if both field and object ID are the same
if (writeMap.containsKey(writeField) &&
- (writeMap.get(writeField) == recordedWriteMap.get(writeField))) {
+ (writeMap.get(writeField).equals(recordedWriteMap.get(writeField)))) {
writeMap.remove(writeField);
}
}
String readField = entry.getKey();
// Remove the entry from rwSet if both field and object ID are the same
if (readMap.containsKey(readField) &&
- (readMap.get(readField) == recordedReadMap.get(readField))) {
+ (readMap.get(readField).equals(recordedReadMap.get(readField)))) {
readMap.remove(readField);
}
}
}
}
- 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
- // TODO: The following is the call to the original version of the method
-// updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
- // TODO: The following is the call to the version of the method with pushing up happens-before transitions
- updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited);
+ updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited, false);
}
-// TODO: This is the original version of the recursive method
-// private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
-// Execution conflictExecution, int conflictChoice,
-// ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
-// // Halt when we have found the first read/write conflicts for all memory locations
-// if (currRWSet.isEmpty()) {
-// return;
-// }
-// TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
-// // Halt when we have visited this transition (in a cycle)
-// if (visited.contains(confTrans)) {
-// return;
-// }
-// visited.add(confTrans);
-// // Explore all predecessors
-// for (Predecessor predecessor : confTrans.getPredecessors()) {
-// // Get the predecessor (previous conflict choice)
-// conflictChoice = predecessor.getChoice();
-// conflictExecution = predecessor.getExecution();
-// // Check if a conflict is found
-// if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
-// createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice);
-// }
-// // Continue performing DFS if conflict is not found
-// updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
-// }
-// }
-
- // TODO: This is the version of the method with pushing up happens-before transitions
+ // 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);
- // TODO: THIS IS THE ACCESS SUMMARY
+ if (visited.contains(currTrans)) {
+ return;
+ }
+ visited.add(currTrans);
TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice);
// Record this transition into rGraph summary
- //currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), confTrans, currRWSet);
- currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet);
- rGraph.recordTransitionSummaryAtState(currTrans.getStateId(), currTrans.getTransitionSummary());
+ currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet, refresh);
// Halt when we have found the first read/write conflicts for all memory locations
if (currRWSet.isEmpty()) {
return;
}
- if (visited.contains(currTrans)) {
- return;
- }
- visited.add(currTrans);
// Explore all predecessors
for (Predecessor predecessor : currTrans.getPredecessors()) {
// Get the predecessor (previous conflict choice)
// Check if a conflict is found
if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
- newConflictChoice = conflictChoice;
- newConflictExecution = conflictExecution;
+ newConflictChoice = predecessorChoice;
+ newConflictExecution = predecessorExecution;
}
// 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) {
+ private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, 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 updateBacktrackSetsFromPreviousExecution(int stateId) {
// Collect all the reachable transitions from R-Graph
- HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitions(stateId);
+ HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
for(TransitionEvent transition : reachableTransitions) {
- Execution execution = transition.getExecution();
+ // Current transition that stems from this state ID
+ Execution currentExecution = transition.getExecution();
int currentChoice = transition.getChoiceCounter();
- updateBacktrackSet(execution, currentChoice);
- }
- }*/
-
- // TODO: THIS IS THE ACCESS SUMMARY
- private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, 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),
- // 3) state > 0 (state 0 is for boolean CG)
- if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
- if (currVisitedStates.contains(stateId) || prevVisitedStates.contains(stateId)) {
- // Update reachable transitions in the graph with a predecessor
- HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
- for(TransitionEvent transition : reachableTransitions) {
- transition.recordPredecessor(currentExecution, choiceCounter - 1);
- }
- updateBacktrackSetsFromPreviousExecution(currentExecution, choiceCounter - 1, stateId);
+ // Iterate over the stored conflict transitions in the summary
+ for(Map.Entry<Integer, SummaryNode> conflictTransition : transition.getTransitionSummary().entrySet()) {
+ SummaryNode summaryNode = conflictTransition.getValue();
+ // Conflict transition in the summary node
+ TransitionEvent confTrans = summaryNode.getTransitionEvent();
+ Execution conflictExecution = confTrans.getExecution();
+ int conflictChoice = confTrans.getChoiceCounter();
+ // Copy ReadWriteSet object
+ ReadWriteSet currRWSet = summaryNode.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<>();
+ updateBacktrackSetRecursive(currentExecution, currentChoice, conflictExecution,
+ conflictChoice, currRWSet, visited, true);
}
}
}
-
- private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) {
- // Collect all the reachable transitions from R-Graph
- HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionSummary(stateId);
- for(Map.Entry<Integer, SummaryNode> transition : reachableTransitions.entrySet()) {
- SummaryNode summaryNode = transition.getValue();
- TransitionEvent reachableTransition = summaryNode.getTransitionEvent();
- Execution conflictExecution = reachableTransition.getExecution();
- int conflictChoice = reachableTransition.getChoiceCounter();
- // Copy ReadWriteSet object
- ReadWriteSet currRWSet = summaryNode.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<>();
- updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
- }
- }
}