X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FStateReducer.java;h=e03135454330bf21df98cb80db167cfc819fd8de;hp=67446f323faf1e6d4c6aaecc5128d6feabe9299f;hb=9f853a376c28deeae82cb6e9e2841c4f2a0d2fa3;hpb=1418a055d0a3e09ae21b101195659f04be39c882 diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 67446f3..e031354 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -23,25 +23,32 @@ import gov.nasa.jpf.ListenerAdapter; import gov.nasa.jpf.search.Search; import gov.nasa.jpf.jvm.bytecode.*; import gov.nasa.jpf.vm.*; -import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction; import gov.nasa.jpf.vm.bytecode.ReadInstruction; -import gov.nasa.jpf.vm.bytecode.StoreInstruction; import gov.nasa.jpf.vm.bytecode.WriteInstruction; -import gov.nasa.jpf.vm.choice.IntIntervalGenerator; +import gov.nasa.jpf.vm.choice.IntChoiceFromSet; import java.io.PrintWriter; import java.util.*; // TODO: Fix for Groovy's model-checking -// TODO: This is a listener created to detect device conflicts and global variable conflicts +// TODO: This is a setter to change the values of the ChoiceGenerator to implement POR /** - * Simple listener tool to track remove unwanted ChoiceGenerators that are registered - * while an existing ChoiceGenerator is being explored. Multiple ChoiceGenerators of the same - * type could be registered spuriously during a while(true) loop. + * Simple tool to log state changes. + * + * 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. */ public class StateReducer extends ListenerAdapter { + // Debug info fields private boolean debugMode; private boolean stateReductionMode; private final PrintWriter out; @@ -49,25 +56,48 @@ public class StateReducer extends ListenerAdapter { private int depth; private int id; private Transition transition; - private HashSet conflictSet; - private HashSet appSet; - // Holds the event value numbers that execute write instructions - private HashSet writeEventNumberSet; - // Holds values that have appeared during CG advances - private HashSet cgChoiceSet; + + // State reduction fields + private Integer[] choices; + private Integer[] refChoices; + private IntChoiceFromSet currCG; + private int choiceCounter; private Integer choiceUpperBound; + private Integer maxUpperBound; private boolean isInitialized; - private int currentChoice; - // Records how many times BooleanChoiceGenerator has been advanced - private int bCGIsAdvanced; - // Records how many times we have looped through all the event numbers (IntIntervalGenerator) - private int iiCGIsLooped; + private boolean isResetAfterAnalysis; + private boolean isBooleanCGFlipped; + private HashMap cgMap; + // Record the mapping between event number and field accesses (Read and Write) + private HashMap readWriteFieldsMap; + // The following is the backtrack map (set) that stores all the backtrack information + // e.g., event number 1 can have two backtrack sequences: {3,1,2,4,...} and {2,1,3,4,...} + private HashMap> backtrackMap; + // Stores explored backtrack lists in the form of HashSet of Strings + private HashSet backtrackSet; + private HashMap> conflictPairMap; - // Constants to determine when to start reducing states - private final int BOOLEAN_CG_ADVANCED_THRESHOLD = 2; - private final int INTEGER_CG_ADVANCED_THRESHOLD = 50; + // Map that represents graph G + // (i.e., visible operation dependency graph (VOD Graph) + private HashMap> vodGraphMap; + // Set that represents hash table H + // (i.e., hash table that records encountered states) + // VOD graph is updated when the state has not yet been seen + // Current state + private HashSet justVisitedStates; + // Previous choice number + private int prevChoiceValue; + // HashSet that stores references to unused CGs + private HashSet unusedCG; - public StateReducer (Config config) { + //private HashMap stateGraph; + private HashMap> stateToEventMap; + // Map state to event + // Visited states in the previous and current executions/traces for terminating condition + private HashSet prevVisitedStates; + private HashSet currVisitedStates; + + public StateReducer(Config config, JPF jpf) { debugMode = config.getBoolean("debug_state_transition", false); stateReductionMode = config.getBoolean("activate_state_reduction", true); if (debugMode) { @@ -79,29 +109,37 @@ public class StateReducer extends ListenerAdapter { depth = 0; id = 0; transition = null; - cgChoiceSet = new HashSet<>(); - choiceUpperBound = 0; - isInitialized = false; - conflictSet = new HashSet<>(); - String[] conflictVars = config.getStringArray("variables"); - // We are not tracking anything if it is null - if (conflictVars != null) { - for (String var : conflictVars) { - conflictSet.add(var); - } - } - appSet = new HashSet<>(); - String[] apps = config.getStringArray("apps"); - // We are not tracking anything if it is null - if (apps != null) { - for (String var : apps) { - appSet.add(var); - } + isBooleanCGFlipped = false; + vodGraphMap = new HashMap<>(); + justVisitedStates = new HashSet<>(); + prevChoiceValue = -1; + cgMap = new HashMap<>(); + readWriteFieldsMap = new HashMap<>(); + backtrackMap = new HashMap<>(); + backtrackSet = new HashSet<>(); + conflictPairMap = new HashMap<>(); + unusedCG = new HashSet<>(); + stateToEventMap = new HashMap<>(); + prevVisitedStates = new HashSet<>(); + currVisitedStates = new HashSet<>(); + initializeStateReduction(); + } + + private void initializeStateReduction() { + if (stateReductionMode) { + choices = null; + refChoices = null; + currCG = null; + choiceCounter = 0; + choiceUpperBound = 0; + maxUpperBound = 0; + isInitialized = false; + isResetAfterAnalysis = false; + cgMap.clear(); + resetReadWriteAnalysis(); + backtrackMap.clear(); + backtrackSet.clear(); } - currentChoice = 0; - writeEventNumberSet = new HashSet<>(); - bCGIsAdvanced = 0; - iiCGIsLooped = 0; } @Override @@ -124,60 +162,299 @@ public class StateReducer extends ListenerAdapter { } } + private void resetReadWriteAnalysis() { + // Reset the following data structure when the choice counter reaches 0 again + conflictPairMap.clear(); + readWriteFieldsMap.clear(); + } + + private IntChoiceFromSet setNewCG(IntChoiceFromSet icsCG) { + icsCG.setNewValues(choices); + icsCG.reset(); + // Use a modulo since choiceCounter is going to keep increasing + int choiceIndex = choiceCounter % choices.length; + icsCG.advance(choices[choiceIndex]); + if (choiceIndex == 0) { + resetReadWriteAnalysis(); + } + return icsCG; + } + + private Integer[] copyChoices(Integer[] choicesToCopy) { + + Integer[] copyOfChoices = new Integer[choicesToCopy.length]; + System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length); + return copyOfChoices; + } + + private void continueExecutingThisTrace(IntChoiceFromSet icsCG) { + // We repeat the same trace if a state match is not found yet + IntChoiceFromSet setCG = setNewCG(icsCG); + unusedCG.add(setCG); + } + + private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) { + if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) { + // Update the choices of the first CG and add '-1' + if (choices == null) { + // Initialize backtrack set that stores all the explored backtrack lists + maxUpperBound = cgChoices.length; + // All the choices are always the same so we only need to update it once + // Get the choice array and final choice in the array + choices = cgChoices; + // Make a copy of choices as reference + refChoices = copyChoices(choices); + String firstChoiceListString = buildStringFromChoiceList(choices); + backtrackSet.add(firstChoiceListString); + } + IntChoiceFromSet setCG = setNewCG(icsCG); + cgMap.put(setCG, refChoices[choiceCounter]); + } else { + continueExecutingThisTrace(icsCG); + } + } + + private void manageChoiceGeneratorsInSubsequentTraces(IntChoiceFromSet icsCG) { + // If this is the first iteration of the trace then set other CGs done + if (choiceCounter <= choiceUpperBound) { + icsCG.setDone(); + } else { + // If this is the subsequent iterations of the trace then set up new CGs to continue the execution + continueExecutingThisTrace(icsCG); + } + } + @Override - public void choiceGeneratorSet (VM vm, ChoiceGenerator newCG) { + public void choiceGeneratorRegistered(VM vm, ChoiceGenerator nextCG, ThreadInfo currentThread, Instruction executedInstruction) { if (stateReductionMode) { // Initialize with necessary information from the CG - if (newCG instanceof IntIntervalGenerator) { - IntIntervalGenerator iigCG = (IntIntervalGenerator) newCG; + if (nextCG instanceof IntChoiceFromSet) { + IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG; // Check if CG has been initialized, otherwise initialize it + Integer[] cgChoices = icsCG.getAllChoices(); if (!isInitialized) { - Integer[] choices = iigCG.getChoices(); // Get the upper bound from the last element of the choices - choiceUpperBound = choices[choices.length - 1]; + choiceUpperBound = cgChoices[cgChoices.length - 1]; isInitialized = true; + } + // Record the subsequent Integer CGs only until we hit the upper bound + if (!isResetAfterAnalysis) { + initializeChoiceGenerators(icsCG, cgChoices); + } else { + // Set new CGs to done so that the search algorithm explores the existing CGs + //icsCG.setDone(); + manageChoiceGeneratorsInSubsequentTraces(icsCG); + } + choiceCounter++; + } + } + } + + private void setDoneUnusedCG() { + // Set done every CG in the unused CG set + for (IntChoiceFromSet cg : unusedCG) { + cg.setDone(); + } + unusedCG.clear(); + } + + private void resetAllCGs() { + // Extract the event numbers that have backtrack lists + Set eventSet = backtrackMap.keySet(); + // Return if there is no conflict at all (highly unlikely) + if (eventSet.isEmpty()) { + // Set every CG to done! + for (IntChoiceFromSet cg : cgMap.keySet()) { + cg.setDone(); + } + return; + } + // Reset every CG with the first backtrack lists + for (IntChoiceFromSet cg : cgMap.keySet()) { + int event = cgMap.get(cg); + LinkedList choiceLists = backtrackMap.get(event); + if (choiceLists != null && choiceLists.peekFirst() != null) { + Integer[] choiceList = choiceLists.removeFirst(); + // Deploy the new choice list for this CG + cg.setNewValues(choiceList); + cg.reset(); + } else { + cg.setDone(); + } + } + setDoneUnusedCG(); + saveVisitedStates(); + } + + // Detect cycles in the current execution/trace + // We terminate the execution iff: + // (1) the state has been visited in the current execution + // (2) the state has one or more cycles that involve all the events + // With simple approach we only need to check for a re-visited state. + // Basically, we have to check that we have executed all events between two occurrences of such state. + private boolean containsCyclesWithAllEvents(int stId) { + + HashSet visitedEvents = stateToEventMap.get(stId); + boolean containsCyclesWithAllEvts = false; + if (checkIfAllEventsInvolved(visitedEvents)) { + containsCyclesWithAllEvts = true; + } + + return containsCyclesWithAllEvts; + } + + private boolean checkIfAllEventsInvolved(HashSet visitedEvents) { + + // Check if this set contains all the event choices + // If not then this is not the terminating condition + for(int i=0; i<=choiceUpperBound; i++) { + if (!visitedEvents.contains(i)) { + return false; + } + } + return true; + } + + private void saveVisitedStates() { + // CG is being reset + // Save all the visited states + prevVisitedStates.addAll(currVisitedStates); + currVisitedStates.clear(); + } + + private void updateChoicesForNewExecution(IntChoiceFromSet icsCG) { + if (choices == null || choices != icsCG.getAllChoices()) { + currCG = icsCG; + choices = icsCG.getAllChoices(); + refChoices = copyChoices(choices); + // Reset a few things for the sub-graph + resetReadWriteAnalysis(); + choiceCounter = 0; + } + } + + private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) { + // Traverse the sub-graphs + if (isResetAfterAnalysis) { + // Do this for every CG after finishing each backtrack list + // We try to update the CG with a backtrack list if the state has been visited multiple times + //if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) { + //if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) { + if (choiceCounter > 1 && cgMap.containsKey(icsCG)) { + int event = cgMap.get(icsCG); + LinkedList choiceLists = backtrackMap.get(event); + if (choiceLists != null && choiceLists.peekFirst() != null) { + Integer[] choiceList = choiceLists.removeFirst(); + // Deploy the new choice list for this CG + icsCG.setNewValues(choiceList); + icsCG.reset(); } else { - newCG.setDone(); + // Set done if this was the last backtrack list + icsCG.setDone(); } + setDoneUnusedCG(); + saveVisitedStates(); + } + } else { + // Update and reset the CG if needed (do this for the first time after the analysis) + // Start backtracking if this is a visited state and it is not a repeating state + resetAllCGs(); + isResetAfterAnalysis = true; + } + } + + private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) { + // Check the next choice and if the value is not the same as the expected then force the expected value + int choiceIndex = (choiceCounter - 1) % refChoices.length; + if (choices[choiceIndex] != icsCG.getNextChoiceIndex()) { + int expectedChoice = refChoices[choiceIndex]; + int currCGIndex = icsCG.getNextChoiceIndex(); + if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) { + icsCG.setChoice(currCGIndex, expectedChoice); } } } + private boolean terminateCurrentExecution() { + // We need to check all the states that have just been visited + // Often a transition (choice/event) can result into forwarding/backtracking to a number of states + for(Integer stateId : justVisitedStates) { + if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) { + return true; + } + } + return false; + } + @Override - public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator currentCG) { + public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { + if (stateReductionMode) { - // Check for BooleanChoiceGenerator + // Check the boolean CG and if it is flipped, we are resetting the analysis if (currentCG instanceof BooleanChoiceGenerator) { - bCGIsAdvanced++; + if (!isBooleanCGFlipped) { + isBooleanCGFlipped = true; + } else { + initializeStateReduction(); + } } // Check every choice generated and make sure that all the available choices // are chosen first before repeating the same choice of value twice! - if (currentCG instanceof IntIntervalGenerator) { - IntIntervalGenerator iigCG = (IntIntervalGenerator) currentCG; - Integer nextChoice = iigCG.getNextChoice(); - if (!cgChoiceSet.contains(nextChoice)) { - cgChoiceSet.add(nextChoice); - } - // Allow reinitialization after an upper bound is hit - // This means all available choices have been explored once during this iteration - if (cgChoiceSet.contains(choiceUpperBound)) { - isInitialized = false; - cgChoiceSet.clear(); - iiCGIsLooped++; - } - // Record the current choice - currentChoice = iigCG.getNextChoice(); - // Start reducing (advancing) if the thresholds are passed - if (iiCGIsLooped >= INTEGER_CG_ADVANCED_THRESHOLD && - bCGIsAdvanced >= BOOLEAN_CG_ADVANCED_THRESHOLD) { - if (!writeEventNumberSet.contains(currentChoice)) { - iigCG.advance(); - } + if (currentCG instanceof IntChoiceFromSet) { + IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; + // Update the current pointer to the current set of choices + updateChoicesForNewExecution(icsCG); + // Check if we have seen this state or this state contains cycles that involve all events + if (terminateCurrentExecution()) { + exploreNextBacktrackSets(icsCG); } + justVisitedStates.clear(); + // If we don't see a fair scheduling of events/choices then we have to enforce it + checkAndEnforceFairScheduling(icsCG); + // Update the VOD graph always with the latest + updateVODGraph(icsCG.getNextChoice()); } } } + 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; + } + + private void mapStateToEvent(Search search, int stateId) { + // Insert state ID and event choice into the map + HashSet eventSet; + if (stateToEventMap.containsKey(stateId)) { + eventSet = stateToEventMap.get(stateId); + } else { + eventSet = new HashSet<>(); + stateToEventMap.put(stateId, eventSet); + } + eventSet.add(prevChoiceValue); + } + + private void updateStateInfo(Search search) { + if (stateReductionMode) { + // Update the state variables + // Line 19 in the paper page 11 (see the heading note above) + int stateId = search.getStateId(); + currVisitedStates.add(stateId); + mapStateToEvent(search, stateId); + justVisitedStates.add(stateId); + } + } + @Override public void stateAdvanced(Search search) { if (debugMode) { @@ -197,6 +474,7 @@ public class StateReducer extends ListenerAdapter { out.println("\n==> DEBUG: The state is forwarded to state with id: " + id + " with depth: " + depth + " which is " + detail + " Transition: " + transition + "\n"); } + updateStateInfo(search); } @Override @@ -210,6 +488,7 @@ public class StateReducer extends ListenerAdapter { out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition + " and depth: " + depth + "\n"); } + updateStateInfo(search); } @Override @@ -219,47 +498,306 @@ public class StateReducer extends ListenerAdapter { } } - @Override - public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { - // CASE #1: Detecting variable write-after-write conflict + // 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 + private class ReadWriteSet { + private HashMap readSet; + private HashMap writeSet; + + public ReadWriteSet() { + readSet = new HashMap<>(); + writeSet = new HashMap<>(); + } + + public void addReadField(String field, int objectId) { + readSet.put(field, objectId); + } + + public void addWriteField(String field, int objectId) { + writeSet.put(field, objectId); + } + + public boolean readFieldExists(String field) { + return readSet.containsKey(field); + } + + public boolean writeFieldExists(String field) { + return writeSet.containsKey(field); + } + + public int readFieldObjectId(String field) { + return readSet.get(field); + } + + public int writeFieldObjectId(String field) { + return writeSet.get(field); + } + } + + private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) { + // Do the analysis to get Read and Write accesses to fields + ReadWriteSet rwSet; + // We already have an entry + if (readWriteFieldsMap.containsKey(refChoices[currentChoice])) { + rwSet = readWriteFieldsMap.get(refChoices[currentChoice]); + } else { // We need to create a new entry + rwSet = new ReadWriteSet(); + readWriteFieldsMap.put(refChoices[currentChoice], rwSet); + } + int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef(); + // Record the field in the map if (executedInsn instanceof WriteInstruction) { - // Check for write-after-write conflict - String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName(); - for(String var : conflictSet) { - if (varId.contains(var)) { - String writer = getWriter(ti.getStack()); - // Just return if the writer is not one of the listed apps in the .jpf file - if (writer == null) - return; - - // Stores event number that executes WriteInstruction - if (!writeEventNumberSet.contains(currentChoice)) { - writeEventNumberSet.add(currentChoice); + // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes + for (String str : EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) { + if (fieldClass.startsWith(str)) { + return; + } + } + rwSet.addWriteField(fieldClass, objectId); + } else if (executedInsn instanceof ReadInstruction) { + rwSet.addReadField(fieldClass, objectId); + } + } + + private boolean recordConflictPair(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 service 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 String buildStringFromChoiceList(Integer[] newChoiceList) { + + // When we see a choice list shorter than the upper bound, e.g., [3,2] for choices 0,1,2, and 3, + // then we have to pad the beginning before we store it, because [3,2] actually means [0,1,3,2] + // First, calculate the difference between this choice list and the upper bound + // The actual list doesn't include '-1' at the end + int actualListLength = newChoiceList.length - 1; + int diff = maxUpperBound - actualListLength; + StringBuilder sb = new StringBuilder(); + // Pad the beginning if necessary + for (int i = 0; i < diff; i++) { + sb.append(i); + } + // Then continue with the actual choice list + // We don't include the '-1' at the end + for (int i = 0; i < newChoiceList.length - 1; i++) { + sb.append(newChoiceList[i]); + } + return sb.toString(); + } + + private void checkAndAddBacktrackList(LinkedList backtrackChoiceLists, Integer[] newChoiceList) { + + String newChoiceListString = buildStringFromChoiceList(newChoiceList); + // Add only if we haven't seen this combination before + if (!backtrackSet.contains(newChoiceListString)) { + backtrackSet.add(newChoiceListString); + backtrackChoiceLists.addLast(newChoiceList); + } + } + + private void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) { + + LinkedList backtrackChoiceLists; + // Create a new list of choices for backtrack based on the current choice and conflicting event number + // If we have a conflict between 1 and 3, then we create the list {3, 1, 2, 4, 5} for backtrack + // The backtrack point is the CG for event number 1 and the list length is one less than the original list + // (originally of length 6) since we don't start from event number 0 + if (!isResetAfterAnalysis) { + // Check if we have a list for this choice number + // If not we create a new one for it + if (!backtrackMap.containsKey(conflictEventNumber)) { + backtrackChoiceLists = new LinkedList<>(); + backtrackMap.put(conflictEventNumber, backtrackChoiceLists); + } else { + backtrackChoiceLists = backtrackMap.get(conflictEventNumber); + } + int maxListLength = choiceUpperBound + 1; + int listLength = maxListLength - conflictEventNumber; + Integer[] newChoiceList = new Integer[listLength]; + // Put the conflicting event numbers first and reverse the order + newChoiceList[0] = refChoices[currentChoice]; + newChoiceList[1] = refChoices[conflictEventNumber]; + // Put the rest of the event numbers into the array starting from the minimum to the upper bound + for (int i = conflictEventNumber + 1, j = 2; j < listLength; i++) { + if (refChoices[i] != refChoices[currentChoice]) { + newChoiceList[j] = refChoices[i]; + j++; + } + } + checkAndAddBacktrackList(backtrackChoiceLists, newChoiceList); + // The start index for the recursion is always 1 (from the main branch) + } else { // This is a sub-graph + // There is a case/bug that after a re-initialization, currCG is not yet initialized + if (currCG != null && cgMap.containsKey(currCG)) { + int backtrackListIndex = cgMap.get(currCG); + backtrackChoiceLists = backtrackMap.get(backtrackListIndex); + int listLength = refChoices.length; + Integer[] newChoiceList = new Integer[listLength]; + // Copy everything before the conflict number + for (int i = 0; i < conflictEventNumber; i++) { + newChoiceList[i] = refChoices[i]; + } + // Put the conflicting events + newChoiceList[conflictEventNumber] = refChoices[currentChoice]; + newChoiceList[conflictEventNumber + 1] = refChoices[conflictEventNumber]; + // Copy the rest + for (int i = conflictEventNumber + 1, j = conflictEventNumber + 2; j < listLength - 1; i++) { + if (refChoices[i] != refChoices[currentChoice]) { + newChoiceList[j] = refChoices[i]; + j++; } } + checkAndAddBacktrackList(backtrackChoiceLists, newChoiceList); + } + } + } + + // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure + private final static String[] EXCLUDED_FIELDS_STARTS_WITH_LIST = + // Java and Groovy libraries + { "java", "org", "sun", "com", "gov", "groovy"}; + private final static String[] EXCLUDED_FIELDS_ENDS_WITH_LIST = + // Groovy library created fields + {"stMC", "callSiteArray", "metaClass", "staticClassInfo", "__constructor__", + // Infrastructure + "sendEvent", "Object", "reference", "location", "app", "state", "log", "functionList", "objectList", + "eventList", "valueList", "settings", "printToConsole", "app1", "app2"}; + private final static String[] EXCLUDED_FIELDS_CONTAINS_LIST = {"_closure"}; + private final static String[] EXCLUDED_FIELDS_WRITE_INSTRUCTIONS_STARTS_WITH_LIST = {"Event"}; + + private boolean isFieldExcluded(String field) { + // Check against "starts-with" list + for(String str : EXCLUDED_FIELDS_STARTS_WITH_LIST) { + if (field.startsWith(str)) { + return true; + } + } + // Check against "ends-with" list + for(String str : EXCLUDED_FIELDS_ENDS_WITH_LIST) { + if (field.endsWith(str)) { + return true; + } + } + // Check against "contains" list + for(String str : EXCLUDED_FIELDS_CONTAINS_LIST) { + if (field.contains(str)) { + return true; } } + + return false; } - // Find the variable writer - // It should be one of the apps listed in the .jpf file - private String getWriter(List sfList) { - // Start looking from the top of the stack backward - for(int i=sfList.size()-1; i>=0; i--) { - MethodInfo mi = sfList.get(i).getMethodInfo(); - if(!mi.isJPFInternal()) { - String method = mi.getStackTraceName(); - // Check against the apps in the appSet - for(String app : appSet) { - // There is only one writer at a time but we need to always - // check all the potential writers in the list - if (method.contains(app)) { - return app; + // This method checks whether a choice is reachable in the VOD graph from a reference choice + // This is a BFS search + private boolean isReachableInVODGraph(int checkedChoice, int referenceChoice) { + // Record visited choices as we search in the graph + HashSet visitedChoice = new HashSet<>(); + visitedChoice.add(referenceChoice); + 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(referenceChoice)) { + nodesToVisit.addAll(vodGraphMap.get(referenceChoice)); + while(!nodesToVisit.isEmpty()) { + int currChoice = nodesToVisit.getFirst(); + if (currChoice == checkedChoice) { + return true; + } + if (visitedChoice.contains(currChoice)) { + // If there is a loop then we don't find it + return false; + } + // Continue searching + visitedChoice.add(currChoice); + HashSet currChoiceNextNodes = vodGraphMap.get(currChoice); + if (currChoiceNextNodes != null) { + // Add only if there is a mapping for next nodes + for (Integer nextNode : currChoiceNextNodes) { + // Skip cycles + if (nextNode == currChoice) { + continue; + } + nodesToVisit.addLast(nextNode); } } } } + return false; + } - return null; + @Override + public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { + if (stateReductionMode) { + if (isInitialized) { + int currentChoice = (choiceCounter % refChoices.length) - 1; + if (currentChoice < 0) { + // We do not compute the conflicts for the choice '-1' + return; + } + // 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); + } + } + // Analyze conflicts from next instructions + if (nextInsn instanceof JVMFieldInstruction) { + // The constructor is only called once when the object is initialized + // It does not have shared access with other objects + MethodInfo mi = nextInsn.getMethodInfo(); + if (!mi.getName().equals("")) { + String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); + // We don't care about libraries + if (!isFieldExcluded(fieldClass)) { + // Check for conflict (go backward from currentChoice and get the first conflict) + // If the current event has conflicts with multiple events, then these will be detected + // one by one as this recursively checks backward when backtrack set is revisited and executed. + for (int eventNumber = currentChoice - 1; eventNumber >= 0; eventNumber--) { + // Skip if this event number does not have any Read/Write set + if (!readWriteFieldsMap.containsKey(refChoices[eventNumber])) { + continue; + } + ReadWriteSet rwSet = readWriteFieldsMap.get(refChoices[eventNumber]); + int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef(); + // 1) 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)) { + // We do not record and service the same backtrack pair/point twice! + // If it has been serviced before, we just skip this + if (recordConflictPair(currentChoice, eventNumber)) { + // 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); + // Break if a conflict is found! + break; + } + } + } + } + } + } + } + } + } } -} \ No newline at end of file +}