From 9f89d20067acb0133c90727bb465670cdb67d442 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Thu, 7 May 2020 11:14:42 -0700 Subject: [PATCH] Fixing a bug: completing reachability graph with missing past traces. --- .../nasa/jpf/listener/DPORStateReducer.java | 134 ++++++++++++------ 1 file changed, 91 insertions(+), 43 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 37ae774..885add3 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -82,7 +82,7 @@ public class DPORStateReducer extends ListenerAdapter { private HashMap readWriteFieldsMap; // Record fields that are accessed private HashMap restorableStateMap; // Maps state IDs to the restorable state object private HashMap stateToChoiceCounterMap; // Maps state IDs to the choice counter - private HashMap stateToRGraph; // Maps state IDs to a ReachabilityGraph + private HashMap> rGraph; // Create a reachability graph // Boolean states private boolean isBooleanCGFlipped; @@ -387,11 +387,11 @@ public class DPORStateReducer extends ListenerAdapter { } // This class stores a compact representation of a reachability graph for past executions - private class ReachabilityGraph { + private class ReachableTrace { private ArrayList pastBacktrackPointList; private HashMap pastReadWriteFieldsMap; - public ReachabilityGraph(ArrayList btrackPointList, + public ReachableTrace(ArrayList btrackPointList, HashMap rwFieldsMap) { pastBacktrackPointList = btrackPointList; pastReadWriteFieldsMap = rwFieldsMap; @@ -497,7 +497,7 @@ public class DPORStateReducer extends ListenerAdapter { doneBacktrackSet = new HashSet<>(); readWriteFieldsMap = new HashMap<>(); stateToChoiceCounterMap = new HashMap<>(); - stateToRGraph = new HashMap<>(); + rGraph = new HashMap<>(); // Booleans isEndOfExecution = false; } @@ -532,11 +532,21 @@ public class DPORStateReducer extends ListenerAdapter { HashSet 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); + // Save execution state into the Reachability only if + // (1) It is not a revisited state from a past execution, or + // (2) It is just a new backtracking point + if (!prevVisitedStates.contains(stateId) || + choiceCounter <= 1) { + ReachableTrace reachableTrace= new + ReachableTrace(backtrackPointList, readWriteFieldsMap); + ArrayList rTrace; + if (!prevVisitedStates.contains(stateId)) { + rTrace = new ArrayList<>(); + rGraph.put(stateId, rTrace); + } else { + rTrace = rGraph.get(stateId); + } + rTrace.add(reachableTrace); } stateToChoiceCounterMap.put(stateId, choiceCounter); analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); @@ -928,18 +938,18 @@ public class DPORStateReducer extends ListenerAdapter { return pastConfChoice; } - // Save the information from this execution for future reachability analysis -// private void saveExecutionInfo() { -// Set 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); -// } -// } -// } + // Get a sorted list of reachable state IDs starting from the input stateId + private ArrayList getReachableStateIds(Set stateIds, int stateId) { + // Only include state IDs equal or greater than the input stateId: these are reachable states + ArrayList sortedStateIds = new ArrayList<>(); + for(Integer stId : stateIds) { + if (stId >= stateId) { + sortedStateIds.add(stId); + } + } + Collections.sort(sortedStateIds); + return sortedStateIds; + } // Update the backtrack sets in the cycle private void updateBacktrackSetsInCycle(int stateId) { @@ -957,32 +967,70 @@ 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; + } + } else { + choiceSet = new HashSet<>(); + checkedStateIdAndChoice.put(stateId, choiceSet); + } + choiceSet.add(choice); + + return true; + } + // Update the backtrack sets in a previous execution private void updateBacktrackSetsInPreviousExecution(int stateId) { - // Find the right ReachabilityGraph object that contains the stateId - ReachabilityGraph rGraph = stateToRGraph.get(stateId); - // Find the choice/event that marks the start of the subtrace from the previous execution - ArrayList pastBacktrackPointList = rGraph.getPastBacktrackPointList(); - HashMap pastReadWriteFieldsMap = rGraph.getPastReadWriteFieldsMap(); - int pastConfChoice = getPastConflictChoice(stateId, pastBacktrackPointList); - int conflictChoice = choiceCounter; - // Iterate from the starting point until the end of the past execution trace - while (pastConfChoice < pastBacktrackPointList.size() - 1) { // BacktrackPoint list always has a surplus of 1 - // Get the info of the event from the past execution trace - BacktrackPoint confBtrackPoint = pastBacktrackPointList.get(pastConfChoice); - ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice); - // Append this event to the current list and map - backtrackPointList.add(confBtrackPoint); - readWriteFieldsMap.put(choiceCounter, rwSet); - for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) { - if (isConflictFound(eventCounter, conflictChoice, true) && isNewConflict(conflictChoice, eventCounter)) { - createBacktrackingPoint(conflictChoice, eventCounter, true); + // 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<>(); + // Get sorted reachable state IDs + ArrayList reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId); + // Iterate from this state ID until the biggest state ID + for(Integer stId : reachableStateIds) { + // Find the right reachability graph object that contains the stateId + ArrayList rTraces = rGraph.get(stId); + for (ReachableTrace rTrace : rTraces) { + if (!checkedTrace.contains(rTrace)) { + // Find the choice/event that marks the start of the subtrace from the previous execution + ArrayList pastBacktrackPointList = rTrace.getPastBacktrackPointList(); + HashMap pastReadWriteFieldsMap = rTrace.getPastReadWriteFieldsMap(); + int pastConfChoice = getPastConflictChoice(stId, pastBacktrackPointList); + int conflictChoice = choiceCounter; + // Iterate from the starting point until the end of the past execution trace + while (pastConfChoice < pastBacktrackPointList.size() - 1) { // BacktrackPoint list always has a surplus of 1 + // Get the info of the event from the past execution trace + BacktrackPoint confBtrackPoint = pastBacktrackPointList.get(pastConfChoice); + if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) { + ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice); + // Append this event to the current list and map + backtrackPointList.add(confBtrackPoint); + readWriteFieldsMap.put(choiceCounter, rwSet); + for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) { + if (isConflictFound(eventCounter, conflictChoice, true) && isNewConflict(conflictChoice, eventCounter)) { + createBacktrackingPoint(conflictChoice, eventCounter, true); + } + } + // Remove this event to replace it with a new one + backtrackPointList.remove(backtrackPointList.size() - 1); + readWriteFieldsMap.remove(choiceCounter); + } + pastConfChoice++; + } + checkedTrace.add(rTrace); } } - // Remove this event to replace it with a new one - backtrackPointList.remove(backtrackPointList.size() - 1); - readWriteFieldsMap.remove(choiceCounter); - pastConfChoice++; } } } -- 2.34.1