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=0da718cb6e43f787387ddbd99b0fe446248dc955;hp=823bd525491681dca1f469204423ca44ccf92f7a;hb=332b6623f6b5d4cd9119c61352c804ef78870889;hpb=bd5eee6485e94af774e8db1d6ae20748391aaca2 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 823bd52..0da718c 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -59,24 +59,26 @@ public class DPORStateReducer extends ListenerAdapter { private int choiceCounter; private int maxEventChoice; // Data structure to track the events seen by each state to track cycles (containing all events) for termination - 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 + private HashSet justVisitedStates; // States just visited in the previous choice/event + private HashSet prevVisitedStates; // States visited in the previous execution + private HashSet nonRelevantClasses;// Class info objects of non-relevant classes + private HashSet nonRelevantFields; // Field info objects of non-relevant fields + private HashSet relevantFields; // Field info objects of relevant fields private HashMap> stateToEventMap; // Data structure to analyze field Read/Write accesses and conflicts private HashMap> backtrackMap; // Track created backtracking points private PriorityQueue backtrackStateQ; // Heap that returns the latest state private Execution currentExecution; // Holds the information about the current execution - private HashSet doneBacktrackSet; // Record state ID and trace already constructed + private HashMap> doneBacktrackMap; // Record state ID and trace already constructed private HashMap restorableStateMap; // Maps state IDs to the restorable state object - private ReachabilityGraph rGraph; // Reachability graph for past executions + private RGraph rGraph; // R-Graph for past executions // Boolean states private boolean isBooleanCGFlipped; private boolean isEndOfExecution; // Statistics - private int numOfConflicts; private int numOfTransitions; public DPORStateReducer(Config config, JPF jpf) { @@ -95,8 +97,10 @@ public class DPORStateReducer extends ListenerAdapter { } } isBooleanCGFlipped = false; - numOfConflicts = 0; numOfTransitions = 0; + nonRelevantClasses = new HashSet<>(); + nonRelevantFields = new HashSet<>(); + relevantFields = new HashSet<>(); restorableStateMap = new HashMap<>(); initializeStatesVariables(); } @@ -164,19 +168,13 @@ public class DPORStateReducer extends ListenerAdapter { @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(); @@ -189,6 +187,8 @@ public class DPORStateReducer extends ListenerAdapter { // Initialize with necessary information from the CG if (nextCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG; + // Tell JPF that we are performing DPOR + icsCG.setDpor(); if (!isEndOfExecution) { // Check if CG has been initialized, otherwise initialize it Integer[] cgChoices = icsCG.getAllChoices(); @@ -215,15 +215,12 @@ public class DPORStateReducer extends ListenerAdapter { @Override public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { - if (stateReductionMode) { // Check the boolean CG and if it is flipped, we are resetting the analysis if (currentCG instanceof BooleanChoiceGenerator) { 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(); } @@ -269,11 +266,9 @@ public class DPORStateReducer extends ListenerAdapter { currentChoice = checkAndAdjustChoice(currentChoice, vm); // Record accesses from executed instructions if (executedInsn instanceof JVMFieldInstruction) { - // Analyze only after being initialized - String fieldClass = ((JVMFieldInstruction) executedInsn).getFieldInfo().getFullName(); // We don't care about libraries - if (!isFieldExcluded(fieldClass)) { - analyzeReadWriteAccesses(executedInsn, fieldClass, currentChoice); + if (!isFieldExcluded(executedInsn)) { + analyzeReadWriteAccesses(executedInsn, currentChoice); } } else if (executedInsn instanceof INVOKEINTERFACE) { // Handle the read/write accesses that occur through iterators @@ -310,7 +305,7 @@ public class DPORStateReducer extends ListenerAdapter { } } - // This class stores a representation of the execution graph node + // This class stores a representation of an execution // TODO: We can modify this class to implement some optimization (e.g., clock-vector) // TODO: We basically need to keep track of: // TODO: (1) last read/write access to each memory location @@ -320,14 +315,12 @@ public class DPORStateReducer extends ListenerAdapter { private ArrayList executionTrace; // The BacktrackPoint objects of this execution private boolean isNew; // Track if this is the first time it is accessed private HashMap readWriteFieldsMap; // Record fields that are accessed - private HashMap stateToTransitionMap; // For O(1) access to backtrack point public Execution() { cgToChoiceMap = new HashMap<>(); executionTrace = new ArrayList<>(); isNew = true; readWriteFieldsMap = new HashMap<>(); - stateToTransitionMap = new HashMap<>(); } public void addTransition(TransitionEvent newBacktrackPoint) { @@ -350,16 +343,12 @@ public class DPORStateReducer extends ListenerAdapter { return executionTrace.get(0); } - public HashMap getReadWriteFieldsMap() { - return readWriteFieldsMap; + public TransitionEvent getLastTransition() { + return executionTrace.get(executionTrace.size() - 1); } - public TransitionEvent getTransitionFromState(int stateId) { - if (stateToTransitionMap.containsKey(stateId)) { - return stateToTransitionMap.get(stateId); - } - // Return the latest transition for unseen states (that have just been encountered in this transition) - return executionTrace.get(executionTrace.size() - 1); + public HashMap getReadWriteFieldsMap() { + return readWriteFieldsMap; } public boolean isNew() { @@ -374,10 +363,6 @@ public class DPORStateReducer extends ListenerAdapter { public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) { cgToChoiceMap.put(icsCG, choice); } - - public void mapStateToTransition(int stateId, TransitionEvent backtrackPoint) { - stateToTransitionMap.put(stateId, backtrackPoint); - } } // This class compactly stores a predecessor @@ -401,12 +386,13 @@ public class DPORStateReducer extends ListenerAdapter { } } - // This class represents a Reachability Graph - private class ReachabilityGraph { + // This class represents a R-Graph (in the paper it is a state transition graph R) + // This implementation stores reachable transitions from and connects with past executions + private class RGraph { private int hiStateId; // Maximum state Id - private HashMap> graph; // Reachability graph for past executions + private HashMap> graph; // Reachable transitions from past executions - public ReachabilityGraph() { + public RGraph() { hiStateId = 0; graph = new HashMap<>(); } @@ -430,6 +416,12 @@ public class DPORStateReducer extends ListenerAdapter { } public HashSet getReachableTransitionsAtState(int stateId) { + if (!graph.containsKey(stateId)) { + // This is a loop from a transition to itself, so just return the current transition + HashSet transitionSet = new HashSet<>(); + transitionSet.add(currentExecution.getLastTransition()); + return transitionSet; + } return graph.get(stateId); } @@ -437,7 +429,11 @@ public class DPORStateReducer extends ListenerAdapter { HashSet reachableTransitions = new HashSet<>(); // All transitions from states higher than the given state ID (until the highest state ID) are reachable for(int stId = stateId; stId <= hiStateId; stId++) { - reachableTransitions.addAll(graph.get(stId)); + // We might encounter state IDs from the first round of Boolean CG + // The second round of Boolean CG should consider these new states + if (graph.containsKey(stId)) { + reachableTransitions.addAll(graph.get(stId)); + } } return reachableTransitions; } @@ -524,7 +520,7 @@ public class DPORStateReducer extends ListenerAdapter { } } - // This class compactly stores backtrack points: + // This class compactly stores transitions: // 1) CG, // 2) state ID, // 3) choice, @@ -639,14 +635,16 @@ public class DPORStateReducer extends ListenerAdapter { // Get state ID and associate it with this transition int stateId = vm.getStateId(); TransitionEvent transition = setupTransition(icsCG, stateId, choiceIndex); - // Add new transition to the current execution + // Add new transition to the current execution and map it in R-Graph for (Integer stId : justVisitedStates) { // Map this transition to all the previously passed states - currentExecution.mapStateToTransition(stId, transition); + rGraph.addReachableTransition(stId, transition); } currentExecution.mapCGToChoice(icsCG, choiceCounter); // Store restorable state object for this state (always store the latest) - RestorableVMState restorableState = vm.getRestorableState(); - restorableStateMap.put(stateId, restorableState); + if (!restorableStateMap.containsKey(stateId)) { + RestorableVMState restorableState = vm.getRestorableState(); + restorableStateMap.put(stateId, restorableState); + } } private TransitionEvent setupTransition(IntChoiceFromSet icsCG, int stateId, int choiceIndex) { @@ -665,10 +663,6 @@ public class DPORStateReducer extends ListenerAdapter { transition.setStateId(stateId); transition.setChoice(refChoices[choiceIndex]); transition.setChoiceCounter(choiceCounter); - // Add transition into R-Graph - for (Integer stId : justVisitedStates) { - rGraph.addReachableTransition(stId, transition); - } return transition; } @@ -682,7 +676,6 @@ public class DPORStateReducer extends ListenerAdapter { // 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 completeFullCycle(int stId) { - // False if the state ID hasn't been recorded if (!stateToEventMap.containsKey(stId)) { return false; @@ -714,8 +707,8 @@ public class DPORStateReducer extends ListenerAdapter { backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); currentExecution = new Execution(); currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point - doneBacktrackSet = new HashSet<>(); - rGraph = new ReachabilityGraph(); + doneBacktrackMap = new HashMap<>(); + rGraph = new RGraph(); // Booleans isEndOfExecution = false; } @@ -743,7 +736,6 @@ public class DPORStateReducer extends ListenerAdapter { private void updateStateInfo(Search search) { // Update the state variables - // Line 19 in the paper page 11 (see the heading note above) int stateId = search.getStateId(); // Insert state ID into the map if it is new if (!stateToEventMap.containsKey(stateId)) { @@ -780,17 +772,28 @@ public class DPORStateReducer extends ListenerAdapter { } // Analyze Read/Write accesses that are directly invoked on fields - private void analyzeReadWriteAccesses(Instruction executedInsn, String fieldClass, int currentChoice) { + private void analyzeReadWriteAccesses(Instruction executedInsn, int currentChoice) { + // Get the field info + FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo(); + // Analyze only after being initialized + String fieldClass = fieldInfo.getFullName(); // Do the analysis to get Read and Write accesses to fields ReadWriteSet rwSet = getReadWriteSet(currentChoice); - int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef(); + int objectId = fieldInfo.getClassInfo().getClassObjectRef(); // Record the field in the map if (executedInsn instanceof WriteInstruction) { - // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes - for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) { - if (fieldClass.startsWith(str)) { - return; + // We first check the non-relevant fields set + if (!nonRelevantFields.contains(fieldInfo)) { + // Exclude certain field writes because of infrastructure needs, e.g., Event class field writes + for (String str : EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST) { + if (fieldClass.startsWith(str)) { + nonRelevantFields.add(fieldInfo); + return; + } } + } else { + // If we have this field in the non-relevant fields set then we return right away + return; } rwSet.addWriteField(fieldClass, objectId); } else if (executedInsn instanceof ReadInstruction) { @@ -819,9 +822,17 @@ public class DPORStateReducer extends ListenerAdapter { 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) || - excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName)) { + ClassInfo classInfo = eiAccessObj.getClassInfo(); + String objClassName = classInfo.getName(); + // Check if this class info is part of the non-relevant classes set already + if (!nonRelevantClasses.contains(classInfo)) { + if (excludeThisForItStartsWith(EXCLUDED_FIELDS_READ_WRITE_INSTRUCTIONS_STARTS_WITH_LIST, objClassName) || + excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName)) { + nonRelevantClasses.add(classInfo); + return; + } + } else { + // If it is part of the non-relevant classes set then return immediately return; } // Extract fields from this object and put them into the read write @@ -942,21 +953,21 @@ public class DPORStateReducer extends ListenerAdapter { private boolean isConflictFound(Execution execution, int reachableChoice, Execution conflictExecution, int conflictChoice, ReadWriteSet currRWSet) { ArrayList executionTrace = execution.getExecutionTrace(); - HashMap execRWFieldsMap = execution.getReadWriteFieldsMap(); ArrayList conflictTrace = conflictExecution.getExecutionTrace(); + HashMap confRWFieldsMap = conflictExecution.getReadWriteFieldsMap(); // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) - if (!execRWFieldsMap.containsKey(conflictChoice) || + if (!confRWFieldsMap.containsKey(conflictChoice) || executionTrace.get(reachableChoice).getChoice() == conflictTrace.get(conflictChoice).getChoice()) { return false; } // R/W set of choice/event that may have a potential conflict - ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice); + ReadWriteSet confRWSet = confRWFieldsMap.get(conflictChoice); // 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)) { + if ((confRWSet.readFieldExists(writeField) && confRWSet.readFieldObjectId(writeField) == currObjId) || + (confRWSet.writeFieldExists(writeField) && confRWSet.writeFieldObjectId(writeField) == currObjId)) { // Remove this from the write set as we are tracking per memory location currRWSet.removeWriteField(writeField); return true; @@ -966,7 +977,7 @@ public class DPORStateReducer extends ListenerAdapter { Set currReadSet = currRWSet.getReadSet(); for(String readField : currReadSet) { int currObjId = currRWSet.readFieldObjectId(readField); - if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) { + if (confRWSet.writeFieldExists(readField) && confRWSet.writeFieldObjectId(readField) == currObjId) { // Remove this from the read set as we are tracking per memory location currRWSet.removeReadField(readField); return true; @@ -990,33 +1001,47 @@ public class DPORStateReducer extends ListenerAdapter { return rwSet; } - private boolean isFieldExcluded(String field) { + private boolean isFieldExcluded(Instruction executedInsn) { + // Get the field info + FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo(); + // Check if the non-relevant fields set already has it + if (nonRelevantFields.contains(fieldInfo)) { + return true; + } + // Check if the relevant fields set already has it + if (relevantFields.contains(fieldInfo)) { + return false; + } + // Analyze only after being initialized + String field = fieldInfo.getFullName(); // Check against "starts-with", "ends-with", and "contains" list if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) || excludeThisForItEndsWith(EXCLUDED_FIELDS_ENDS_WITH_LIST, field) || excludeThisForItContains(EXCLUDED_FIELDS_CONTAINS_LIST, field)) { + nonRelevantFields.add(fieldInfo); return true; } - + relevantFields.add(fieldInfo); return false; } // Check if this trace is already constructed 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 - // another trace that starts with event 1 at state 1, e.g., the trace 1:13024 - // The second time this event 1 is explored, it will generate the same state as the first one - StringBuilder sb = new StringBuilder(); - sb.append(stateId); - sb.append(':'); - sb.append(firstChoice); // Check if the trace has been constructed as a backtrack point for this state - if (doneBacktrackSet.contains(sb.toString())) { - return true; + // TODO: THIS IS AN OPTIMIZATION! + HashSet choiceSet; + if (doneBacktrackMap.containsKey(stateId)) { + choiceSet = doneBacktrackMap.get(stateId); + if (choiceSet.contains(firstChoice)) { + return true; + } + } else { + choiceSet = new HashSet<>(); + doneBacktrackMap.put(stateId, choiceSet); } - doneBacktrackSet.add(sb.toString()); + choiceSet.add(firstChoice); + return false; } @@ -1060,8 +1085,6 @@ public class DPORStateReducer extends ListenerAdapter { // 1) recursively, and // 2) track accesses per memory location (per shared variable/field) private void updateBacktrackSet(Execution execution, int currentChoice) { - // Choice/event we want to check for conflict against (start from actual choice) - int conflictChoice = currentChoice; // Copy ReadWriteSet object HashMap currRWFieldsMap = execution.getReadWriteFieldsMap(); ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice); @@ -1072,11 +1095,13 @@ public class DPORStateReducer extends ListenerAdapter { // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle HashSet visited = new HashSet<>(); // Update backtrack set recursively -// updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, currRWSet, visited); - int hbChoice = currentChoice; - updateBacktrackSetRecursive(execution, currentChoice, execution, conflictChoice, execution, hbChoice, currRWSet, visited); + // TODO: The following is the call to the original version of the method +// updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited); + // TODO: The following is the call to the version of the method with pushing up happens-before transitions + updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, execution, currentChoice, currRWSet, visited); } +// TODO: This is the original version of the recursive method // private void updateBacktrackSetRecursive(Execution execution, int currentChoice, // Execution conflictExecution, int conflictChoice, // ReadWriteSet currRWSet, HashSet visited) { @@ -1137,6 +1162,9 @@ public class DPORStateReducer extends ListenerAdapter { updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, pushedExecution, pushedChoice, currRWSet, visited); } + // Remove the transition after being explored + // TODO: Seems to cause a lot of loops---commented out for now + //visited.remove(confTrans); } // --- Functions related to the reachability analysis when there is a state match @@ -1147,13 +1175,8 @@ public class DPORStateReducer extends ListenerAdapter { // 2) at least 2 choices/events have been explored (choiceCounter > 1), // 3) state > 0 (state 0 is for boolean CG) if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) { - if (currVisitedStates.contains(stateId)) { - // Get the backtrack point from the current execution - TransitionEvent transition = currentExecution.getTransitionFromState(stateId); - transition.recordPredecessor(currentExecution, choiceCounter - 1); - updateBacktrackSetsFromPreviousExecution(stateId); - } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution - // Update past executions with a predecessor + if (currVisitedStates.contains(stateId) || prevVisitedStates.contains(stateId)) { + // Update reachable transitions in the graph with a predecessor HashSet reachableTransitions = rGraph.getReachableTransitionsAtState(stateId); for(TransitionEvent transition : reachableTransitions) { transition.recordPredecessor(currentExecution, choiceCounter - 1);