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=bf06232f33e149185ec9f35fb2f1f108ff3efd17;hp=e613f09fb15609ebc3f45e9f337351dbc1a80e06;hb=960a84cbcae04e3e57dfbaf70644671ba0714126;hpb=3f2ed878a49e2214926a724ccf7ced0939f5a0af diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index e613f09..bf06232 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -28,8 +28,11 @@ import gov.nasa.jpf.vm.bytecode.WriteInstruction; import gov.nasa.jpf.vm.choice.IntChoiceFromSet; import gov.nasa.jpf.vm.choice.IntIntervalGenerator; +import java.io.FileWriter; import java.io.PrintWriter; import java.util.*; +import java.util.logging.Logger; +import java.io.IOException; // TODO: Fix for Groovy's model-checking // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR @@ -39,12 +42,13 @@ import java.util.*; * This DPOR implementation is augmented by the algorithm presented in this SPIN paper: * http://spinroot.com/spin/symposia/ws08/spin2008_submission_33.pdf * - * The algorithm is presented on page 11 of the paper. Basically, we create a graph G - * (i.e., visible operation dependency graph) - * that maps inter-related threads/sub-programs that trigger state changes. - * The key to this approach is that we evaluate graph G in every iteration/recursion to - * only update the backtrack sets of the threads/sub-programs that are reachable in graph G - * from the currently running thread/sub-program. + * The algorithm is presented on page 11 of the paper. Basically, we have a graph G + * (i.e., visible operation dependency graph). + * This DPOR implementation actually fixes the algorithm in the SPIN paper that does not + * consider cases where a state could be matched early. In this new algorithm/implementation, + * each run is terminated iff: + * - we find a state that matches a state in a previous run, or + * - we have a matched state in the current run that consists of cycles that contain all choices/events. */ public class DPORStateReducer extends ListenerAdapter { @@ -52,6 +56,7 @@ public class DPORStateReducer extends ListenerAdapter { private boolean verboseMode; private boolean stateReductionMode; private final PrintWriter out; + private PrintWriter fileWriter; private String detail; private int depth; private int id; @@ -69,22 +74,22 @@ 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 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 Execution currentExecution; // Holds the information about the current execution private HashSet doneBacktrackSet; // Record state ID and trace already constructed - 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; - private HashMap> vodGraphMap; // Visible operation dependency graph (VOD graph) + private HashMap stateToChoiceCounterMap; // Maps state IDs to the choice counter + private HashMap> rGraph; // Create a reachability graph // Boolean states private boolean isBooleanCGFlipped; private boolean isEndOfExecution; + // Statistics + private int numOfConflicts; + private int numOfTransitions; + public DPORStateReducer(Config config, JPF jpf) { verboseMode = config.getBoolean("printout_state_transition", false); stateReductionMode = config.getBoolean("activate_state_reduction", true); @@ -93,7 +98,16 @@ public class DPORStateReducer extends ListenerAdapter { } else { out = null; } + String outputFile = config.getString("file_output"); + if (!outputFile.isEmpty()) { + try { + fileWriter = new PrintWriter(new FileWriter(outputFile, true), true); + } catch (IOException e) { + } + } isBooleanCGFlipped = false; + numOfConflicts = 0; + numOfTransitions = 0; restorableStateMap = new HashMap<>(); initializeStatesVariables(); } @@ -157,10 +171,26 @@ public class DPORStateReducer extends ListenerAdapter { } } + static Logger log = JPF.getLogger("report"); + @Override public void searchFinished(Search search) { + if (stateReductionMode) { + // Number of conflicts = first trace + subsequent backtrack points + numOfConflicts += 1 + doneBacktrackSet.size(); + } if (verboseMode) { + out.println("\n==> DEBUG: ----------------------------------- search finished"); + out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode); + out.println("\n==> DEBUG: Number of conflicts : " + numOfConflicts); + out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions); out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n"); + + fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode); + fileWriter.println("==> DEBUG: Number of conflicts : " + numOfConflicts); + fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions); + fileWriter.println(); + fileWriter.close(); } } @@ -203,6 +233,8 @@ public class DPORStateReducer extends ListenerAdapter { if (!isBooleanCGFlipped) { isBooleanCGFlipped = true; } else { + // Number of conflicts = first trace + subsequent backtrack points + numOfConflicts = 1 + doneBacktrackSet.size(); // Allocate new objects for data structure when the boolean is flipped from "false" to "true" initializeStatesVariables(); } @@ -214,17 +246,21 @@ public class DPORStateReducer extends ListenerAdapter { resetStatesForNewExecution(icsCG, vm); // If we don't see a fair scheduling of events/choices then we have to enforce it 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()) { + // Explore the next backtrack point: + // 1) if we have seen this state or this state contains cycles that involve all events, and + // 2) after the current CG is advanced at least once + if (terminateCurrentExecution() && choiceCounter > 0) { exploreNextBacktrackPoints(vm, icsCG); + } else { + numOfTransitions++; } + // Map state to event + mapStateToEvent(icsCG.getNextChoice()); justVisitedStates.clear(); choiceCounter++; } + } else { + numOfTransitions++; } } @@ -258,18 +294,7 @@ public class DPORStateReducer extends ListenerAdapter { 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); - } - } - } + findFirstConflictAndCreateBacktrackPoint(currentChoice, nextInsn, fieldClass); } } } @@ -283,6 +308,95 @@ public class DPORStateReducer extends ListenerAdapter { // -- INNER CLASSES + // This class compactly stores backtrack execution: + // 1) backtrack choice list, and + // 2) backtrack execution + private class BacktrackExecution { + private Integer[] choiceList; + private Execution execution; + + public BacktrackExecution(Integer[] choList, Execution exec) { + choiceList = choList; + execution = exec; + } + + public Integer[] getChoiceList() { + return choiceList; + } + + public Execution getExecution() { + return execution; + } + } + + // This class compactly stores backtrack points: + // 1) backtrack state ID, and + // 2) backtracking choices + private class BacktrackPoint { + 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 stId, int cho) { + backtrackCG = cg; + stateId = stId; + choice = cho; + } + + public IntChoiceFromSet getBacktrackCG() { return backtrackCG; } + + public int getStateId() { + return stateId; + } + + public int getChoice() { + return choice; + } + } + + // This class stores a representation of the execution graph node + private class Execution { + private ArrayList executionTrace; // The BacktrackPoint objects of this execution + private int parentChoice; // The parent's choice that leads to this execution + private Execution parent; // Store the parent for backward DFS to find conflicts + private HashMap readWriteFieldsMap; // Record fields that are accessed + + public Execution() { + executionTrace = new ArrayList<>(); + parentChoice = -1; + parent = null; + readWriteFieldsMap = new HashMap<>(); + } + + public void addBacktrackPoint(BacktrackPoint newBacktrackPoint) { + executionTrace.add(newBacktrackPoint); + } + + public ArrayList getExecutionTrace() { + return executionTrace; + } + + public int getParentChoice() { + return parentChoice; + } + + public Execution getParent() { + return parent; + } + + public HashMap getReadWriteFieldsMap() { + return readWriteFieldsMap; + } + + public void setParentChoice(int parChoice) { + parentChoice = parChoice; + } + + public void setParent(Execution par) { + parent = par; + } + } + // 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 @@ -303,6 +417,14 @@ public class DPORStateReducer extends ListenerAdapter { writeSet.put(field, objectId); } + public Set getReadSet() { + return readSet.keySet(); + } + + public Set getWriteSet() { + return writeSet.keySet(); + } + public boolean readFieldExists(String field) { return readSet.containsKey(field); } @@ -320,26 +442,25 @@ public class DPORStateReducer extends ListenerAdapter { } } - // This class compactly stores backtrack points: 1) backtrack state ID, and 2) backtracking choices - private class BacktrackPoint { - 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 stId, int cho) { - backtrackCG = cg; - stateId = stId; - choice = cho; - } - public IntChoiceFromSet getBacktrackCG() { return backtrackCG; } + // This class stores a compact representation of a reachability graph for past executions + private class ReachableTrace { + private ArrayList pastBacktrackPointList; + private HashMap pastReadWriteFieldsMap; - public int getStateId() { - return stateId; + public ReachableTrace(ArrayList btrackPointList, + HashMap rwFieldsMap) { + pastBacktrackPointList = btrackPointList; + pastReadWriteFieldsMap = rwFieldsMap; } - public int getChoice() { - return choice; + public ArrayList getPastBacktrackPointList() { + return pastBacktrackPointList; + } + + public HashMap getPastReadWriteFieldsMap() { + return pastReadWriteFieldsMap; } } @@ -376,7 +497,12 @@ public class DPORStateReducer extends ListenerAdapter { } } // Record state ID and choice/event as backtrack point - backtrackPointList.add(new BacktrackPoint(icsCG, vm.getStateId(), refChoices[choiceIndex])); + int stateId = vm.getStateId(); +// backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex])); + currentExecution.addBacktrackPoint(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex])); + // Store restorable state object for this state (always store the latest) + RestorableVMState restorableState = vm.getRestorableState(); + restorableStateMap.put(stateId, restorableState); } private Integer[] copyChoices(Integer[] choicesToCopy) { @@ -425,13 +551,10 @@ public class DPORStateReducer extends ListenerAdapter { // Backtracking backtrackMap = new HashMap<>(); backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); - backtrackPointList = new ArrayList<>(); - conflictPairMap = new HashMap<>(); + currentExecution = new Execution(); doneBacktrackSet = new HashSet<>(); - readWriteFieldsMap = new HashMap<>(); - // VOD graph - prevChoiceValue = -1; - vodGraphMap = new HashMap<>(); + stateToChoiceCounterMap = new HashMap<>(); + rGraph = new HashMap<>(); // Booleans isEndOfExecution = false; } @@ -461,30 +584,50 @@ public class DPORStateReducer extends ListenerAdapter { // Update the state variables // Line 19 in the paper page 11 (see the heading note above) int stateId = search.getStateId(); - currVisitedStates.add(stateId); // Insert state ID into the map if it is new if (!stateToEventMap.containsKey(stateId)) { HashSet eventSet = new HashSet<>(); stateToEventMap.put(stateId, eventSet); } + // Save execution state into the Reachability only if + // (1) It is not a revisited state from a past execution, or + // (2) It is just a new backtracking point + // TODO: New algorithm +/* if (!prevVisitedStates.contains(stateId) || + choiceCounter <= 1) { + ReachableTrace reachableTrace= new + ReachableTrace(backtrackPointList, readWriteFieldsMap); + ArrayList rTrace; + if (!prevVisitedStates.contains(stateId)) { + rTrace = new ArrayList<>(); + rGraph.put(stateId, rTrace); + } else { + rTrace = rGraph.get(stateId); + } + rTrace.add(reachableTrace); + } + stateToChoiceCounterMap.put(stateId, choiceCounter); + analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);*/ justVisitedStates.add(stateId); - // Store restorable state object for this state (always store the latest) - RestorableVMState restorableState = search.getVM().getRestorableState(); - restorableStateMap.put(stateId, restorableState); + currVisitedStates.add(stateId); } // --- Functions related to Read/Write access analysis on shared fields - private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList) { + private void addNewBacktrackPoint(int stateId, Integer[] newChoiceList, Execution parentExecution, int parentChoice) { // Insert backtrack point to the right state ID - LinkedList backtrackList; + LinkedList backtrackExecList; if (backtrackMap.containsKey(stateId)) { - backtrackList = backtrackMap.get(stateId); + backtrackExecList = backtrackMap.get(stateId); } else { - backtrackList = new LinkedList<>(); - backtrackMap.put(stateId, backtrackList); + backtrackExecList = new LinkedList<>(); + backtrackMap.put(stateId, backtrackExecList); } - backtrackList.addFirst(newChoiceList); + // Add the new backtrack execution object + Execution newExecution = new Execution(); + newExecution.setParent(parentExecution); + newExecution.setParentChoice(parentChoice); + backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, newExecution)); // Add to priority queue if (!backtrackStateQ.contains(stateId)) { backtrackStateQ.add(stateId); @@ -555,15 +698,24 @@ 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 = 0; + int currChoiceFromCG = currChoiceInd; ChoiceGenerator currentCG = vm.getChoiceGenerator(); // This is the main event CG - if (currentCG instanceof IntChoiceFromSet) { - currChoiceFromCG = currChoiceInd; - } else { + if (currentCG instanceof IntIntervalGenerator) { // This is the interval CG used in device handlers ChoiceGenerator parentCG = ((IntIntervalGenerator) currentCG).getPreviousChoiceGenerator(); - currChoiceFromCG = ((IntChoiceFromSet) parentCG).getNextChoiceIndex(); + // Iterate until we find the IntChoiceFromSet CG + while (!(parentCG instanceof IntChoiceFromSet)) { + parentCG = ((IntIntervalGenerator) parentCG).getPreviousChoiceGenerator(); + } + int actualEvtNum = ((IntChoiceFromSet) parentCG).getNextChoice(); + // Find the index of the event/choice in refChoices + for (int i = 0; i pastTrace = execution.getExecutionTrace(); + ArrayList currTrace = currentExecution.getExecutionTrace(); + int backtrackEvent = currTrace.get(currentChoice).getChoice(); + int stateId = pastTrace.get(conflictChoice).getStateId(); + // Check if this trace has been done from this state + if (isTraceAlreadyConstructed(backtrackEvent, stateId)) { + return; + } // Put the conflicting event numbers first and reverse the order - int actualCurrCho = currentChoice % refChoices.length; - // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method - newChoiceList[0] = choices[actualCurrCho]; - newChoiceList[1] = backtrackPointList.get(confEvtNum).getChoice(); + newChoiceList[0] = backtrackEvent; + newChoiceList[1] = pastTrace.get(conflictChoice).getChoice(); // 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]) { @@ -589,14 +748,8 @@ public class DPORStateReducer extends ListenerAdapter { j++; } } - // Get the backtrack CG for this backtrack point - int stateId = backtrackPointList.get(confEvtNum).getStateId(); - // Check if this trace has been done starting from this state - if (isTraceAlreadyConstructed(newChoiceList, stateId)) { - return; - } - //BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList); - addNewBacktrackPoint(stateId, newChoiceList); + // Parent choice is conflict choice - 1 + addNewBacktrackPoint(stateId, newChoiceList, execution, conflictChoice - 1); } private boolean excludeThisForItContains(String[] excludedStrings, String className) { @@ -628,70 +781,165 @@ public class DPORStateReducer extends ListenerAdapter { 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) { - // 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()) { - // 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(); - } - // 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; - } + // 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()) { + // Set done all the other backtrack points + for (BacktrackPoint backtrackPoint : currentExecution.getExecutionTrace()) { + 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(); + } + // 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; } - private ReadWriteSet getReadWriteSet(int currentChoice) { - // Do the analysis to get Read and Write accesses to fields - ReadWriteSet rwSet; - // We already have an entry - if (readWriteFieldsMap.containsKey(currentChoice)) { - rwSet = readWriteFieldsMap.get(currentChoice); - } else { // We need to create a new entry - rwSet = new ReadWriteSet(); - readWriteFieldsMap.put(currentChoice, rwSet); + private void findFirstConflictAndCreateBacktrackPoint(int currentChoice, Instruction nextInsn, String fieldClass) { + // Check for conflict (go backward from current choice and get the first conflict) + Execution execution = currentExecution; + // Actual choice of the current execution trace + //int actualChoice = currentChoice % refChoices.length; + // Choice/event we want to check for conflict against (start from actual choice) + int pastChoice = currentChoice; + // Perform backward DFS through the execution graph + while (true) { + // Get the next conflict choice + if (pastChoice > 0) { + // Case #1: check against a previous choice in the same execution for conflict + pastChoice = pastChoice - 1; + } else { // pastChoice == 0 means we are at the first BacktrackPoint of this execution path + // Case #2: check against a previous choice in a parent execution + int parentChoice = execution.getParentChoice(); + if (parentChoice > -1) { + // Get the parent execution + execution = execution.getParent(); + pastChoice = execution.getParentChoice(); + } else { + // If parent is -1 then this is the first execution (it has no parent) and we stop here + break; + } + } + // Check if a conflict is found + if (isConflictFound(nextInsn, pastChoice, execution, currentChoice, fieldClass)) { + createBacktrackingPoint(currentChoice, pastChoice, execution); + break; // Stop at the first found conflict + } } - return rwSet; } - private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) { + private boolean isConflictFound(Instruction nextInsn, int pastChoice, Execution pastExecution, + int currentChoice, String fieldClass) { - int actualCurrCho = currentChoice % refChoices.length; + HashMap pastRWFieldsMap = pastExecution.getReadWriteFieldsMap(); + ArrayList pastTrace = pastExecution.getExecutionTrace(); + ArrayList currTrace = currentExecution.getExecutionTrace(); // 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] == backtrackPointList.get(eventCounter).getChoice()) { + if (!pastRWFieldsMap.containsKey(pastChoice) || + //choices[actualChoice] == pastTrace.get(pastChoice).getChoice()) { + currTrace.get(currentChoice).getChoice() == pastTrace.get(pastChoice).getChoice()) { return false; } - ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter); + HashMap currRWFieldsMap = pastExecution.getReadWriteFieldsMap(); + ReadWriteSet rwSet = currRWFieldsMap.get(pastChoice); 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)) { + rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) || + (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) && + rwSet.readFieldObjectId(fieldClass) == currObjId)) { return true; } return false; } + // private boolean isConflictFound(int eventCounter, int currentChoice, boolean isPastTrace) { +// +// int currActualChoice; +// if (isPastTrace) { +// currActualChoice = backtrackPointList.get(currentChoice).getChoice(); +// } else { +// int actualCurrCho = currentChoice % refChoices.length; +// currActualChoice = choices[actualCurrCho]; +// } +// // 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) || +// currActualChoice == backtrackPointList.get(eventCounter).getChoice()) { +// return false; +// } +// // Current R/W set +// ReadWriteSet currRWSet = readWriteFieldsMap.get(currentChoice); +// // R/W set of choice/event that may have a potential conflict +// ReadWriteSet evtRWSet = readWriteFieldsMap.get(eventCounter); +// // Check for conflicts with Read and Write fields for Write instructions +// Set currWriteSet = currRWSet.getWriteSet(); +// for(String writeField : currWriteSet) { +// int currObjId = currRWSet.writeFieldObjectId(writeField); +// if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) || +// (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) { +// return true; +// } +// } +// // Check for conflicts with Write fields for Read instructions +// Set currReadSet = currRWSet.getReadSet(); +// for(String readField : currReadSet) { +// int currObjId = currRWSet.readFieldObjectId(readField); +// if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) { +// return true; +// } +// } +// // Return false if no conflict is found +// return false; +// } + +// private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) { +// +// 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] == backtrackPointList.get(eventCounter).getChoice()) { +// 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 ReadWriteSet getReadWriteSet(int currentChoice) { + // Do the analysis to get Read and Write accesses to fields + ReadWriteSet rwSet; + // We already have an entry + HashMap currReadWriteFieldsMap = currentExecution.getReadWriteFieldsMap(); + if (currReadWriteFieldsMap.containsKey(currentChoice)) { + rwSet = currReadWriteFieldsMap.get(currentChoice); + } else { // We need to create a new entry + rwSet = new ReadWriteSet(); + currReadWriteFieldsMap.put(currentChoice, rwSet); + } + return rwSet; + } + private boolean isFieldExcluded(String field) { // Check against "starts-with", "ends-with", and "contains" list if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) || @@ -703,25 +951,7 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private boolean isNewConflict(int currentEvent, int eventNumber) { - HashSet conflictSet; - if (!conflictPairMap.containsKey(currentEvent)) { - conflictSet = new HashSet<>(); - conflictPairMap.put(currentEvent, conflictSet); - } else { - conflictSet = conflictPairMap.get(currentEvent); - } - // If this conflict has been recorded before, we return false because - // we don't want to save this backtrack point twice - if (conflictSet.contains(eventNumber)) { - return false; - } - // If it hasn't been recorded, then do otherwise - conflictSet.add(eventNumber); - return true; - } - - private boolean isTraceAlreadyConstructed(Integer[] choiceList, int stateId) { + private boolean isTraceAlreadyConstructed(int firstChoice, int stateId) { // Concatenate state ID and only the first event in the string, e.g., "1:1 for the trace 10234 at state 1" // TODO: THIS IS AN OPTIMIZATION! // This is the optimized version because after we execute, e.g., the trace 1:10234, we don't need to try @@ -730,7 +960,7 @@ public class DPORStateReducer extends ListenerAdapter { StringBuilder sb = new StringBuilder(); sb.append(stateId); sb.append(':'); - sb.append(choiceList[0]); + sb.append(firstChoice); // Check if the trace has been constructed as a backtrack point for this state if (doneBacktrackSet.contains(sb.toString())) { return true; @@ -745,84 +975,170 @@ public class DPORStateReducer extends ListenerAdapter { choiceCounter = 0; choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); - // Clearing data structures - conflictPairMap.clear(); - readWriteFieldsMap.clear(); - stateToEventMap.clear(); + // Clear data structures + stateToChoiceCounterMap = new HashMap<>(); + stateToEventMap = new HashMap<>(); isEndOfExecution = false; - backtrackPointList.clear(); } } private void setBacktrackCG(int stateId, IntChoiceFromSet backtrackCG) { // Set a backtrack CG based on a state ID - LinkedList backtrackChoices = backtrackMap.get(stateId); - backtrackCG.setNewValues(backtrackChoices.removeLast()); // Get the last from the queue + LinkedList backtrackExecutions = backtrackMap.get(stateId); + BacktrackExecution backtrackExecution = backtrackExecutions.removeLast(); + backtrackCG.setNewValues(backtrackExecution.getChoiceList()); // Get the last from the queue backtrackCG.setStateId(stateId); backtrackCG.reset(); + // Update current execution with this new execution + Execution newExecution = backtrackExecution.getExecution(); + if (newExecution.getParentChoice() == -1) { + // If it is -1 then that means we should start from the end of the parent trace for backward DFS + ArrayList parentTrace = newExecution.getParent().getExecutionTrace(); + newExecution.setParentChoice(parentTrace.size() - 1); + } + currentExecution = newExecution; // Remove from the queue if we don't have more backtrack points for that state - if (backtrackChoices.isEmpty()) { + if (backtrackExecutions.isEmpty()) { backtrackMap.remove(stateId); backtrackStateQ.remove(stateId); } } - // --- 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 prevChoIndex = (currentChoice - 1) % refChoices.length; - int currEvent = refChoices[choiceIndex]; - int prevEvent = refChoices[prevChoIndex]; - // 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); - } - } + // --- Functions related to the reachability analysis when there is a state match + + // We use backtrackPointsList to analyze the reachable states/events when there is a state match: + // 1) Whenever there is state match, there is a cycle of events + // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle + // 3) Then we create a new backtrack point for every new conflict + private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { + // Perform this analysis only when: + // 1) there is a state match, + // 2) this is not during a switch to a new execution, + // 3) at least 2 choices/events have been explored (choiceCounter > 1), + // 4) the matched state has been encountered in the current execution, and + // 5) state > 0 (state 0 is for boolean CG) + if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && (stateId > 0)) { + if (currVisitedStates.contains(stateId)) { + // Update the backtrack sets in the cycle + updateBacktrackSetsInCycle(stateId); + } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution + // Update the backtrack sets in a previous execution + updateBacktrackSetsInPreviousExecution(stateId); } } - return false; } - private void updateVODGraph(int currChoiceValue) { - // Update the graph when we have the current choice value + // Get the start event for the past execution trace when there is a state matched from a past execution + private int getPastConflictChoice(int stateId, ArrayList pastBacktrackPointList) { + // Iterate and find the first occurrence of the state ID + // It is guaranteed that a choice should be found because the state ID is in the list + int pastConfChoice = 0; + for(int i = 0; i getReachableStateIds(Set stateIds, int stateId) { + // Only include state IDs equal or greater than the input stateId: these are reachable states + ArrayList sortedStateIds = new ArrayList<>(); + for(Integer stId : stateIds) { + if (stId >= stateId) { + sortedStateIds.add(stId); + } + } + Collections.sort(sortedStateIds); + return sortedStateIds; + } + + // Update the backtrack sets in the cycle + private void updateBacktrackSetsInCycle(int stateId) { +// // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts +// int conflictChoice = stateToChoiceCounterMap.get(stateId); +// int currentChoice = choiceCounter - 1; +// // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward) +// while (conflictChoice < currentChoice) { +// for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) { +// if (isConflictFound(eventCounter, conflictChoice, false)) { +//// && isNewConflict(conflictChoice, eventCounter)) { +// createBacktrackingPoint(conflictChoice, eventCounter, false); +// } +// } +// conflictChoice++; +// } + } + + // TODO: OPTIMIZATION! + // Check and make sure that state ID and choice haven't been explored for this trace + private boolean isNotChecked(HashMap> checkedStateIdAndChoice, + BacktrackPoint backtrackPoint) { + int stateId = backtrackPoint.getStateId(); + int choice = backtrackPoint.getChoice(); HashSet choiceSet; - if (vodGraphMap.containsKey(prevChoiceValue)) { - // If the key already exists, just retrieve it - choiceSet = vodGraphMap.get(prevChoiceValue); + if (checkedStateIdAndChoice.containsKey(stateId)) { + choiceSet = checkedStateIdAndChoice.get(stateId); + if (choiceSet.contains(choice)) { + // State ID and choice found. It has been checked! + return false; + } } else { - // Create a new entry choiceSet = new HashSet<>(); - vodGraphMap.put(prevChoiceValue, choiceSet); + checkedStateIdAndChoice.put(stateId, choiceSet); } - choiceSet.add(currChoiceValue); - prevChoiceValue = currChoiceValue; + choiceSet.add(choice); + + return true; + } + + // Update the backtrack sets in a previous execution + private void updateBacktrackSetsInPreviousExecution(int stateId) { +// // Don't check a past trace twice! +// HashSet checkedTrace = new HashSet<>(); +// // Don't check the same event twice for a revisited state +// HashMap> checkedStateIdAndChoice = new HashMap<>(); +// // Get sorted reachable state IDs +// ArrayList reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId); +// // Iterate from this state ID until the biggest state ID +// for(Integer stId : reachableStateIds) { +// // Find the right reachability graph object that contains the stateId +// ArrayList rTraces = rGraph.get(stId); +// for (ReachableTrace rTrace : rTraces) { +// if (!checkedTrace.contains(rTrace)) { +// // Find the choice/event that marks the start of the subtrace from the previous execution +// ArrayList pastBacktrackPointList = rTrace.getPastBacktrackPointList(); +// HashMap pastReadWriteFieldsMap = rTrace.getPastReadWriteFieldsMap(); +// int pastConfChoice = getPastConflictChoice(stId, pastBacktrackPointList); +// int conflictChoice = choiceCounter; +// // Iterate from the starting point until the end of the past execution trace +// while (pastConfChoice < pastBacktrackPointList.size() - 1) { // BacktrackPoint list always has a surplus of 1 +// // Get the info of the event from the past execution trace +// BacktrackPoint confBtrackPoint = pastBacktrackPointList.get(pastConfChoice); +// if (isNotChecked(checkedStateIdAndChoice, confBtrackPoint)) { +// ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice); +// // Append this event to the current list and map +// backtrackPointList.add(confBtrackPoint); +// readWriteFieldsMap.put(choiceCounter, rwSet); +// for (int eventCounter = conflictChoice - 1; eventCounter >= 0; eventCounter--) { +// if (isConflictFound(eventCounter, conflictChoice, true)) { +// && isNewConflict(conflictChoice, eventCounter)) { +// createBacktrackingPoint(conflictChoice, eventCounter, true); +// } +// } +// // Remove this event to replace it with a new one +// backtrackPointList.remove(backtrackPointList.size() - 1); +// readWriteFieldsMap.remove(choiceCounter); +// } +// pastConfChoice++; +// } +// checkedTrace.add(rTrace); +// } +// } +// } } }