From e576d51a191dd7fec0ccb0fa24202fc7846f19d7 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Wed, 8 Apr 2020 14:30:55 -0700 Subject: [PATCH 1/1] Committing a version that almost works: bug to fix is that when an execution finishes and the first backtrack point requires to get back to a higher state, there is no mechanism to roll back to that state. --- .../nasa/jpf/listener/DPORStateReducer.java | 103 +++++++++++++----- 1 file changed, 78 insertions(+), 25 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index fe87989..643350a 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -69,13 +69,14 @@ 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 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 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 // Visible operation dependency graph implementation (SPIN paper) related fields private int prevChoiceValue; @@ -212,6 +213,10 @@ 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); // If we don't see a fair scheduling of events/choices then we have to enforce it @@ -222,7 +227,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); + exploreNextBacktrackPoints(icsCG, vm); } justVisitedStates.clear(); choiceCounter++; @@ -230,6 +235,19 @@ 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) { @@ -419,6 +437,7 @@ 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<>(); @@ -561,6 +580,29 @@ public class DPORStateReducer extends ListenerAdapter { 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 @@ -616,21 +658,18 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG) { + 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 (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 = 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); + int hiStateId = getHighestStateId(icsCG, vm); + IntChoiceFromSet backtrackCG = setBacktrackCG(hiStateId, backtrackCGs); + currBacktrackCG = backtrackCG; } // Clear unused CGs for (BacktrackPoint backtrackPoint : backtrackPointList) { @@ -660,6 +699,24 @@ public class DPORStateReducer extends ListenerAdapter { } } + 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; @@ -755,7 +812,7 @@ public class DPORStateReducer extends ListenerAdapter { } } - private void setBacktrackCG(int stateId, HashSet backtrackCGs) { + private IntChoiceFromSet 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 @@ -765,14 +822,10 @@ public class DPORStateReducer extends ListenerAdapter { } } LinkedList backtrackChoices = backtrackMap.get(stateId); - backtrackCG.setNewValues(backtrackChoices.removeLast()); // Get the last from the queue + backtrackCG.setNewValues(backtrackChoices.peekLast()); // Get the last from the queue backtrackCG.reset(); - // 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 backtrackCG; } // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper -- 2.34.1