X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerWithSummary.java;h=2bc18a9f83a5e0210a577be66959cec9bd9294f8;hp=39616d97fef3025d072ae95a3c0b339e5b32b5fc;hb=65940568a7cd0c600af6e481d12b97afb3c55b19;hpb=adca12bcd2d11a210d05ad71d0d03b2ec62f97db diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java index 39616d9..2bc18a9 100755 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java @@ -72,13 +72,15 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { private PriorityQueue backtrackStateQ; // Heap that returns the latest state private Execution currentExecution; // Holds the information about the current execution private HashMap> doneBacktrackMap; // Record state ID and trace already constructed + private MainSummary mainSummary; // Main summary (M) for state ID, event, and R/W set + private HashMap stateToPredInfo; // Predecessor info indexed by state ID private HashMap restorableStateMap; // Maps state IDs to the restorable state object private RGraph rGraph; // R-Graph for past executions - private MainSummary mainSummary; // Main summary (M) for state ID, event, and R/W set // Boolean states private boolean isBooleanCGFlipped; private boolean isEndOfExecution; + private boolean isNotCheckedForEventsYet; // Statistics private int numOfTransitions; @@ -99,12 +101,14 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { } } isBooleanCGFlipped = false; - numOfTransitions = 0; - nonRelevantClasses = new HashSet<>(); - nonRelevantFields = new HashSet<>(); - relevantFields = new HashSet<>(); - restorableStateMap = new HashMap<>(); + isNotCheckedForEventsYet = true; mainSummary = new MainSummary(); + numOfTransitions = 0; + nonRelevantClasses = new HashSet<>(); + nonRelevantFields = new HashSet<>(); + relevantFields = new HashSet<>(); + restorableStateMap = new HashMap<>(); + stateToPredInfo = new HashMap<>(); initializeStatesVariables(); } @@ -186,6 +190,18 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { @Override public void choiceGeneratorRegistered(VM vm, ChoiceGenerator nextCG, ThreadInfo currentThread, Instruction executedInstruction) { + if (isNotCheckedForEventsYet) { + // Check if this benchmark has no events + if (nextCG instanceof IntChoiceFromSet) { + IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG; + Integer[] cgChoices = icsCG.getAllChoices(); + if (cgChoices.length == 2 && cgChoices[0] == 0 && cgChoices[1] == -1) { + // This means the benchmark only has 2 choices, i.e., 0 and -1 which means that it has no events + stateReductionMode = false; + } + isNotCheckedForEventsYet = false; + } + } if (stateReductionMode) { // Initialize with necessary information from the CG if (nextCG instanceof IntChoiceFromSet) { @@ -259,7 +275,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { if (!isEndOfExecution) { - // Has to be initialized and a integer CG + // Has to be initialized and it is a integer CG ChoiceGenerator cg = vm.getChoiceGenerator(); if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) { int currentChoice = choiceCounter - 1; // Accumulative choice w.r.t the current trace @@ -523,6 +539,48 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { } } + // This class is a representation of a state. + // It stores the predecessors to a state. + // TODO: We also have stateToEventMap, restorableStateMap, and doneBacktrackMap that has state Id as HashMap key. + private class PredecessorInfo { + private HashSet predecessors; // Maps incoming events/transitions (execution and choice) + private HashMap> recordedPredecessors; + // Memorize event and choice number to not record them twice + + public PredecessorInfo() { + predecessors = new HashSet<>(); + recordedPredecessors = new HashMap<>(); + } + + public HashSet getPredecessors() { + return predecessors; + } + + private boolean isRecordedPredecessor(Execution execution, int choice) { + // See if we have recorded this predecessor earlier + HashSet recordedChoices; + if (recordedPredecessors.containsKey(execution)) { + recordedChoices = recordedPredecessors.get(execution); + if (recordedChoices.contains(choice)) { + return true; + } + } else { + recordedChoices = new HashSet<>(); + recordedPredecessors.put(execution, recordedChoices); + } + // Record the choice if we haven't seen it + recordedChoices.add(choice); + + return false; + } + + public void recordPredecessor(Execution execution, int choice) { + if (!isRecordedPredecessor(execution, choice)) { + predecessors.add(new Predecessor(choice, execution)); + } + } + } + // This class compactly stores transitions: // 1) CG, // 2) state ID, @@ -532,9 +590,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { private int choice; // Choice chosen at this transition private int choiceCounter; // Choice counter at this transition private Execution execution; // The execution where this transition belongs - private HashSet predecessors; // Maps incoming events/transitions (execution and choice) - private HashMap> recordedPredecessors; - // Memorize event and choice number to not record them twice private int stateId; // State at this transition private IntChoiceFromSet transitionCG; // CG at this transition @@ -542,8 +597,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { choice = 0; choiceCounter = 0; execution = null; - predecessors = new HashSet<>(); - recordedPredecessors = new HashMap<>(); stateId = 0; transitionCG = null; } @@ -560,40 +613,12 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { return execution; } - public HashSet getPredecessors() { - return predecessors; - } - public int getStateId() { return stateId; } public IntChoiceFromSet getTransitionCG() { return transitionCG; } - private boolean isRecordedPredecessor(Execution execution, int choice) { - // See if we have recorded this predecessor earlier - HashSet recordedChoices; - if (recordedPredecessors.containsKey(execution)) { - recordedChoices = recordedPredecessors.get(execution); - if (recordedChoices.contains(choice)) { - return true; - } - } else { - recordedChoices = new HashSet<>(); - recordedPredecessors.put(execution, recordedChoices); - } - // Record the choice if we haven't seen it - recordedChoices.add(choice); - - return false; - } - - public void recordPredecessor(Execution execution, int choice) { - if (!isRecordedPredecessor(execution, choice)) { - predecessors.add(new Predecessor(choice, execution)); - } - } - public void setChoice(int cho) { choice = cho; } @@ -606,10 +631,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { execution = exec; } - public void setPredecessors(HashSet preds) { - predecessors = new HashSet<>(preds); - } - public void setStateId(int stId) { stateId = stId; } @@ -632,7 +653,8 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { public Set getEventChoicesAtStateId(int stateId) { HashMap stateSummary = mainSummary.get(stateId); - return stateSummary.keySet(); + // Return a new set since this might get updated concurrently + return new HashSet<>(stateSummary.keySet()); } public ReadWriteSet getRWSetForEventChoiceAtState(int eventChoice, int stateId) { @@ -640,6 +662,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { return stateSummary.get(eventChoice); } + public Set getStateIds() { + return mainSummary.keySet(); + } + private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) { // Combine the same write accesses and record in the recordedRWSet HashMap recordedWriteMap = recordedRWSet.getWriteMap(); @@ -760,7 +786,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { } else { transition = new TransitionEvent(); currentExecution.addTransition(transition); - transition.recordPredecessor(currentExecution, choiceCounter - 1); + addPredecessors(stateId); } transition.setExecution(currentExecution); transition.setTransitionCG(icsCG); @@ -802,16 +828,31 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { choiceCounter = 0; maxEventChoice = 0; // Cycle tracking - currVisitedStates = new HashMap<>(); - justVisitedStates = new HashSet<>(); - prevVisitedStates = new HashSet<>(); - stateToEventMap = new HashMap<>(); + if (!isBooleanCGFlipped) { + currVisitedStates = new HashMap<>(); + justVisitedStates = new HashSet<>(); + prevVisitedStates = new HashSet<>(); + stateToEventMap = new HashMap<>(); + } else { + currVisitedStates.clear(); + justVisitedStates.clear(); + prevVisitedStates.clear(); + stateToEventMap.clear(); + } // Backtracking - backtrackMap = new HashMap<>(); + if (!isBooleanCGFlipped) { + backtrackMap = new HashMap<>(); + } else { + backtrackMap.clear(); + } backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); currentExecution = new Execution(); currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point - doneBacktrackMap = new HashMap<>(); + if (!isBooleanCGFlipped) { + doneBacktrackMap = new HashMap<>(); + } else { + doneBacktrackMap.clear(); + } rGraph = new RGraph(); // Booleans isEndOfExecution = false; @@ -831,15 +872,20 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { // 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 boolean terminate = false; + Set mainStateIds = mainSummary.getStateIds(); for(Integer stateId : justVisitedStates) { - // We perform updates on backtrack sets for every - if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) { - updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1); - terminate = true; - } - // If frequency > 1 then this means we have visited this stateId more than once - if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) { - updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1); + // We exclude states that are produced by other CGs that are not integer CG + // When we encounter these states, then we should also encounter the corresponding integer CG state ID + if (mainStateIds.contains(stateId)) { + // We perform updates on backtrack sets for every + if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) { + updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1); + terminate = true; + } + // If frequency > 1 then this means we have visited this stateId more than once in the current execution + if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) { + updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1); + } } } return terminate; @@ -878,7 +924,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { } // Add the new backtrack execution object TransitionEvent backtrackTransition = new TransitionEvent(); - backtrackTransition.setPredecessors(conflictTransition.getPredecessors()); backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition)); // Add to priority queue if (!backtrackStateQ.contains(stateId)) { @@ -886,6 +931,17 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { } } + private void addPredecessors(int stateId) { + PredecessorInfo predecessorInfo; + if (!stateToPredInfo.containsKey(stateId)) { + predecessorInfo = new PredecessorInfo(); + stateToPredInfo.put(stateId, predecessorInfo); + } else { // This is a new state Id + predecessorInfo = stateToPredInfo.get(stateId); + } + predecessorInfo.recordPredecessor(currentExecution, choiceCounter - 1); + } + // Analyze Read/Write accesses that are directly invoked on fields private void analyzeReadWriteAccesses(Instruction executedInsn, int currentChoice) { // Get the field info @@ -1038,31 +1094,31 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { } private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) { - // 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 (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) { + // 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 (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) { backtrackTransition.getTransitionCG().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.keySet()); - // This marks a transitional period to the new CG - isEndOfExecution = true; + } + // 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.keySet()); + // This marks a transitional period to the new CG + isEndOfExecution = true; } private boolean isConflictFound(int eventChoice, Execution conflictExecution, int conflictChoice, @@ -1101,20 +1157,6 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { 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(Instruction executedInsn) { // Get the field info FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo(); @@ -1159,6 +1201,33 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { return false; } + private HashSet getPredecessors(int stateId) { + // Get a set of predecessors for this state ID + HashSet predecessors; + if (stateToPredInfo.containsKey(stateId)) { + PredecessorInfo predecessorInfo = stateToPredInfo.get(stateId); + predecessors = predecessorInfo.getPredecessors(); + } else { + predecessors = new HashSet<>(); + } + + return predecessors; + } + + 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; + } + // Reset data structure for each new execution private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) { if (choices == null || choices != icsCG.getAllChoices()) { @@ -1167,8 +1236,8 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); // Clear data structures - currVisitedStates = new HashMap<>(); - stateToEventMap = new HashMap<>(); + currVisitedStates.clear(); + stateToEventMap.clear(); isEndOfExecution = false; } } @@ -1224,26 +1293,26 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { return; } visited.add(currTrans); - // Halt if the set is empty - if (currRWSet.isEmpty()) { - return; - } - // Explore all predecessors - for (Predecessor predecessor : currTrans.getPredecessors()) { - // Get the predecessor (previous conflict choice) - int predecessorChoice = predecessor.getChoice(); - Execution predecessorExecution = predecessor.getExecution(); - // Push up one happens-before transition - int newConflictEventChoice = conflictEventChoice; - // Check if a conflict is found - if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, currRWSet)) { - createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice); - // We need to extract the pushed happens-before event choice from the predecessor execution and choice - newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice(); + // Check the predecessors only if the set is not empty + if (!currRWSet.isEmpty()) { + // Explore all predecessors + for (Predecessor predecessor : getPredecessors(currTrans.getStateId())) { + // Get the predecessor (previous conflict choice) + int predecessorChoice = predecessor.getChoice(); + Execution predecessorExecution = predecessor.getExecution(); + // Push up one happens-before transition + int newConflictEventChoice = conflictEventChoice; + // Check if a conflict is found + ReadWriteSet newCurrRWSet = currRWSet.getCopy(); + if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) { + createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice); + // We need to extract the pushed happens-before event choice from the predecessor execution and choice + newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice(); + } + // Continue performing DFS if conflict is not found + updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice, + newCurrRWSet, visited); } - // Continue performing DFS if conflict is not found - updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice, - currRWSet, visited); } } @@ -1257,11 +1326,8 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) { if ((currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) || 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); - } + // Record a new predecessor for a revisited state + addPredecessors(stateId); } } }