From 9adeb9b41d1ca24612350f1b055af8d9e0f65e8b Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 1 May 2020 15:47:12 -0700 Subject: [PATCH] Adding reachability graph for past executions. --- .../nasa/jpf/listener/DPORStateReducer.java | 131 +++++++++++++++--- 1 file changed, 110 insertions(+), 21 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 6ba35e7..4645d2c 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -82,6 +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 // Boolean states private boolean isBooleanCGFlipped; @@ -251,6 +252,7 @@ public class DPORStateReducer extends ListenerAdapter { // 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++; @@ -385,6 +387,26 @@ public class DPORStateReducer extends ListenerAdapter { } } + // This class stores a compact representation of a reachability graph for past executions + private class ReachabilityGraph { + private ArrayList pastBacktrackPointList; + private HashMap pastReadWriteFieldsMap; + + public ReachabilityGraph(ArrayList btrackPointList, + HashMap rwFieldsMap) { + pastBacktrackPointList = btrackPointList; + pastReadWriteFieldsMap = rwFieldsMap; + } + + public ArrayList getPastBacktrackPointList() { + return pastBacktrackPointList; + } + + public HashMap getPastReadWriteFieldsMap() { + return pastReadWriteFieldsMap; + } + } + // -- CONSTANTS private final static String DO_CALL_METHOD = "doCall"; // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure @@ -476,6 +498,7 @@ public class DPORStateReducer extends ListenerAdapter { doneBacktrackSet = new HashSet<>(); readWriteFieldsMap = new HashMap<>(); stateToChoiceCounterMap = new HashMap<>(); + stateToRGraph = new HashMap<>(); // Booleans isEndOfExecution = false; } @@ -630,9 +653,8 @@ public class DPORStateReducer extends ListenerAdapter { // for the original set {0, 1, 2, 3} Integer[] newChoiceList = new Integer[refChoices.length]; // Put the conflicting event numbers first and reverse the order - int actualCurrCho = currentChoice % refChoices.length; // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method - newChoiceList[0] = choices[actualCurrCho]; + newChoiceList[0] = backtrackPointList.get(currentChoice).getChoice(); 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++) { @@ -722,10 +744,9 @@ public class DPORStateReducer extends ListenerAdapter { private boolean isConflictFound(int eventCounter, int currentChoice) { - int actualCurrCho = currentChoice % refChoices.length; // 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) || - choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) { + backtrackPointList.get(currentChoice).getChoice() == backtrackPointList.get(eventCounter).getChoice()) { return false; } // Current R/W set @@ -826,12 +847,13 @@ public class DPORStateReducer extends ListenerAdapter { choiceCounter = 0; choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); - // Clearing data structures - conflictPairMap.clear(); - readWriteFieldsMap.clear(); - stateToEventMap.clear(); + // Clear data structures + backtrackPointList = new ArrayList<>(); + conflictPairMap = new HashMap<>(); + readWriteFieldsMap = new HashMap<>(); + stateToChoiceCounterMap = new HashMap<>(); + stateToEventMap = new HashMap<>(); isEndOfExecution = false; - backtrackPointList.clear(); } } @@ -861,20 +883,87 @@ public class DPORStateReducer extends ListenerAdapter { // 3) at least 2 choices/events have been explored (choiceCounter > 1), // 4) the matched state has been encountered in the current execution, and // 5) state > 0 (state 0 is for boolean CG) - if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && - currVisitedStates.contains(stateId) && (stateId > 0)) { - // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts - int conflictChoice = stateToChoiceCounterMap.get(stateId); - int currentChoice = choiceCounter - 1; - // 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 (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && (stateId > 0)) { + 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 + // Update the backtrack sets in a previous execution + updateBacktrackSetsInPreviousExecution(stateId); + } + } + } + + // Save the information from this execution for future reachability analysis + private void saveExecutionInfo() { + Set 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); + } + } + } + + // 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 conflictChoice = stateToChoiceCounterMap.get(stateId); + int currentChoice = choiceCounter - 1; + // 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); + } + } + conflictChoice++; + } + } + + private int getPastConflictChoice(int stateId, ArrayList 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 = 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) && isNewConflict(conflictChoice, eventCounter)) { + createBacktrackingPoint(conflictChoice, eventCounter); } - conflictChoice++; } + // Remove this event to replace it with a new one + backtrackPointList.remove(backtrackPointList.size() - 1); + readWriteFieldsMap.remove(choiceCounter); + pastConfChoice++; } } } -- 2.34.1