From fa86b972ca0ced9985639d19684ed1e4fc8cad56 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 3 Apr 2020 16:13:34 -0700 Subject: [PATCH] Reimplementing DPOR Phase 3: Architecting the subsequent executions (backtrack points); need to test how CGs are explored with the current DFSearch. --- .../nasa/jpf/listener/DPORStateReducer.java | 255 ++++++++++++------ 1 file changed, 172 insertions(+), 83 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 8c6a1d6..feb51c7 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -69,12 +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 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 activeBacktrackCGs; // Record active backtrack CGs + private HashMap readWriteFieldsMap; // Record fields that are accessed // Visible operation dependency graph implementation (SPIN paper) related fields private int prevChoiceValue; @@ -82,6 +83,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); @@ -103,16 +106,19 @@ public class DPORStateReducer extends ListenerAdapter { stateToEventMap = new HashMap<>(); // Backtracking backtrackMap = new HashMap<>(); - btrckPtsStack = new Stack<>(); - btrckCGSet = new HashSet<>(); + backtrackStateQ = new PriorityQueue<>(); cgList = new ArrayList<>(); + cgMap = new HashMap<>(); conflictPairMap = new HashMap<>(); +// activeBacktrackCGs = new HashSet<>(); readWriteFieldsMap = new HashMap<>(); // VOD graph prevChoiceValue = -1; vodGraphMap = new HashMap<>(); // Booleans isBooleanCGFlipped = false; + isEndOfExecution = false; + isFirstResetDone = false; } @Override @@ -187,23 +193,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); } } } @@ -223,6 +234,8 @@ public class DPORStateReducer extends ListenerAdapter { // 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 +244,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 +255,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); + } } } } @@ -449,6 +465,26 @@ 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<>(); + } + 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 @@ -540,10 +576,8 @@ 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); + //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList); + addNewBacktrackPoint(backtrackCG, newChoiceList); } private boolean excludeThisForItContains(String[] excludedStrings, String className) { @@ -573,31 +607,19 @@ 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 + if (backtrackMap.isEmpty()) { + // This means we are reaching the end of our execution: no more backtracking points to explore return; } - 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(); + setNextBacktrackPoint(icsCG); // 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 +648,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) || (actualEvtCntr == actualCurrCho)) { return false; } ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); @@ -672,6 +696,71 @@ public class DPORStateReducer extends ListenerAdapter { return true; } + private void resetStatesForNewExecution(IntChoiceFromSet icsCG) { + if (choices == null || choices != icsCG.getAllChoices()) { + // Reset state variables + choiceCounter = 0; + choices = icsCG.getAllChoices(); + refChoices = copyChoices(choices); + // Clearing data structures + backtrackMap.clear(); + conflictPairMap.clear(); + readWriteFieldsMap.clear(); + stateToEventMap.clear(); + isEndOfExecution = false; + } + } + + private IntChoiceFromSet 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); + } + return backtrackCG; + } + + 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); + } +// activeBacktrackCGs.addAll(cgMap.values()); + isFirstResetDone = true; + } else { + // Check if we still have backtrack points for the current CG + int currStateId = icsCG.getStateId(); + if (backtrackMap.containsKey(currStateId)) { + setBacktrackCG(currStateId); + } else { +// activeBacktrackCGs.remove(icsCG); + // 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(); + IntChoiceFromSet backtrackCG = setBacktrackCG(hiStateId); +// activeBacktrackCGs.add(backtrackCG); + } + } + } + // 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) -- 2.34.1