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=8aa2c381c636597093e286a53480af3045af30bb;hp=67446f323faf1e6d4c6aaecc5128d6feabe9299f;hb=76bdd87b5c4d921fc9949c225bb1dd22e70d7dfa;hpb=1418a055d0a3e09ae21b101195659f04be39c882 diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 67446f3..8aa2c38 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -17,6 +17,7 @@ */ package gov.nasa.jpf.listener; +import com.sun.org.apache.xpath.internal.operations.Bool; import gov.nasa.jpf.Config; import gov.nasa.jpf.JPF; import gov.nasa.jpf.ListenerAdapter; @@ -27,47 +28,46 @@ 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.IntChoiceFromSet; import gov.nasa.jpf.vm.choice.IntIntervalGenerator; +import java.awt.*; import java.io.PrintWriter; import java.util.*; +import java.util.List; // 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 */ public class StateReducer extends ListenerAdapter { + // Debug info fields private boolean debugMode; private boolean stateReductionMode; private final PrintWriter out; - private String detail; - 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; + volatile private String detail; + volatile private int depth; + volatile private int id; + Transition transition; + + // State reduction fields + private int choiceCounter; private Integer choiceUpperBound; 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; - - // Constants to determine when to start reducing states - private final int BOOLEAN_CG_ADVANCED_THRESHOLD = 2; - private final int INTEGER_CG_ADVANCED_THRESHOLD = 50; + 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; + private HashMap> conflictPairMap; - public StateReducer (Config config) { + public StateReducer (Config config, JPF jpf) { debugMode = config.getBoolean("debug_state_transition", false); stateReductionMode = config.getBoolean("activate_state_reduction", true); if (debugMode) { @@ -79,29 +79,21 @@ 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; + initializeStateReduction(); + } + + private void initializeStateReduction() { + if (stateReductionMode) { + choiceCounter = 0; + choiceUpperBound = 0; + isInitialized = false; + isResetAfterAnalysis = false; + cgMap = new HashMap<>(); + readWriteFieldsMap = new HashMap<>(); + backtrackMap = new HashMap<>(); + conflictPairMap = new HashMap<>(); } - currentChoice = 0; - writeEventNumberSet = new HashSet<>(); - bCGIsAdvanced = 0; - iiCGIsLooped = 0; } @Override @@ -125,53 +117,93 @@ public class StateReducer extends ListenerAdapter { } @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 + Object[] choices = 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 = (Integer) choices[choices.length - 1]; isInitialized = true; + } + // Record the subsequent Integer CGs only until we hit the upper bound + if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) { + // Update the choices of the first CG and add '-1' + Integer[] newChoices = new Integer[choices.length + 1]; + System.arraycopy(choices, 0, newChoices, 0, choices.length); + newChoices[newChoices.length - 1] = -1; + icsCG.setNewValues(newChoices); + icsCG.reset(); + // Advance the current Integer CG + // This way we explore all the event numbers in the first pass + icsCG.advance(choiceCounter); + cgMap.put(icsCG, choiceCounter); + choiceCounter++; } else { - newCG.setDone(); + // Set done the subsequent CGs + // We only need n CGs (n is event numbers) + icsCG.setDone(); } } } } + 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()) { + 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(); + } + } + } + @Override public void choiceGeneratorAdvanced (VM vm, ChoiceGenerator currentCG) { - if (stateReductionMode) { - // Check for BooleanChoiceGenerator + + if(stateReductionMode) { + // 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++; + if (currentCG instanceof IntChoiceFromSet) { + IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; + // Update and reset the CG if needed (do this for the first time after the analysis) + if (!isResetAfterAnalysis && icsCG.getNextChoice() == -1) { + resetAllCGs(); + isResetAfterAnalysis = true; } - // 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(); + // Do this for every CG after finishing each backtrack list + if (isResetAfterAnalysis && icsCG.getNextChoice() == -1) { + int event = cgMap.get(icsCG); + LinkedList choiceLists = backtrackMap.get(event); + if (choiceLists.peekFirst() != null) { + Integer[] choiceList = choiceLists.removeFirst(); + // Deploy the new choice list for this CG + icsCG.setNewValues(choiceList); + icsCG.reset(); + } else { + // Set done if this was the last backtrack list + icsCG.setDone(); } } } @@ -219,47 +251,189 @@ 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(currentChoice)) { + rwSet = readWriteFieldsMap.get(currentChoice); + } else { // We need to create a new entry + rwSet = new ReadWriteSet(); + readWriteFieldsMap.put(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; + rwSet.addWriteField(fieldClass, objectId); + } else if (executedInsn instanceof ReadInstruction) { + rwSet.addReadField(fieldClass, objectId); + } + } - // Stores event number that executes WriteInstruction - if (!writeEventNumberSet.contains(currentChoice)) { - writeEventNumberSet.add(currentChoice); - } - } + 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 void createBacktrackChoiceList(int currentChoice, int conflictEventNumber) { + + int minChoice = Math.min(currentChoice, conflictEventNumber); + int maxChoice = Math.max(currentChoice, conflictEventNumber); + LinkedList backtrackChoiceLists; + // Check if we have a list for this choice number + // If not we create a new one for it + if (!backtrackMap.containsKey(minChoice)) { + backtrackChoiceLists = new LinkedList<>(); + backtrackMap.put(minChoice, backtrackChoiceLists); + } else { + backtrackChoiceLists = backtrackMap.get(minChoice); + } + // TODO: The following might change depending on the POR implementation detail + // 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 + int maxListLength = choiceUpperBound + 1; + int listLength = maxListLength - minChoice; + Integer[] choiceList = new Integer[listLength+1]; + // Put the conflicting event numbers first and reverse the order + choiceList[0] = maxChoice; + choiceList[1] = minChoice; + // Put the rest of the event numbers into the array starting from the minimum to the upper bound + for(int i = minChoice + 1, j = 2; j < listLength; i++) { + if (i != maxChoice) { + choiceList[j] = i; + j++; } } + // Set the last element to '-1' as the end of the sequence + choiceList[choiceList.length - 1] = -1; + backtrackChoiceLists.addLast(choiceList); } - // 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; + @Override + public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { + if (stateReductionMode) { + if (isInitialized) { + int currentChoice = choiceCounter - 1; + // 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 (!fieldClass.startsWith("java") && + !fieldClass.startsWith("org") && + !fieldClass.startsWith("sun") && + !fieldClass.startsWith("com") && + !fieldClass.startsWith("gov") && + !fieldClass.startsWith("groovy") && + // and fields generated for the Groovy library + !fieldClass.endsWith("stMC") && + !fieldClass.endsWith("callSiteArray") && + !fieldClass.endsWith("metaClass") && + !fieldClass.endsWith("staticClassInfo") && + !fieldClass.endsWith("__constructor__")) { + 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 (!fieldClass.startsWith("java") && + !fieldClass.startsWith("org") && + !fieldClass.startsWith("sun") && + !fieldClass.startsWith("com") && + !fieldClass.startsWith("gov") && + !fieldClass.startsWith("groovy") && + // and fields generated for the Groovy library + !fieldClass.endsWith("stMC") && + !fieldClass.endsWith("callSiteArray") && + !fieldClass.endsWith("metaClass") && + !fieldClass.endsWith("staticClassInfo") && + !fieldClass.endsWith("__constructor__")) { + // 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(eventNumber)) { + continue; + } + ReadWriteSet rwSet = readWriteFieldsMap.get(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)) { + createBacktrackChoiceList(currentChoice, eventNumber); + // Break if a conflict is found! + break; + } + } + } + } } } } } - - return null; } } \ No newline at end of file