- // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper
-
- // This method checks whether a choice is reachable in the VOD graph from a reference choice (BFS algorithm)
- //private boolean isReachableInVODGraph(int checkedChoice, int referenceChoice) {
- private boolean isReachableInVODGraph(int currentChoice) {
- // Extract previous and current events
- int choiceIndex = currentChoice % refChoices.length;
- int prevChoIndex = (currentChoice - 1) % refChoices.length;
- int currEvent = refChoices[choiceIndex];
- int prevEvent = refChoices[prevChoIndex];
- // Record visited choices as we search in the graph
- HashSet<Integer> visitedChoice = new HashSet<>();
- visitedChoice.add(prevEvent);
- LinkedList<Integer> nodesToVisit = new LinkedList<>();
- // If the state doesn't advance as the threads/sub-programs are executed (basically there is no new state),
- // there is a chance that the graph doesn't have new nodes---thus this check will return a null.
- if (vodGraphMap.containsKey(prevEvent)) {
- nodesToVisit.addAll(vodGraphMap.get(prevEvent));
- while(!nodesToVisit.isEmpty()) {
- int choice = nodesToVisit.getFirst();
- if (choice == currEvent) {
- return true;
- }
- if (visitedChoice.contains(choice)) { // If there is a loop then just continue the exploration
- continue;
- }
- // Continue searching
- visitedChoice.add(choice);
- HashSet<Integer> choiceNextNodes = vodGraphMap.get(choice);
- if (choiceNextNodes != null) {
- // Add only if there is a mapping for next nodes
- for (Integer nextNode : choiceNextNodes) {
- // Skip cycles
- if (nextNode == choice) {
- continue;
- }
- nodesToVisit.addLast(nextNode);
- }
+ // 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);
+ }
+
+ // --- 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,
+ // 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);