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;
// --- Functions related to the reachability analysis when there is a state match
+ // TODO: OPTIMIZATION!
+ // Check and make sure that state ID and choice haven't been explored for this trace
+ private boolean alreadyChecked(HashSet<String> checkedStateIdAndChoice, BacktrackPoint backtrackPoint) {
+ int stateId = backtrackPoint.getStateId();
+ int choice = backtrackPoint.getChoice();
+ StringBuilder sb = new StringBuilder();
+ sb.append(stateId);
+ sb.append(':');
+ sb.append(choice);
+ // Check if the trace has been constructed as a backtrack point for this state
+ if (checkedStateIdAndChoice.contains(sb.toString())) {
+ return true;
+ }
+ checkedStateIdAndChoice.add(sb.toString());
+ return false;
+ }
+
// 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
updateBacktrackSetsInCycle(stateId);
} else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution
// Update the backtrack sets in a previous execution
- updateBacktrackSetsInPreviousExecution(stateId);
+ updateBacktrackSetsInPreviousExecutions(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++;
}
}
- // TODO: OPTIMIZATION!
- // Check and make sure that state ID and choice haven't been explored for this trace
- private boolean isNotChecked(HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice,
- BacktrackPoint backtrackPoint) {
- int stateId = backtrackPoint.getStateId();
- int choice = backtrackPoint.getChoice();
- HashSet<Integer> choiceSet;
- if (checkedStateIdAndChoice.containsKey(stateId)) {
- choiceSet = checkedStateIdAndChoice.get(stateId);
- if (choiceSet.contains(choice)) {
- // State ID and choice found. It has been checked!
- return false;
+ private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId,
+ HashSet<String> checkedStateIdAndChoice) {
+ // Find the choice/event that marks the start of the subtrace from the previous execution
+ ArrayList<BacktrackPoint> pastExecutionTrace = rExecution.getExecutionTrace();
+ HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap();
+ int pastConfChoice = getPastConflictChoice(stateId, pastExecutionTrace);
+ int reachableChoice = choiceCounter;
+ // Iterate from the starting point until the end of the past execution trace
+ while (pastConfChoice < pastExecutionTrace.size() - 1) { // BacktrackPoint list always has a surplus of 1
+ // Get the info of the event from the past execution trace
+ BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);
+ if (!alreadyChecked(checkedStateIdAndChoice, confBtrackPoint)) {
+ ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
+ // Append this event to the current list and map
+ ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
+ HashMap<Integer, ReadWriteSet> currRWFieldsMap = currentExecution.getReadWriteFieldsMap();
+ currentTrace.add(confBtrackPoint);
+ currRWFieldsMap.put(choiceCounter, rwSet);
+ for (int conflictChoice = reachableChoice - 1; conflictChoice >= 0; conflictChoice--) {
+ if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) {
+ createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution);
+ }
+ }
+ // Remove this event to replace it with a new one
+ currentTrace.remove(currentTrace.size() - 1);
+ currRWFieldsMap.remove(choiceCounter);
}
- } else {
- choiceSet = new HashSet<>();
- checkedStateIdAndChoice.put(stateId, choiceSet);
+ pastConfChoice++;
}
- choiceSet.add(choice);
-
- return true;
}
// Update the backtrack sets in a previous execution
- private void updateBacktrackSetsInPreviousExecution(int stateId) {
+ private void updateBacktrackSetsInPreviousExecutions(int stateId) {
// Don't check a past trace twice!
HashSet<Execution> checkedTrace = new HashSet<>();
// Don't check the same event twice for a revisited state
- HashMap<Integer, HashSet<Integer>> checkedStateIdAndChoice = new HashMap<>();
+ HashSet<String> checkedStateIdAndChoice = new HashSet<>();
// Get sorted reachable state IDs
ArrayList<Integer> reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId);
// Iterate from this state ID until the biggest state ID
ArrayList<Execution> rExecutions = rGraph.get(stId);
for (Execution rExecution : rExecutions) {
if (!checkedTrace.contains(rExecution)) {
- // Find the choice/event that marks the start of the subtrace from the previous execution
- ArrayList<BacktrackPoint> pastExecutionTrace = rExecution.getExecutionTrace();
- HashMap<Integer, ReadWriteSet> pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap();
- int pastConfChoice = getPastConflictChoice(stId, pastExecutionTrace);
- int conflictChoice = choiceCounter;
- // Iterate from the starting point until the end of the past execution trace
- while (pastConfChoice < pastExecutionTrace.size() - 1) { // BacktrackPoint list always has a surplus of 1
- // Get the info of the event from the past execution trace
- BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice);
- if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) {
- ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice);
- // Append this event to the current list and map
- ArrayList<BacktrackPoint> currentTrace = currentExecution.getExecutionTrace();
- HashMap<Integer, ReadWriteSet> currRWFieldsMap = currentExecution.getReadWriteFieldsMap();
- currentTrace.add(confBtrackPoint);
- currRWFieldsMap.put(choiceCounter, rwSet);
- for (int pastChoice = conflictChoice - 1; pastChoice >= 0; pastChoice--) {
- if (isConflictFound(conflictChoice, pastChoice, rExecution)) {
- createBacktrackingPoint(conflictChoice, pastChoice, rExecution);
- }
- }
- // Remove this event to replace it with a new one
- currentTrace.remove(currentTrace.size() - 1);
- currRWFieldsMap.remove(choiceCounter);
- }
- pastConfChoice++;
- }
+ updateBacktrackSetsInPreviousExecution(rExecution, stateId, checkedStateIdAndChoice);
checkedTrace.add(rExecution);
}
}
projects / jpf-core.git / blobdiff