X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducer.java;h=fe879895529b018884d09ca9450e040ea615fe3f;hp=72fc44e6c67f8ec4a48cfa8dd141a2ab043c33c3;hb=19a15ce37ab3cec800bfd5908bbc4d17259e4d49;hpb=b1c560c27cc9169acd9ad874b09df56eea7187a9 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 72fc44e..fe87989 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -60,9 +60,8 @@ public class DPORStateReducer extends ListenerAdapter { // DPOR-related fields // Basic information private Integer[] choices; - private Integer[] refChoices; + private Integer[] refChoices; // Second reference to a copy of choices (choices may be modified for fair scheduling) 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 @@ -72,7 +71,7 @@ public class DPORStateReducer extends ListenerAdapter { // Data structure to analyze field Read/Write accesses and conflicts private HashMap> backtrackMap; // Track created backtracking points private PriorityQueue backtrackStateQ; // Heap that returns the latest state - private ArrayList cgList; // Record CGs for backtracking points + private ArrayList backtrackPointList; // Record backtrack points (CG and choice) private HashMap cgMap; // Maps state IDs to CGs private HashMap> conflictPairMap; // Record conflicting events private HashSet doneBacktrackSet; // Record state ID and trace that are done @@ -84,7 +83,6 @@ public class DPORStateReducer extends ListenerAdapter { // Boolean states private boolean isBooleanCGFlipped; - private boolean isFirstResetDone; private boolean isEndOfExecution; public DPORStateReducer(Config config, JPF jpf) { @@ -188,7 +186,8 @@ public class DPORStateReducer extends ListenerAdapter { int choiceIndex = choiceCounter % choices.length; icsCG.advance(choices[choiceIndex]); // Index the ChoiceGenerator to set backtracking points - cgList.add(icsCG); + BacktrackPoint backtrackPoint = new BacktrackPoint(icsCG, choices[choiceIndex]); + backtrackPointList.add(backtrackPoint); } else { // Set done all CGs while transitioning to a new execution icsCG.setDone(); @@ -223,7 +222,7 @@ public class DPORStateReducer extends ListenerAdapter { updateVODGraph(icsCG.getNextChoice()); // Check if we have seen this state or this state contains cycles that involve all events if (terminateCurrentExecution()) { - exploreNextBacktrackPoints(icsCG, vm); + exploreNextBacktrackPoints(icsCG); } justVisitedStates.clear(); choiceCounter++; @@ -326,19 +325,19 @@ public class DPORStateReducer extends ListenerAdapter { // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices private class BacktrackPoint { private IntChoiceFromSet backtrackCG; // CG to backtrack from - private Integer[] backtrackChoices; // Choices to set for this backtrack CG + private int choice; // Choice chosen at this backtrack point - public BacktrackPoint(IntChoiceFromSet cg, Integer[] choices) { + public BacktrackPoint(IntChoiceFromSet cg, int cho) { backtrackCG = cg; - backtrackChoices = choices; + choice = cho; } public IntChoiceFromSet getBacktrackCG() { return backtrackCG; } - public Integer[] getBacktrackChoices() { - return backtrackChoices; + public int getChoice() { + return choice; } } @@ -413,7 +412,6 @@ public class DPORStateReducer extends ListenerAdapter { choices = null; refChoices = null; choiceCounter = 0; - lastCGStateId = 0; maxEventChoice = 0; // Cycle tracking currVisitedStates = new HashSet<>(); @@ -423,7 +421,7 @@ public class DPORStateReducer extends ListenerAdapter { // Backtracking backtrackMap = new HashMap<>(); backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); - cgList = new ArrayList<>(); + backtrackPointList = new ArrayList<>(); cgMap = new HashMap<>(); conflictPairMap = new HashMap<>(); doneBacktrackSet = new HashSet<>(); @@ -433,7 +431,6 @@ public class DPORStateReducer extends ListenerAdapter { vodGraphMap = new HashMap<>(); // Booleans isEndOfExecution = false; - isFirstResetDone = false; } private void mapStateToEvent(int nextChoiceValue) { @@ -572,10 +569,9 @@ public class DPORStateReducer extends ListenerAdapter { Integer[] newChoiceList = new Integer[refChoices.length]; // Put the conflicting event numbers first and reverse the order int actualCurrCho = currentChoice % refChoices.length; - int actualConfEvtNum = confEvtNum % refChoices.length; - // We use the actual choices here in case they have been modified/adjusted + // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method newChoiceList[0] = choices[actualCurrCho]; - newChoiceList[1] = choices[actualConfEvtNum]; + 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++) { if (refChoices[i] != newChoiceList[0] && refChoices[i] != newChoiceList[1]) { @@ -583,8 +579,8 @@ public class DPORStateReducer extends ListenerAdapter { j++; } } - // Record the backtracking point in the stack as well - IntChoiceFromSet backtrackCG = cgList.get(confEvtNum); + // Get the backtrack CG for this backtrack point + IntChoiceFromSet backtrackCG = backtrackPointList.get(confEvtNum).getBacktrackCG(); // Check if this trace has been done starting from this state if (isTraceConstructed(newChoiceList, backtrackCG)) { return; @@ -620,13 +616,30 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG, VM vm) { + private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG) { // We can start exploring the next backtrack point after the current CG is advanced at least once if (icsCG.getNextChoiceIndex() > 0) { + HashSet backtrackCGs = new HashSet<>(cgMap.values()); // Check if we are reaching the end of our execution: no more backtracking points to explore - if (!backtrackMap.isEmpty()) { - setNextBacktrackPoint(icsCG); + // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough) + if (!backtrackStateQ.isEmpty()) { + // Reset the next CG with the latest state + int hiStateId = backtrackStateQ.peek(); + // Check with the current state and if it's lower than the highest state, we defer to this lower state + int currStateId = icsCG.getStateId(); + if (currStateId < hiStateId && cgMap.keySet().contains(currStateId)) { + hiStateId = currStateId; + } + setBacktrackCG(hiStateId, backtrackCGs); + } + // Clear unused CGs + for (BacktrackPoint backtrackPoint : backtrackPointList) { + IntChoiceFromSet cg = backtrackPoint.getBacktrackCG(); + if (!backtrackCGs.contains(cg)) { + cg.setDone(); + } } + backtrackPointList.clear(); // Save all the visited states when starting a new execution of trace prevVisitedStates.addAll(currVisitedStates); currVisitedStates.clear(); @@ -661,10 +674,11 @@ public class DPORStateReducer extends ListenerAdapter { } private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) { - 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) || choices[actualCurrCho] == choices[actualEvtCntr]) { + if (!readWriteFieldsMap.containsKey(eventCounter) || + choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) { return false; } ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); @@ -731,20 +745,25 @@ public class DPORStateReducer extends ListenerAdapter { choiceCounter = 0; choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); - lastCGStateId = icsCG.getStateId(); // Clearing data structures conflictPairMap.clear(); readWriteFieldsMap.clear(); stateToEventMap.clear(); isEndOfExecution = false; - // Adding this CG as the first CG for this execution - cgList.add(icsCG); + // Adding this CG as the first backtrack point for this execution + backtrackPointList.add(new BacktrackPoint(icsCG, choices[0])); } } - private void setBacktrackCG(int stateId) { + private void setBacktrackCG(int stateId, HashSet backtrackCGs) { // Set a backtrack CG based on a state ID IntChoiceFromSet backtrackCG = cgMap.get(stateId); + // Need to reset the CGs first so that the CG last reset will be chosen next + for (IntChoiceFromSet cg : backtrackCGs) { + if (cg != backtrackCG && cg.getNextChoiceIndex() > -1) { + cg.reset(); + } + } LinkedList backtrackChoices = backtrackMap.get(stateId); backtrackCG.setNewValues(backtrackChoices.removeLast()); // Get the last from the queue backtrackCG.reset(); @@ -756,37 +775,6 @@ public class DPORStateReducer extends ListenerAdapter { } } - private void setNextBacktrackPoint(IntChoiceFromSet icsCG) { - - HashSet backtrackCGs = new HashSet<>(cgMap.values()); - if (!isFirstResetDone) { - // Reset the last CG of every LinkedList in the map and set done everything else - for (Integer stateId : cgMap.keySet()) { - setBacktrackCG(stateId); - } - isFirstResetDone = true; - } else { - // Check if we still have backtrack points for the last state after the last backtrack - if (backtrackMap.containsKey(lastCGStateId)) { - setBacktrackCG(lastCGStateId); - } else { - // 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(); - setBacktrackCG(hiStateId); - } - } - } - // Clear unused CGs - for(IntChoiceFromSet cg : cgList) { - if (!backtrackCGs.contains(cg)) { - cg.setDone(); - } - } - cgList.clear(); - } - // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper // This method checks whether a choice is reachable in the VOD graph from a reference choice (BFS algorithm)