+ // Update backtrack sets
+ // 1) recursively, and
+ // 2) track accesses per memory location (per shared variable/field)
+ private void updateBacktrackSet(Execution execution, int currentChoice) {
+ // Copy ReadWriteSet object
+ HashMap<Integer, ReadWriteSet> currRWFieldsMap = execution.getReadWriteFieldsMap();
+ ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice);
+ if (currRWSet == null) {
+ return;
+ }
+ currRWSet = currRWSet.getCopy();
+ // 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, execution, currentChoice, currRWSet, visited);
+ }
+
+// 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
+ private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
+ Execution conflictExecution, int conflictChoice,
+ Execution hbExecution, int hbChoice,
+ 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();
+ // Push up one happens-before transition
+ int pushedChoice = hbChoice;
+ Execution pushedExecution = hbExecution;
+ // Check if a conflict is found
+ if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) {
+ createBacktrackingPoint(pushedExecution, pushedChoice, conflictExecution, conflictChoice);
+ pushedChoice = conflictChoice;
+ pushedExecution = conflictExecution;
+ }
+ // Continue performing DFS if conflict is not found
+ updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice,
+ pushedExecution, pushedChoice, currRWSet, visited);
+ }
+ // Remove the transition after being explored
+ visited.remove(confTrans);
+ }
+