From: rtrimana Date: Thu, 9 Apr 2020 07:03:43 +0000 (-0700) Subject: Changing approach: Using vm.restoreState() method to restore JPF to the desired state... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=ebcf259b97ccf4d66fe75b59a5ebd36fadda4ddd Changing approach: Using vm.restoreState() method to restore JPF to the desired state when backtracking; everything looks correct but probably needs more tests. --- diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 643350a..54170ea 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -69,14 +69,13 @@ public class DPORStateReducer extends ListenerAdapter { private HashSet prevVisitedStates; // States visited in the previous execution private HashMap> stateToEventMap; // Data structure to analyze field Read/Write accesses and conflicts - private IntChoiceFromSet currBacktrackCG; // Current backtrack CG - private HashMap> backtrackMap; // Track created backtracking points - private PriorityQueue backtrackStateQ; // Heap that returns the latest state - 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 - private HashMap readWriteFieldsMap; // Record fields that are accessed + private HashMap> backtrackMap; // Track created backtracking points + private PriorityQueue backtrackStateQ; // Heap that returns the latest state + private ArrayList backtrackPointList; // Record backtrack points (CG, state Id, and choice) + private HashMap> conflictPairMap; // Record conflicting events + private HashSet doneBacktrackSet; // Record state ID and trace that are done + private HashMap readWriteFieldsMap; // Record fields that are accessed + private HashMap restorableStateMap; // Maps state IDs to the restorable state object // Visible operation dependency graph implementation (SPIN paper) related fields private int prevChoiceValue; @@ -95,6 +94,7 @@ public class DPORStateReducer extends ListenerAdapter { out = null; } isBooleanCGFlipped = false; + restorableStateMap = new HashMap<>(); initializeStatesVariables(); } @@ -186,9 +186,6 @@ public class DPORStateReducer extends ListenerAdapter { // Use a modulo since choiceCounter is going to keep increasing int choiceIndex = choiceCounter % choices.length; icsCG.advance(choices[choiceIndex]); - // Index the ChoiceGenerator to set backtracking points - BacktrackPoint backtrackPoint = new BacktrackPoint(icsCG, choices[choiceIndex]); - backtrackPointList.add(backtrackPoint); } else { // Set done all CGs while transitioning to a new execution icsCG.setDone(); @@ -213,21 +210,17 @@ public class DPORStateReducer extends ListenerAdapter { // Check every choice generated and ensure fair scheduling! if (currentCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; - // Check if the current CG is the CG just being reset - if (!checkCurrentCGIsValid(icsCG, vm)) { - return; - } // If this is a new CG then we need to update data structures - resetStatesForNewExecution(icsCG); + resetStatesForNewExecution(icsCG, vm); // If we don't see a fair scheduling of events/choices then we have to enforce it - checkAndEnforceFairScheduling(icsCG); + fairSchedulingAndBacktrackPoint(icsCG, vm); // Map state to event mapStateToEvent(icsCG.getNextChoice()); // Update the VOD graph always with the latest 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(vm, icsCG); } justVisitedStates.clear(); choiceCounter++; @@ -235,19 +228,6 @@ public class DPORStateReducer extends ListenerAdapter { } } - private RestorableVMState restorableVMState = null; - - private void restoreState(IntChoiceFromSet icsCG, VM vm) { - - if (icsCG.getStateId() == 10) { - restorableVMState = vm.getRestorableState(); - } - if (restorableVMState != null && icsCG.getStateId() < 10) { - //vm.restoreState(restorableVMState); - System.out.println(); - } - } - @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { @@ -340,18 +320,22 @@ public class DPORStateReducer extends ListenerAdapter { } } - // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices + // This class compactly stores backtrack points: 1) backtrack state ID, and 2) backtracking choices private class BacktrackPoint { - private IntChoiceFromSet backtrackCG; // CG to backtrack from + private IntChoiceFromSet backtrackCG; // CG at this backtrack point + private int stateId; // State at this backtrack point private int choice; // Choice chosen at this backtrack point - public BacktrackPoint(IntChoiceFromSet cg, int cho) { + public BacktrackPoint(IntChoiceFromSet cg, int stId, int cho) { backtrackCG = cg; + stateId = stId; choice = cho; } - public IntChoiceFromSet getBacktrackCG() { - return backtrackCG; + public IntChoiceFromSet getBacktrackCG() { return backtrackCG; } + + public int getStateId() { + return stateId; } public int getChoice() { @@ -380,7 +364,7 @@ public class DPORStateReducer extends ListenerAdapter { private final static String JAVA_STRING_LIB = "java.lang.String"; // -- FUNCTIONS - private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) { + private void fairSchedulingAndBacktrackPoint(IntChoiceFromSet icsCG, VM vm) { // Check the next choice and if the value is not the same as the expected then force the expected value int choiceIndex = choiceCounter % refChoices.length; int nextChoice = icsCG.getNextChoice(); @@ -391,6 +375,8 @@ public class DPORStateReducer extends ListenerAdapter { icsCG.setChoice(currCGIndex, expectedChoice); } } + // Record state ID and choice/event as backtrack point + backtrackPointList.add(new BacktrackPoint(icsCG, vm.getStateId(), refChoices[choiceIndex])); } private Integer[] copyChoices(Integer[] choicesToCopy) { @@ -437,11 +423,9 @@ public class DPORStateReducer extends ListenerAdapter { prevVisitedStates = new HashSet<>(); stateToEventMap = new HashMap<>(); // Backtracking - currBacktrackCG = null; backtrackMap = new HashMap<>(); backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); backtrackPointList = new ArrayList<>(); - cgMap = new HashMap<>(); conflictPairMap = new HashMap<>(); doneBacktrackSet = new HashSet<>(); readWriteFieldsMap = new HashMap<>(); @@ -484,12 +468,14 @@ public class DPORStateReducer extends ListenerAdapter { stateToEventMap.put(stateId, eventSet); } justVisitedStates.add(stateId); + // Store restorable state object for this state (always store the latest) + RestorableVMState restorableState = search.getVM().getRestorableState(); + restorableStateMap.put(stateId, restorableState); } // --- Functions related to Read/Write access analysis on shared fields - private void addNewBacktrackPoint(IntChoiceFromSet backtrackCG, Integer[] newChoiceList) { - int stateId = backtrackCG.getStateId(); + private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList) { // Insert backtrack point to the right state ID LinkedList backtrackList; if (backtrackMap.containsKey(stateId)) { @@ -499,10 +485,6 @@ public class DPORStateReducer extends ListenerAdapter { backtrackMap.put(stateId, backtrackList); } backtrackList.addFirst(newChoiceList); - // Add CG for this state ID if there isn't one yet - if (!cgMap.containsKey(stateId)) { - cgMap.put(stateId, backtrackCG); - } // Add to priority queue if (!backtrackStateQ.contains(stateId)) { backtrackStateQ.add(stateId); @@ -573,36 +555,22 @@ public class DPORStateReducer extends ListenerAdapter { // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator // for certain method calls in the infrastructure, e.g., eventSince() int currChoiceInd = currentChoice % refChoices.length; - int currChoiceFromCG = getCurrentChoice(vm); + int currChoiceFromCG = 0; + ChoiceGenerator currentCG = vm.getChoiceGenerator(); + // This is the main event CG + if (currentCG instanceof IntChoiceFromSet) { + currChoiceFromCG = currChoiceInd; + } else { + // This is the interval CG used in device handlers + ChoiceGenerator parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator(); + currChoiceFromCG = ((IntChoiceFromSet) parentCG).getNextChoiceIndex(); + } if (currChoiceInd != currChoiceFromCG) { currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG; } return currentChoice; } - private boolean checkCurrentCGIsValid(IntChoiceFromSet icsCG, VM vm) { - // Check if the execution explored is from the last CG being reset - if (isEndOfExecution) { - if (currBacktrackCG != null && currBacktrackCG != icsCG) { - // If the reset CG isn't explored, try to explore another one - exploreNextBacktrackPoints(icsCG, vm); - return false; - } else { - int stateId = currBacktrackCG.getStateId(); - LinkedList backtrackChoices = backtrackMap.get(stateId); - backtrackChoices.removeLast(); - // Remove from the queue if we don't have more backtrack points for that state - if (backtrackChoices.isEmpty()) { - cgMap.remove(stateId); - backtrackMap.remove(stateId); - backtrackStateQ.remove(stateId); - } - return true; - } - } - return true; - } - private void createBacktrackingPoint(int currentChoice, int confEvtNum) { // Create a new list of choices for backtrack based on the current choice and conflicting event number @@ -622,13 +590,13 @@ public class DPORStateReducer extends ListenerAdapter { } } // Get the backtrack CG for this backtrack point - IntChoiceFromSet backtrackCG = backtrackPointList.get(confEvtNum).getBacktrackCG(); + int stateId = backtrackPointList.get(confEvtNum).getStateId(); // Check if this trace has been done starting from this state - if (isTraceConstructed(newChoiceList, backtrackCG)) { + if (isTraceConstructed(newChoiceList, stateId)) { return; } //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList); - addNewBacktrackPoint(backtrackCG, newChoiceList); + addNewBacktrackPoint(stateId, newChoiceList); } private boolean excludeThisForItContains(String[] excludedStrings, String className) { @@ -658,27 +626,31 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG, VM vm) { + private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) { // We can start exploring the next backtrack point after the current CG is advanced at least once if (choiceCounter > 0) { - HashSet backtrackCGs = new HashSet<>(cgMap.values()); // Check if we are reaching the end of our execution: no more backtracking points to explore // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough) if (!backtrackStateQ.isEmpty()) { - // Reset the next CG with the latest state - int hiStateId = getHighestStateId(icsCG, vm); - IntChoiceFromSet backtrackCG = setBacktrackCG(hiStateId, backtrackCGs); - currBacktrackCG = backtrackCG; - } - // Clear unused CGs - for (BacktrackPoint backtrackPoint : backtrackPointList) { - IntChoiceFromSet cg = backtrackPoint.getBacktrackCG(); - if (!backtrackCGs.contains(cg)) { - cg.setDone(); + // Set done all the other backtrack points + for (BacktrackPoint backtrackPoint : backtrackPointList) { + backtrackPoint.getBacktrackCG().setDone(); } + // Reset the next backtrack point with the latest state + int hiStateId = backtrackStateQ.peek(); + // Restore the state first if necessary + if (vm.getStateId() != hiStateId) { + RestorableVMState restorableState = restorableStateMap.get(hiStateId); + vm.restoreState(restorableState); + } + // Set the backtrack CG + IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator(); + setBacktrackCG(hiStateId, backtrackCG); + } else { + // Set done this last CG (we save a few rounds) + icsCG.setDone(); } - backtrackPointList.clear(); // Save all the visited states when starting a new execution of trace prevVisitedStates.addAll(currVisitedStates); currVisitedStates.clear(); @@ -687,36 +659,6 @@ public class DPORStateReducer extends ListenerAdapter { } } - private int getCurrentChoice(VM vm) { - ChoiceGenerator currentCG = vm.getChoiceGenerator(); - // This is the main event CG - if (currentCG instanceof IntChoiceFromSet) { - return ((IntChoiceFromSet) currentCG).getNextChoiceIndex(); - } else { - // This is the interval CG used in device handlers - ChoiceGenerator parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator(); - return ((IntChoiceFromSet) parentCG).getNextChoiceIndex(); - } - } - - private int getHighestStateId(IntChoiceFromSet icsCG, VM vm) { - // Try to look for the highest state from the queue - 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) { - // Find the next CG with the next highest state - while (!cgMap.keySet().contains(currStateId) && currStateId > 0) { // Stop at state 0 - currStateId--; - } - if (currStateId > 0) { // If we reach this, it means that there are only CGs with higher states left - hiStateId = currStateId; - } - } - - return hiStateId; - } - private ReadWriteSet getReadWriteSet(int currentChoice) { // Do the analysis to get Read and Write accesses to fields ReadWriteSet rwSet; @@ -779,9 +721,8 @@ public class DPORStateReducer extends ListenerAdapter { return true; } - private boolean isTraceConstructed(Integer[] choiceList, IntChoiceFromSet backtrackCG) { + private boolean isTraceConstructed(Integer[] choiceList, int stateId) { // 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(':'); @@ -796,7 +737,7 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private void resetStatesForNewExecution(IntChoiceFromSet icsCG) { + private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) { if (choices == null || choices != icsCG.getAllChoices()) { // Reset state variables choiceCounter = 0; @@ -807,25 +748,21 @@ public class DPORStateReducer extends ListenerAdapter { readWriteFieldsMap.clear(); stateToEventMap.clear(); isEndOfExecution = false; - // Adding this CG as the first backtrack point for this execution - backtrackPointList.add(new BacktrackPoint(icsCG, choices[0])); + backtrackPointList.clear(); } } - private IntChoiceFromSet setBacktrackCG(int stateId, HashSet backtrackCGs) { + private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) { // 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.peekLast()); // Get the last from the queue + backtrackCG.setNewValues(backtrackChoices.removeLast()); // Get the last from the queue + backtrackCG.setStateId(stateId); backtrackCG.reset(); - - return backtrackCG; + // Remove from the queue if we don't have more backtrack points for that state + if (backtrackChoices.isEmpty()) { + backtrackMap.remove(stateId); + backtrackStateQ.remove(stateId); + } } // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper @@ -835,8 +772,9 @@ public class DPORStateReducer extends ListenerAdapter { private boolean isReachableInVODGraph(int currentChoice) { // Extract previous and current events int choiceIndex = currentChoice % refChoices.length; + int prevChoIndex = (currentChoice - 1) % refChoices.length; int currEvent = refChoices[choiceIndex]; - int prevEvent = refChoices[choiceIndex - 1]; + int prevEvent = refChoices[prevChoIndex]; // Record visited choices as we search in the graph HashSet visitedChoice = new HashSet<>(); visitedChoice.add(prevEvent);