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=72fc44e6c67f8ec4a48cfa8dd141a2ab043c33c3;hp=8c6a1d69e5bb7fcdcbb96281b14c4d7f9e5f8639;hb=b1c560c27cc9169acd9ad874b09df56eea7187a9;hpb=dbaa88b6ff8bd4ae38fc19d131ac8340826c3763 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 8c6a1d6..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 @@ -69,12 +70,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 HashMap> backtrackMap; // Track created backtracking points - private Stack btrckPtsStack; // Stack that stores backtracking points - private List cgList; // Record CGs for backtracking points - private HashSet btrckCGSet; // Set that records all the backtrack CGs - private HashMap> conflictPairMap; // Record conflicting events - 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 cgList; // Record CGs for backtracking points + 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; @@ -82,6 +84,8 @@ public class DPORStateReducer extends ListenerAdapter { // Boolean states private boolean isBooleanCGFlipped; + private boolean isFirstResetDone; + private boolean isEndOfExecution; public DPORStateReducer(Config config, JPF jpf) { verboseMode = config.getBoolean("printout_state_transition", false); @@ -91,28 +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<>(); - btrckPtsStack = new Stack<>(); - btrckCGSet = new HashSet<>(); - cgList = new ArrayList<>(); - conflictPairMap = new HashMap<>(); - readWriteFieldsMap = new HashMap<>(); - // VOD graph - prevChoiceValue = -1; - vodGraphMap = new HashMap<>(); - // Booleans isBooleanCGFlipped = false; + initializeStatesVariables(); } @Override @@ -187,23 +171,28 @@ public class DPORStateReducer extends ListenerAdapter { // Initialize with necessary information from the CG if (nextCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG; - // Check if CG has been initialized, otherwise initialize it - Integer[] cgChoices = icsCG.getAllChoices(); - // Record the events (from choices) - if (choices == null) { - choices = cgChoices; - // Make a copy of choices as reference - refChoices = copyChoices(choices); - // Record the max event choice (the last element of the choice array) - maxEventChoice = choices[choices.length - 1]; + if (!isEndOfExecution) { + // Check if CG has been initialized, otherwise initialize it + Integer[] cgChoices = icsCG.getAllChoices(); + // Record the events (from choices) + if (choices == null) { + choices = cgChoices; + // Make a copy of choices as reference + refChoices = copyChoices(choices); + // Record the max event choice (the last element of the choice array) + maxEventChoice = choices[choices.length - 1]; + } + icsCG.setNewValues(choices); + icsCG.reset(); + // 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 + cgList.add(icsCG); + } else { + // Set done all CGs while transitioning to a new execution + icsCG.setDone(); } - icsCG.setNewValues(choices); - icsCG.reset(); - // 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 - cgList.add(icsCG); } } } @@ -213,16 +202,19 @@ 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; + // 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 checkAndEnforceFairScheduling(icsCG); // Map state to event @@ -231,7 +223,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()) { - exploreNextBacktrackSets(icsCG); + exploreNextBacktrackPoints(icsCG, vm); } justVisitedStates.clear(); choiceCounter++; @@ -242,40 +234,43 @@ public class DPORStateReducer extends ListenerAdapter { @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { - // Has to be initialized and a integer CG - ChoiceGenerator cg = vm.getChoiceGenerator(); - if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) { - int currentChoice = choiceCounter - 1; // Accumulative choice w.r.t the current trace - if (currentChoice < 0) { // If choice is -1 then skip - return; - } - currentChoice = checkAndAdjustChoice(currentChoice, vm); - // Record accesses from executed instructions - if (executedInsn instanceof JVMFieldInstruction) { - // Analyze only after being initialized - String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName(); - // We don't care about libraries - if (!isFieldExcluded(fieldClass)) { - analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice); + if (!isEndOfExecution) { + // Has to be initialized and a integer CG + ChoiceGenerator cg = vm.getChoiceGenerator(); + if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) { + int currentChoice = choiceCounter - 1; // Accumulative choice w.r.t the current trace + if (currentChoice < 0) { // If choice is -1 then skip + return; } - } else if (executedInsn instanceof INVOKEINTERFACE) { - // Handle the read/write accesses that occur through iterators - analyzeReadWriteAccesses(executedInsn, ti, currentChoice); - } - // Analyze conflicts from next instructions - if (nextInsn instanceof JVMFieldInstruction) { - // Skip the constructor because it is called once and does not have shared access with other objects - if (!nextInsn.getMethodInfo().getName().equals("")) { - String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); + currentChoice = checkAndAdjustChoice(currentChoice, vm); + // Record accesses from executed instructions + if (executedInsn instanceof JVMFieldInstruction) { + // Analyze only after being initialized + String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName(); + // We don't care about libraries if (!isFieldExcluded(fieldClass)) { - // Check for conflict (go backward from current choice and get the first conflict) - for (int eventCounter = currentChoice - 1; eventCounter >= 0; eventCounter--) { - // Check for conflicts with Write fields for both Read and Write instructions - // Check and record a backtrack set for just once! - if (isConflictFound(nextInsn, eventCounter, fieldClass) && isNewConflict(currentChoice, eventCounter)) { - // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above) - if (vm.isNewState() || isReachableInVODGraph(currentChoice)) { - createBacktrackingPoint(currentChoice, eventCounter); + analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice); + } + } else if (executedInsn instanceof INVOKEINTERFACE) { + // Handle the read/write accesses that occur through iterators + analyzeReadWriteAccesses(executedInsn, ti, currentChoice); + } + // Analyze conflicts from next instructions + if (nextInsn instanceof JVMFieldInstruction) { + // Skip the constructor because it is called once and does not have shared access with other objects + if (!nextInsn.getMethodInfo().getName().equals("")) { + String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); + if (!isFieldExcluded(fieldClass)) { + // Check for conflict (go backward from current choice and get the first conflict) + for (int eventCounter = currentChoice - 1; eventCounter >= 0; eventCounter--) { + // Check for conflicts with Write fields for both Read and Write instructions + // Check and record a backtrack set for just once! + if (isConflictFound(nextInsn, eventCounter, currentChoice, fieldClass) && + isNewConflict(currentChoice, eventCounter)) { + // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above) + if (vm.isNewState() || isReachableInVODGraph(currentChoice)) { + createBacktrackingPoint(currentChoice, eventCounter); + } } } } @@ -413,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 @@ -449,6 +472,27 @@ public class DPORStateReducer extends ListenerAdapter { // --- Functions related to Read/Write access analysis on shared fields + private void addNewBacktrackPoint(IntChoiceFromSet backtrackCG, Integer[] newChoiceList) { + int stateId = backtrackCG.getStateId(); + // Insert backtrack point to the right state ID + LinkedList backtrackList; + if (backtrackMap.containsKey(stateId)) { + 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 + if (!cgMap.containsKey(stateId)) { + cgMap.put(stateId, backtrackCG); + } + // Add to priority queue + if (!backtrackStateQ.contains(stateId)) { + backtrackStateQ.add(stateId); + } + } + // Analyze Read/Write accesses that are directly invoked on fields private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) { // Do the analysis to get Read and Write accesses to fields @@ -529,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]) { @@ -540,10 +585,12 @@ public class DPORStateReducer extends ListenerAdapter { } // Record the backtracking point in the stack as well IntChoiceFromSet backtrackCG = cgList.get(confEvtNum); - BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList); - btrckPtsStack.push(backtrackPoint); - // Also record the CG in the set - btrckCGSet.add(backtrackCG); + // 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); } private boolean excludeThisForItContains(String[] excludedStrings, String className) { @@ -573,31 +620,18 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - // TODO: THIS METHOD IS STILL UNTESTED AT THIS POINT - private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) { - // We try to update the CG with a backtrack list if the state has been visited multiple times + 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 (btrckPtsStack.empty()) { - // TODO: PROBABLY NEED TO DO CONTEXT SWITCHING HERE - return; + // Check if we are reaching the end of our execution: no more backtracking points to explore + if (!backtrackMap.isEmpty()) { + setNextBacktrackPoint(icsCG); } - BacktrackPoint backtrackPoint = btrckPtsStack.pop(); - Integer[] choiceList = backtrackPoint.getBacktrackChoices(); - IntChoiceFromSet backtrackCG = backtrackPoint.getBacktrackCG(); - // Deploy the new choice list for this CG - backtrackCG.setNewValues(choiceList); - backtrackCG.reset(); - // Clear unused CGs - for(IntChoiceFromSet cg : cgList) { - if (!btrckCGSet.contains(cg)) { - cg.setDone(); - } - } - cgList.clear(); - btrckCGSet.clear(); // Save all the visited states when starting a new execution of trace prevVisitedStates.addAll(currVisitedStates); currVisitedStates.clear(); + // This marks a transitional period to the new CG + isEndOfExecution = true; } } @@ -626,9 +660,11 @@ public class DPORStateReducer extends ListenerAdapter { return rwSet; } - private boolean isConflictFound(Instruction nextInsn, int eventCounter, String fieldClass) { - // Skip if this event does not have any Read/Write set - if (!readWriteFieldsMap.containsKey(eventCounter)) { + 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]) { return false; } ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); @@ -672,6 +708,85 @@ 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 = 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); + } + } + + private void setBacktrackCG(int stateId) { + // Set a backtrack CG based on a state ID + IntChoiceFromSet backtrackCG = cgMap.get(stateId); + LinkedList backtrackChoices = backtrackMap.get(stateId); + backtrackCG.setNewValues(backtrackChoices.removeLast()); // 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); + } + } + + 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)