From: rtrimana Date: Thu, 2 Apr 2020 23:20:26 +0000 (-0700) Subject: Reimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=dbaa88b6ff8bd4ae38fc19d131ac8340826c3763;ds=sidebyside Reimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and conflict analysis; cleaning up and refactoring. --- diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index a688754..8c6a1d6 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -58,20 +58,27 @@ public class DPORStateReducer extends ListenerAdapter { private Transition transition; // DPOR-related fields + // Basic information private Integer[] choices; private Integer[] refChoices; private int choiceCounter; private int maxEventChoice; - // Record CGs for backtracking points - private List cgList; // Data structure to track the events seen by each state to track cycles (containing all events) for termination - private HashMap> stateToEventMap; + private HashSet currVisitedStates; // States being visited in the current execution private HashSet justVisitedStates; // States just visited in the previous choice/event private HashSet prevVisitedStates; // States visited in the previous execution - private HashSet currVisitedStates; // States being visited in the current execution - // Data structure to analyze field Read/Write accesses - private HashMap readWriteFieldsMap; - private HashMap> conflictPairMap; + 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 + + // Visible operation dependency graph implementation (SPIN paper) related fields + private int prevChoiceValue; + private HashMap> vodGraphMap; // Visible operation dependency graph (VOD graph) // Boolean states private boolean isBooleanCGFlipped; @@ -89,13 +96,21 @@ public class DPORStateReducer extends ListenerAdapter { refChoices = null; choiceCounter = 0; maxEventChoice = 0; - cgList = new ArrayList<>(); - stateToEventMap = new HashMap<>(); + // Cycle tracking + currVisitedStates = new HashSet<>(); justVisitedStates = new HashSet<>(); prevVisitedStates = new HashSet<>(); - currVisitedStates = new HashSet<>(); - readWriteFieldsMap = new HashMap<>(); + 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; } @@ -182,6 +197,8 @@ public class DPORStateReducer extends ListenerAdapter { // 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]); @@ -210,6 +227,8 @@ public class DPORStateReducer extends ListenerAdapter { checkAndEnforceFairScheduling(icsCG); // 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()) { exploreNextBacktrackSets(icsCG); @@ -227,10 +246,10 @@ public class DPORStateReducer extends ListenerAdapter { ChoiceGenerator cg = vm.getChoiceGenerator(); if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) { int currentChoice = choiceCounter - 1; // Accumulative choice w.r.t the current trace - //if (getCurrentChoice(vm) < 0) { // If choice is -1 then skip 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 @@ -250,23 +269,13 @@ public class DPORStateReducer extends ListenerAdapter { String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); if (!isFieldExcluded(fieldClass)) { // Check for conflict (go backward from current choice and get the first conflict) - for (int evtCntr = currentChoice - 1; evtCntr >= 0; evtCntr--) { - if (!readWriteFieldsMap.containsKey(evtCntr)) { // Skip if this event does not have any Read/Write set - continue; - } - ReadWriteSet rwSet = readWriteFieldsMap.get(evtCntr); - int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef(); + for (int eventCounter = currentChoice - 1; eventCounter >= 0; eventCounter--) { // Check for conflicts with Write fields for both Read and Write instructions - if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) && - rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) || - (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) && - rwSet.readFieldObjectId(fieldClass) == currObjId)) { - // Check and record a backtrack set for just once! - if (successfullyRecordConflictPair(currentChoice, evtCntr)) { - // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above) -// if (vm.isNewState() || isReachableInVODGraph(refChoices[currentChoice], refChoices[currentChoice-1])) { -// createBacktrackChoiceList(currentChoice, eventNumber); -// } + // 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); } } } @@ -279,7 +288,9 @@ public class DPORStateReducer extends ListenerAdapter { // == HELPERS - // -- INNER CLASS + + // -- INNER CLASSES + // This class compactly stores Read and Write field sets // We store the field name and its object ID // Sharing the same field means the same field name and object ID @@ -317,6 +328,25 @@ public class DPORStateReducer extends ListenerAdapter { } } + // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices + private class BacktrackPoint { + private IntChoiceFromSet backtrackCG; // CG to backtrack from + private Integer[] backtrackChoices; // Choices to set for this backtrack CG + + public BacktrackPoint(IntChoiceFromSet cg, Integer[] choices) { + backtrackCG = cg; + backtrackChoices = choices; + } + + public IntChoiceFromSet getBacktrackCG() { + return backtrackCG; + } + + public Integer[] getBacktrackChoices() { + return backtrackChoices; + } + } + // -- CONSTANTS private final static String DO_CALL_METHOD = "doCall"; // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure @@ -455,6 +485,9 @@ public class DPORStateReducer extends ListenerAdapter { } // Get the iterated object whose property is accessed ElementInfo eiAccessObj = VM.getVM().getHeap().get(frameSlots[1]); + if (eiAccessObj == null) { + return; + } // We exclude library classes (they start with java, org, etc.) and some more String objClassName = eiAccessObj.getClassInfo().getName(); if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName) || @@ -476,6 +509,43 @@ public class DPORStateReducer extends ListenerAdapter { } } + private int checkAndAdjustChoice(int currentChoice, VM vm) { + // 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); + if (currChoiceInd != currChoiceFromCG) { + currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG; + } + return currentChoice; + } + + private void createBacktrackingPoint(int currentChoice, int confEvtNum) { + + // Create a new list of choices for backtrack based on the current choice and conflicting event number + // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2} + // for the original set {0, 1, 2, 3} + Integer[] newChoiceList = new Integer[refChoices.length]; + // 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]; + // 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]) { + newChoiceList[j] = refChoices[i]; + j++; + } + } + // 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); + } + private boolean excludeThisForItContains(String[] excludedStrings, String className) { for (String excludedField : excludedStrings) { if (className.contains(excludedField)) { @@ -503,11 +573,32 @@ public class DPORStateReducer extends ListenerAdapter { return false; } + // TODO: THIS METHOD IS STILL UNTESTED AT THIS POINT private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) { - // Save all the visited states when starting a new execution of trace - prevVisitedStates.addAll(currVisitedStates); - currVisitedStates.clear(); - + // We try to update the CG with a backtrack list if the state has been visited multiple times + if (icsCG.getNextChoiceIndex() > 0) { + if (btrckPtsStack.empty()) { + // TODO: PROBABLY NEED TO DO CONTEXT SWITCHING HERE + 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(); + // Save all the visited states when starting a new execution of trace + prevVisitedStates.addAll(currVisitedStates); + currVisitedStates.clear(); + } } private int getCurrentChoice(VM vm) { @@ -535,6 +626,23 @@ 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)) { + return false; + } + ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); + int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef(); + // Check for conflicts with Write fields for both Read and Write instructions + if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) && + rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) || + (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) && + rwSet.readFieldObjectId(fieldClass) == currObjId)) { + return true; + } + return false; + } + private boolean isFieldExcluded(String field) { // Check against "starts-with", "ends-with", and "contains" list if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) || @@ -546,7 +654,7 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private boolean successfullyRecordConflictPair(int currentEvent, int eventNumber) { + private boolean isNewConflict(int currentEvent, int eventNumber) { HashSet conflictSet; if (!conflictPairMap.containsKey(currentEvent)) { conflictSet = new HashSet<>(); @@ -555,7 +663,7 @@ public class DPORStateReducer extends ListenerAdapter { conflictSet = conflictPairMap.get(currentEvent); } // If this conflict has been recorded before, we return false because - // we don't want to service this backtrack point twice + // we don't want to save this backtrack point twice if (conflictSet.contains(eventNumber)) { return false; } @@ -563,4 +671,62 @@ public class DPORStateReducer extends ListenerAdapter { conflictSet.add(eventNumber); return true; } + + // --- 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) + //private boolean isReachableInVODGraph(int checkedChoice, int referenceChoice) { + private boolean isReachableInVODGraph(int currentChoice) { + // Extract previous and current events + int choiceIndex = currentChoice % refChoices.length; + int currEvent = refChoices[choiceIndex]; + int prevEvent = refChoices[choiceIndex - 1]; + // Record visited choices as we search in the graph + HashSet visitedChoice = new HashSet<>(); + visitedChoice.add(prevEvent); + LinkedList nodesToVisit = new LinkedList<>(); + // If the state doesn't advance as the threads/sub-programs are executed (basically there is no new state), + // there is a chance that the graph doesn't have new nodes---thus this check will return a null. + if (vodGraphMap.containsKey(prevEvent)) { + nodesToVisit.addAll(vodGraphMap.get(prevEvent)); + while(!nodesToVisit.isEmpty()) { + int choice = nodesToVisit.getFirst(); + if (choice == currEvent) { + return true; + } + if (visitedChoice.contains(choice)) { // If there is a loop then we don't find it + return false; + } + // Continue searching + visitedChoice.add(choice); + HashSet choiceNextNodes = vodGraphMap.get(choice); + if (choiceNextNodes != null) { + // Add only if there is a mapping for next nodes + for (Integer nextNode : choiceNextNodes) { + // Skip cycles + if (nextNode == choice) { + continue; + } + nodesToVisit.addLast(nextNode); + } + } + } + } + return false; + } + + private void updateVODGraph(int currChoiceValue) { + // Update the graph when we have the current choice value + HashSet choiceSet; + if (vodGraphMap.containsKey(prevChoiceValue)) { + // If the key already exists, just retrieve it + choiceSet = vodGraphMap.get(prevChoiceValue); + } else { + // Create a new entry + choiceSet = new HashSet<>(); + vodGraphMap.put(prevChoiceValue, choiceSet); + } + choiceSet.add(currChoiceValue); + prevChoiceValue = currChoiceValue; + } }