From: rtrimana Date: Mon, 6 Apr 2020 23:31:08 +0000 (-0700) Subject: Cleaning up and fixing bugs; new DPOR implementation seems to be correct; need to... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=b1c560c27cc9169acd9ad874b09df56eea7187a9;ds=sidebyside Cleaning up and fixing bugs; new DPOR implementation seems to be correct; need to test with other pairs. --- diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 362da3b..72fc44e 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -62,6 +62,7 @@ public class DPORStateReducer extends ListenerAdapter { private Integer[] choices; private Integer[] refChoices; private int choiceCounter; + private int lastCGStateId; // Record the state of the currently active CG private int maxEventChoice; // Data structure to track the events seen by each state to track cycles (containing all events) for termination private HashSet currVisitedStates; // States being visited in the current execution @@ -74,7 +75,7 @@ public class DPORStateReducer extends ListenerAdapter { private ArrayList cgList; // Record CGs for backtracking points private HashMap cgMap; // Maps state IDs to CGs private HashMap> conflictPairMap; // Record conflicting events -// private HashSet activeBacktrackCGs; // Record active backtrack CGs + private HashSet doneBacktrackSet; // Record state ID and trace that are done private HashMap readWriteFieldsMap; // Record fields that are accessed // Visible operation dependency graph implementation (SPIN paper) related fields @@ -94,31 +95,8 @@ public class DPORStateReducer extends ListenerAdapter { } else { out = null; } - // DPOR-related - choices = null; - refChoices = null; - choiceCounter = 0; - maxEventChoice = 0; - // Cycle tracking - currVisitedStates = new HashSet<>(); - justVisitedStates = new HashSet<>(); - prevVisitedStates = new HashSet<>(); - stateToEventMap = new HashMap<>(); - // Backtracking - backtrackMap = new HashMap<>(); - backtrackStateQ = new PriorityQueue<>(); - cgList = new ArrayList<>(); - cgMap = new HashMap<>(); - conflictPairMap = new HashMap<>(); -// activeBacktrackCGs = new HashSet<>(); - readWriteFieldsMap = new HashMap<>(); - // VOD graph - prevChoiceValue = -1; - vodGraphMap = new HashMap<>(); - // Booleans isBooleanCGFlipped = false; - isEndOfExecution = false; - isFirstResetDone = false; + initializeStatesVariables(); } @Override @@ -224,13 +202,14 @@ public class DPORStateReducer extends ListenerAdapter { if (stateReductionMode) { // Check the boolean CG and if it is flipped, we are resetting the analysis -// if (currentCG instanceof BooleanChoiceGenerator) { -// if (!isBooleanCGFlipped) { -// isBooleanCGFlipped = true; -// } else { -// initializeStateReduction(); -// } -// } + if (currentCG instanceof BooleanChoiceGenerator) { + if (!isBooleanCGFlipped) { + isBooleanCGFlipped = true; + } else { + // Allocate new objects for data structure when the boolean is flipped from "false" to "true" + initializeStatesVariables(); + } + } // Check every choice generated and ensure fair scheduling! if (currentCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; @@ -429,6 +408,34 @@ public class DPORStateReducer extends ListenerAdapter { return true; } + private void initializeStatesVariables() { + // DPOR-related + choices = null; + refChoices = null; + choiceCounter = 0; + lastCGStateId = 0; + maxEventChoice = 0; + // Cycle tracking + currVisitedStates = new HashSet<>(); + justVisitedStates = new HashSet<>(); + prevVisitedStates = new HashSet<>(); + stateToEventMap = new HashMap<>(); + // Backtracking + backtrackMap = new HashMap<>(); + backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); + cgList = new ArrayList<>(); + cgMap = new HashMap<>(); + conflictPairMap = new HashMap<>(); + doneBacktrackSet = new HashSet<>(); + readWriteFieldsMap = new HashMap<>(); + // VOD graph + prevChoiceValue = -1; + vodGraphMap = new HashMap<>(); + // Booleans + isEndOfExecution = false; + isFirstResetDone = false; + } + private void mapStateToEvent(int nextChoiceValue) { // Update all states with this event/choice // This means that all past states now see this transition @@ -473,6 +480,7 @@ public class DPORStateReducer extends ListenerAdapter { backtrackList = backtrackMap.get(stateId); } else { backtrackList = new LinkedList<>(); + backtrackMap.put(stateId, backtrackList); } backtrackList.addFirst(newChoiceList); // Add CG for this state ID if there isn't one yet @@ -565,8 +573,9 @@ public class DPORStateReducer extends ListenerAdapter { // Put the conflicting event numbers first and reverse the order int actualCurrCho = currentChoice % refChoices.length; int actualConfEvtNum = confEvtNum % refChoices.length; - newChoiceList[0] = refChoices[actualCurrCho]; - newChoiceList[1] = refChoices[actualConfEvtNum]; + // We use the actual choices here in case they have been modified/adjusted + newChoiceList[0] = choices[actualCurrCho]; + newChoiceList[1] = choices[actualConfEvtNum]; // 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++) { if (refChoices[i] != newChoiceList[0] && refChoices[i] != newChoiceList[1]) { @@ -576,6 +585,10 @@ public class DPORStateReducer extends ListenerAdapter { } // Record the backtracking point in the stack as well IntChoiceFromSet backtrackCG = cgList.get(confEvtNum); + // Check if this trace has been done starting from this state + if (isTraceConstructed(newChoiceList, backtrackCG)) { + return; + } //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList); addNewBacktrackPoint(backtrackCG, newChoiceList); } @@ -610,11 +623,10 @@ public class DPORStateReducer extends ListenerAdapter { private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG, VM vm) { // We can start exploring the next backtrack point after the current CG is advanced at least once if (icsCG.getNextChoiceIndex() > 0) { - if (backtrackMap.isEmpty()) { - // This means we are reaching the end of our execution: no more backtracking points to explore - return; + // Check if we are reaching the end of our execution: no more backtracking points to explore + if (!backtrackMap.isEmpty()) { + setNextBacktrackPoint(icsCG); } - setNextBacktrackPoint(icsCG); // Save all the visited states when starting a new execution of trace prevVisitedStates.addAll(currVisitedStates); currVisitedStates.clear(); @@ -652,7 +664,7 @@ public class DPORStateReducer extends ListenerAdapter { int actualEvtCntr = eventCounter % refChoices.length; 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) || (actualEvtCntr == actualCurrCho)) { + if (!readWriteFieldsMap.containsKey(eventCounter) || choices[actualCurrCho] == choices[actualEvtCntr]) { return false; } ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); @@ -696,14 +708,31 @@ public class DPORStateReducer extends ListenerAdapter { return true; } + private boolean isTraceConstructed(Integer[] choiceList, IntChoiceFromSet backtrackCG) { + // Concatenate state ID and trace in a string, e.g., "1:10234" + int stateId = backtrackCG.getStateId(); + StringBuilder sb = new StringBuilder(); + sb.append(stateId); + sb.append(':'); + for(Integer choice : choiceList) { + sb.append(choice); + } + // Check if the trace has been constructed as a backtrack point for this state + if (doneBacktrackSet.contains(sb.toString())) { + return true; + } + doneBacktrackSet.add(sb.toString()); + return false; + } + private void resetStatesForNewExecution(IntChoiceFromSet icsCG) { if (choices == null || choices != icsCG.getAllChoices()) { // Reset state variables - choiceCounter = 1; + choiceCounter = 0; choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); + lastCGStateId = icsCG.getStateId(); // Clearing data structures - backtrackMap.clear(); conflictPairMap.clear(); readWriteFieldsMap.clear(); stateToEventMap.clear(); @@ -713,7 +742,7 @@ public class DPORStateReducer extends ListenerAdapter { } } - private IntChoiceFromSet setBacktrackCG(int stateId) { + private void setBacktrackCG(int stateId) { // Set a backtrack CG based on a state ID IntChoiceFromSet backtrackCG = cgMap.get(stateId); LinkedList backtrackChoices = backtrackMap.get(stateId); @@ -725,7 +754,6 @@ public class DPORStateReducer extends ListenerAdapter { backtrackMap.remove(stateId); backtrackStateQ.remove(stateId); } - return backtrackCG; } private void setNextBacktrackPoint(IntChoiceFromSet icsCG) { @@ -736,21 +764,17 @@ public class DPORStateReducer extends ListenerAdapter { for (Integer stateId : cgMap.keySet()) { setBacktrackCG(stateId); } -// activeBacktrackCGs.addAll(cgMap.values()); isFirstResetDone = true; } else { - // Check if we still have backtrack points for the current CG - int currStateId = icsCG.getStateId(); - if (backtrackMap.containsKey(currStateId)) { - setBacktrackCG(currStateId); + // Check if we still have backtrack points for the last state after the last backtrack + if (backtrackMap.containsKey(lastCGStateId)) { + setBacktrackCG(lastCGStateId); } else { -// activeBacktrackCGs.remove(icsCG); // We try to reset new CGs (if we do have) when we are running out of active CGs if (!backtrackStateQ.isEmpty()) { // Reset the next CG with the latest state int hiStateId = backtrackStateQ.peek(); - IntChoiceFromSet backtrackCG = setBacktrackCG(hiStateId); -// activeBacktrackCGs.add(backtrackCG); + setBacktrackCG(hiStateId); } } }