// 1) if we have seen this state or this state contains cycles that involve all events, and
// 2) after the current CG is advanced at least once
if (terminateCurrentExecution() && choiceCounter > 0) {
- saveExecutionInfo();
exploreNextBacktrackPoints(vm, icsCG);
} else {
numOfTransitions++;
// Check and record a backtrack set for just once!
if (isConflictFound(nextInsn, eventCounter, currentChoice, fieldClass) &&
isNewConflict(currentChoice, eventCounter)) {
- createBacktrackingPoint(currentChoice, eventCounter);
+ createBacktrackingPoint(currentChoice, eventCounter, false);
}
}
}
HashSet<Integer> eventSet = new HashSet<>();
stateToEventMap.put(stateId, eventSet);
}
+ // Save execution state into the map
+ if (!prevVisitedStates.contains(stateId)) {
+ ReachabilityGraph reachabilityGraph = new
+ ReachabilityGraph(backtrackPointList, readWriteFieldsMap);
+ stateToRGraph.put(stateId, reachabilityGraph);
+ }
stateToChoiceCounterMap.put(stateId, choiceCounter);
analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
justVisitedStates.add(stateId);
return currentChoice;
}
- private void createBacktrackingPoint(int currentChoice, int confEvtNum) {
+ private void createBacktrackingPoint(int currentChoice, int confEvtNum, boolean isPastTrace) {
// 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}
// for the original set {0, 1, 2, 3}
Integer[] newChoiceList = new Integer[refChoices.length];
// Put the conflicting event numbers first and reverse the order
- // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method
- newChoiceList[0] = backtrackPointList.get(currentChoice).getChoice();
+ if (isPastTrace) {
+ // For past trace we get the choice/event from the list
+ newChoiceList[0] = backtrackPointList.get(currentChoice).getChoice();
+ } else {
+ // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method
+ int actualCurrCho = currentChoice % refChoices.length;
+ newChoiceList[0] = choices[actualCurrCho];
+ }
newChoiceList[1] = backtrackPointList.get(confEvtNum).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++) {
return rwSet;
}
- private boolean isConflictFound(int eventCounter, int currentChoice) {
+ private boolean isConflictFound(int eventCounter, int currentChoice, boolean isPastTrace) {
+ int currActualChoice;
+ if (isPastTrace) {
+ currActualChoice = backtrackPointList.get(currentChoice).getChoice();
+ } else {
+ int actualCurrCho = currentChoice % refChoices.length;
+ currActualChoice = choices[actualCurrCho];
+ }
// Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
if (!readWriteFieldsMap.containsKey(eventCounter) ||
- backtrackPointList.get(currentChoice).getChoice() == backtrackPointList.get(eventCounter).getChoice()) {
+ currActualChoice == backtrackPointList.get(eventCounter).getChoice()) {
return false;
}
// Current R/W set
}
}
- // Save the information from this execution for future reachability analysis
- private void saveExecutionInfo() {
- Set<Integer> states = stateToChoiceCounterMap.keySet();
- ReachabilityGraph reachabilityGraph = new
- ReachabilityGraph(backtrackPointList, readWriteFieldsMap);
- // Map all the states visited in this execution to the same ReachabilityGraph object for fast access
- for(Integer state : states) {
- if (!prevVisitedStates.contains(state)) {
- stateToRGraph.put(state, reachabilityGraph);
+ // Get the start event for the past execution trace when there is a state matched from a past execution
+ private int getPastConflictChoice(int stateId, ArrayList<BacktrackPoint> pastBacktrackPointList) {
+ // Iterate and find the first occurrence of the state ID
+ // It is guaranteed that a choice should be found because the state ID is in the list
+ int pastConfChoice = 0;
+ for(int i = 0; i<pastBacktrackPointList.size(); i++) {
+ BacktrackPoint backtrackPoint = pastBacktrackPointList.get(i);
+ int stId = backtrackPoint.getStateId();
+ if (stId == stateId) {
+ pastConfChoice = i;
+ break;
}
}
+ return pastConfChoice;
}
+ // Save the information from this execution for future reachability analysis
+// private void saveExecutionInfo() {
+// Set<Integer> states = stateToChoiceCounterMap.keySet();
+// // Map all the states visited in this execution to the same ReachabilityGraph object for fast access
+// for(Integer state : states) {
+// if (!prevVisitedStates.contains(state)) {
+// ReachabilityGraph reachabilityGraph = new
+// ReachabilityGraph(backtrackPointList, readWriteFieldsMap);
+// stateToRGraph.put(state, reachabilityGraph);
+// }
+// }
+// }
+
// 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
// Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
while (conflictChoice < currentChoice) {
for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) {
- if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
- createBacktrackingPoint(conflictChoice, eventCounter);
+ if (isConflictFound(eventCounter, conflictChoice, false) && isNewConflict(conflictChoice, eventCounter)) {
+ createBacktrackingPoint(conflictChoice, eventCounter, false);
}
}
conflictChoice++;
}
}
- private int getPastConflictChoice(int stateId, ArrayList<BacktrackPoint> pastBacktrackPointList) {
- // Iterate and find the first occurrence of the state ID
- // It is guaranteed that a choice should be found because the state ID is in the list
- int pastConfChoice = 0;
- for(int i = 0; i<pastBacktrackPointList.size(); i++) {
- BacktrackPoint backtrackPoint = pastBacktrackPointList.get(i);
- int stId = backtrackPoint.getStateId();
- if (stId == stateId) {
- pastConfChoice = i;
- break;
- }
- }
- return pastConfChoice;
- }
-
// Update the backtrack sets in a previous execution
private void updateBacktrackSetsInPreviousExecution(int stateId) {
// Find the right ReachabilityGraph object that contains the stateId
backtrackPointList.add(confBtrackPoint);
readWriteFieldsMap.put(choiceCounter, rwSet);
for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) {
- if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
- createBacktrackingPoint(conflictChoice, eventCounter);
+ if (isConflictFound(eventCounter, conflictChoice, true) && isNewConflict(conflictChoice, eventCounter)) {
+ createBacktrackingPoint(conflictChoice, eventCounter, true);
}
}
// Remove this event to replace it with a new one
projects / jpf-core.git / commitdiff