From 19a15ce37ab3cec800bfd5908bbc4d17259e4d49 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Tue, 7 Apr 2020 16:53:36 -0700 Subject: [PATCH] First part of boolean flip seems to be clean; need to debug the second part and figure out what to do when the current state is lower than the highest state ID for backtrack. --- .../nasa/jpf/listener/DPORStateReducer.java | 75 ++++++++----------- 1 file changed, 31 insertions(+), 44 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 53cd566..fe87989 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -62,7 +62,6 @@ public class DPORStateReducer extends ListenerAdapter { private Integer[] choices; 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 @@ -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) { @@ -224,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++; @@ -414,7 +412,6 @@ public class DPORStateReducer extends ListenerAdapter { choices = null; refChoices = null; choiceCounter = 0; - lastCGStateId = 0; maxEventChoice = 0; // Cycle tracking currVisitedStates = new HashSet<>(); @@ -434,7 +431,6 @@ public class DPORStateReducer extends ListenerAdapter { vodGraphMap = new HashMap<>(); // Booleans isEndOfExecution = false; - isFirstResetDone = false; } private void mapStateToEvent(int nextChoiceValue) { @@ -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,7 +745,6 @@ public class DPORStateReducer extends ListenerAdapter { choiceCounter = 0; choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); - lastCGStateId = icsCG.getStateId(); // Clearing data structures conflictPairMap.clear(); readWriteFieldsMap.clear(); @@ -742,9 +755,15 @@ public class DPORStateReducer extends ListenerAdapter { } } - 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,38 +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(BacktrackPoint backtrackPoint : backtrackPointList) { - IntChoiceFromSet cg = backtrackPoint.getBacktrackCG(); - if (!backtrackCGs.contains(cg)) { - cg.setDone(); - } - } - backtrackPointList.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) -- 2.34.1