stateToEventMap.put(stateId, eventSet);
}
saveExecutionToRGraph(stateId);
- stateToChoiceCounterMap.put(stateId, choiceCounter);
analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
+ stateToChoiceCounterMap.put(stateId, choiceCounter);
justVisitedStates.add(stateId);
currVisitedStates.add(stateId);
}
return currentChoice;
}
- private void createBacktrackingPoint(int currentChoice, int conflictChoice, Execution execution) {
+ private void createBacktrackingPoint(int backtrackChoice, int conflictChoice, Execution execution) {
// Create a new list of choices for backtrack based on the current choice and conflicting event number
// E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2}
//int firstChoice = choices[actualChoice];
ArrayList<BacktrackPoint> pastTrace = execution.getExecutionTrace();
ArrayList<BacktrackPoint> currTrace = currentExecution.getExecutionTrace();
- int backtrackEvent = currTrace.get(currentChoice).getChoice();
+ int btrackChoice = currTrace.get(backtrackChoice).getChoice();
int stateId = pastTrace.get(conflictChoice).getStateId();
// Check if this trace has been done from this state
- if (isTraceAlreadyConstructed(backtrackEvent, stateId)) {
+ if (isTraceAlreadyConstructed(btrackChoice, stateId)) {
return;
}
// Put the conflicting event numbers first and reverse the order
- newChoiceList[0] = backtrackEvent;
+ newChoiceList[0] = btrackChoice;
newChoiceList[1] = pastTrace.get(conflictChoice).getChoice();
// Put the rest of the event numbers into the array starting from the minimum to the upper bound
for (int i = 0, j = 2; i < refChoices.length; i++) {
}
// Save all the visited states when starting a new execution of trace
prevVisitedStates.addAll(currVisitedStates);
- currVisitedStates.clear();
// This marks a transitional period to the new CG
isEndOfExecution = true;
}
return false;
}
- private boolean isConflictFound(int currentChoice, int reachableEvent, Execution execution) {
+ private boolean isConflictFound(int reachableChoice, int conflictChoice, Execution execution) {
ArrayList<BacktrackPoint> executionTrace = execution.getExecutionTrace();
HashMap<Integer, ReadWriteSet> execRWFieldsMap = execution.getReadWriteFieldsMap();
// Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
- if (!execRWFieldsMap.containsKey(reachableEvent) ||
- executionTrace.get(currentChoice).getChoice() == executionTrace.get(reachableEvent).getChoice()) {
+ if (!execRWFieldsMap.containsKey(conflictChoice) ||
+ executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) {
return false;
}
// Current R/W set
- ReadWriteSet currRWSet = execRWFieldsMap.get(currentChoice);
+ ReadWriteSet currRWSet = execRWFieldsMap.get(reachableChoice);
// R/W set of choice/event that may have a potential conflict
- ReadWriteSet evtRWSet = execRWFieldsMap.get(reachableEvent);
+ ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice);
// Check for conflicts with Read and Write fields for Write instructions
Set<String> currWriteSet = currRWSet.getWriteSet();
for(String writeField : currWriteSet) {
choices = icsCG.getAllChoices();
refChoices = copyChoices(choices);
// Clear data structures
+ currVisitedStates = new HashSet<>();
stateToChoiceCounterMap = new HashMap<>();
stateToEventMap = new HashMap<>();
isEndOfExecution = false;
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
+ } /* else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
// Update the backtrack sets in a previous execution
updateBacktrackSetsInPreviousExecution(stateId);
- }
+ }*/
}
}
// Update the backtrack sets in the cycle
private void updateBacktrackSetsInCycle(int stateId) {
// Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
- int currentChoice = stateToChoiceCounterMap.get(stateId);
+ int reachableChoice = stateToChoiceCounterMap.get(stateId);
int cycleEndChoice = choiceCounter - 1;
// Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
- while (currentChoice < cycleEndChoice) {
- for (int reachableEvent = currentChoice + 1; reachableEvent <= cycleEndChoice; reachableEvent++) {
- if (isConflictFound(currentChoice, reachableEvent, currentExecution)) {
- createBacktrackingPoint(currentChoice, reachableEvent, currentExecution);
+ while (reachableChoice < cycleEndChoice) {
+ for (int conflictChoice = reachableChoice + 1; conflictChoice <= cycleEndChoice; conflictChoice++) {
+ if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) {
+ createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution);
}
}
- currentChoice++;
+ reachableChoice++;
}
}