From c4889f13b870dd32124a09d1b840cb3ce4f66a99 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 15 May 2020 16:27:23 -0700 Subject: [PATCH 1/1] Tested updating backtrack sets in the reachability graph. --- .../nasa/jpf/listener/DPORStateReducer.java | 100 +++++++++--------- 1 file changed, 50 insertions(+), 50 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 37353f3..f4b5923 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -980,6 +980,23 @@ public class DPORStateReducer extends ListenerAdapter { // --- 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 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 @@ -995,10 +1012,10 @@ public class DPORStateReducer extends ListenerAdapter { 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); - }*/ + updateBacktrackSetsInPreviousExecutions(stateId); + } } } @@ -1047,34 +1064,43 @@ public class DPORStateReducer extends ListenerAdapter { } } - // TODO: OPTIMIZATION! - // Check and make sure that state ID and choice haven't been explored for this trace - private boolean isNotChecked(HashMap> checkedStateIdAndChoice, - BacktrackPoint backtrackPoint) { - int stateId = backtrackPoint.getStateId(); - int choice = backtrackPoint.getChoice(); - HashSet 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 checkedStateIdAndChoice) { + // Find the choice/event that marks the start of the subtrace from the previous execution + ArrayList pastExecutionTrace = rExecution.getExecutionTrace(); + HashMap 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 currentTrace = currentExecution.getExecutionTrace(); + HashMap 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 checkedTrace = new HashSet<>(); // Don't check the same event twice for a revisited state - HashMap> checkedStateIdAndChoice = new HashMap<>(); + HashSet checkedStateIdAndChoice = new HashSet<>(); // Get sorted reachable state IDs ArrayList reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId); // Iterate from this state ID until the biggest state ID @@ -1083,33 +1109,7 @@ public class DPORStateReducer extends ListenerAdapter { ArrayList 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 pastExecutionTrace = rExecution.getExecutionTrace(); - HashMap 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 currentTrace = currentExecution.getExecutionTrace(); - HashMap 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); } } -- 2.34.1