transition = new TransitionEvent();
currentExecution.addTransition(transition);
transition.recordPredecessor(currentExecution, choiceCounter - 1);
+ // We have to check if there is a transition whose source state ID is the same
+ // If such exists, then we need to add its predecessors to the predecessor set of the current transition
+ for (TransitionEvent trans : rGraph.getReachableTransitionsAtState(stateId)) {
+ for (Predecessor pred : trans.getPredecessors()) {
+ transition.recordPredecessor(pred.getExecution(), pred.getChoice());
+ }
+ }
}
transition.setExecution(currentExecution);
transition.setTransitionCG(icsCG);
int newConflictChoice = conflictChoice;
Execution newConflictExecution = conflictExecution;
// Check if a conflict is found
- if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
+ ReadWriteSet newCurrRWSet = currRWSet.getCopy();
+ if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) {
createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
newConflictChoice = predecessorChoice;
newConflictExecution = predecessorExecution;
}
// Continue performing DFS if conflict is not found
updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
- currRWSet, visited);
+ newCurrRWSet, visited);
}
}
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
if (stateReductionMode) {
if (!isEndOfExecution) {
- // Has to be initialized and a integer CG
+ // Has to be initialized and it is a integer CG
ChoiceGenerator<?> cg = vm.getChoiceGenerator();
if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
int currentChoice = choiceCounter - 1; // Accumulative choice w.r.t the current trace
public Set<Integer> getEventChoicesAtStateId(int stateId) {
HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
- return stateSummary.keySet();
+ // Return a new set since this might get updated concurrently
+ return new HashSet<>(stateSummary.keySet());
}
public ReadWriteSet getRWSetForEventChoiceAtState(int eventChoice, int stateId) {
return stateSummary.get(eventChoice);
}
+ public Set<Integer> getStateIds() {
+ return mainSummary.keySet();
+ }
+
private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
// Combine the same write accesses and record in the recordedRWSet
HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
transition = new TransitionEvent();
currentExecution.addTransition(transition);
transition.recordPredecessor(currentExecution, choiceCounter - 1);
+ // We have to check if there is a transition whose source state ID is the same
+ // If such exists, then we need to add its predecessors to the predecessor set of the current transition
+ for (TransitionEvent trans : rGraph.getReachableTransitionsAtState(stateId)) {
+ for (Predecessor pred : trans.getPredecessors()) {
+ transition.recordPredecessor(pred.getExecution(), pred.getChoice());
+ }
+ }
}
transition.setExecution(currentExecution);
transition.setTransitionCG(icsCG);
// We need to check all the states that have just been visited
// Often a transition (choice/event) can result into forwarding/backtracking to a number of states
boolean terminate = false;
+ Set<Integer> mainStateIds = mainSummary.getStateIds();
for(Integer stateId : justVisitedStates) {
- // We perform updates on backtrack sets for every
- if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
- updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
- terminate = true;
- }
- // If frequency > 1 then this means we have visited this stateId more than once
- if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
- updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+ // We exclude states that are produced by other CGs that are not integer CG
+ // When we encounter these states, then we should also encounter the corresponding integer CG state ID
+ if (mainStateIds.contains(stateId)) {
+ // We perform updates on backtrack sets for every
+ if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
+ updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+ terminate = true;
+ }
+ // If frequency > 1 then this means we have visited this stateId more than once
+ if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
+ updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+ }
}
}
return terminate;
return;
}
visited.add(currTrans);
- // Halt if the set is empty
- if (currRWSet.isEmpty()) {
- return;
- }
- // Explore all predecessors
- for (Predecessor predecessor : currTrans.getPredecessors()) {
- // Get the predecessor (previous conflict choice)
- int predecessorChoice = predecessor.getChoice();
- Execution predecessorExecution = predecessor.getExecution();
- // Push up one happens-before transition
- int newConflictEventChoice = conflictEventChoice;
- // Check if a conflict is found
- if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, currRWSet)) {
- createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
- // We need to extract the pushed happens-before event choice from the predecessor execution and choice
- newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+ // Check the predecessors only if the set is not empty
+ if (!currRWSet.isEmpty()) {
+ // Explore all predecessors
+ for (Predecessor predecessor : currTrans.getPredecessors()) {
+ // Get the predecessor (previous conflict choice)
+ int predecessorChoice = predecessor.getChoice();
+ Execution predecessorExecution = predecessor.getExecution();
+ // Push up one happens-before transition
+ int newConflictEventChoice = conflictEventChoice;
+ // Check if a conflict is found
+ ReadWriteSet newCurrRWSet = currRWSet.getCopy();
+ if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) {
+ createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
+ // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+ newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+ }
+ // Continue performing DFS if conflict is not found
+ updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
+ newCurrRWSet, visited);
}
- // Continue performing DFS if conflict is not found
- updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
- currRWSet, visited);
}
}