- // We use backtrackPointsList to analyze the reachable states/events when there is a state match:
- // 1) Whenever there is state match, there is a cycle of events
- // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
- // 3) Then we create a new backtrack point for every new conflict
- private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
- // Perform this analysis only when:
- // 1) there is a state match,
- // 2) this is not during a switch to a new execution,
- // 3) at least 2 choices/events have been explored (choiceCounter > 1),
- // 4) the matched state has been encountered in the current execution, and
- // 5) state > 0 (state 0 is for boolean CG)
- if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && (stateId > 0)) {
- if (currVisitedStates.contains(stateId)) {
- // Update the backtrack sets in the cycle
- updateBacktrackSetsInCycle(stateId);
- } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
- // Update the backtrack sets in a previous execution
- updateBacktrackSetsInPreviousExecutions(stateId);
- }
+// 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;