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=71eaf325f2022190bd8da2d1e3f4aa5ba612107e;hp=f70c992219956b8e9fc003bc289bff1882bbaca2;hb=25f3da45d7f3fbc53ee80b92d8ff60fcaca48738;hpb=2c58565baa61262d690c9683b1864f8f99bcba2a diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index f70c992..71eaf32 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -34,7 +34,17 @@ import java.util.*; // TODO: Fix for Groovy's model-checking // TODO: This is a setter to change the values of the ChoiceGenerator to implement POR /** - * simple tool to log state changes + * 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 { @@ -66,7 +76,24 @@ public class StateReducer extends ListenerAdapter { private HashSet backtrackSet; private HashMap> conflictPairMap; // Map choicelist with start index -// private HashMap choiceListStartIndexMap; + // private HashMap choiceListStartIndexMap; + + // 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 int stateId; + // Previous state + private int prevStateId; + // Previous choice number + private int prevChoiceValue; + // Counter for a visited state + private HashMap visitedStateCounter; + // HashSet that stores references to unused CGs + private HashSet unusedCG; public StateReducer(Config config, JPF jpf) { debugMode = config.getBoolean("debug_state_transition", false); @@ -81,6 +108,17 @@ public class StateReducer extends ListenerAdapter { id = 0; transition = null; isBooleanCGFlipped = false; + vodGraphMap = new HashMap<>(); + stateId = -1; + prevStateId = -1; + prevChoiceValue = -1; + cgMap = new HashMap<>(); + readWriteFieldsMap = new HashMap<>(); + backtrackMap = new HashMap<>(); + backtrackSet = new HashSet<>(); + conflictPairMap = new HashMap<>(); + unusedCG = new HashSet<>(); + visitedStateCounter = new HashMap<>(); initializeStateReduction(); } @@ -93,11 +131,11 @@ public class StateReducer extends ListenerAdapter { maxUpperBound = 0; isInitialized = false; isResetAfterAnalysis = false; - cgMap = new HashMap<>(); - readWriteFieldsMap = new HashMap<>(); - backtrackMap = new HashMap<>(); - backtrackSet = new HashSet<>(); - conflictPairMap = new HashMap<>(); + cgMap.clear(); + readWriteFieldsMap.clear(); + backtrackMap.clear(); + backtrackSet.clear(); + conflictPairMap.clear(); } } @@ -135,28 +173,37 @@ public class StateReducer extends ListenerAdapter { isInitialized = true; } // Record the subsequent Integer CGs only until we hit the upper bound - if (!isResetAfterAnalysis && 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 - choices = new Integer[cgChoices.length + 1]; - System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length); - choices[choices.length - 1] = -1; - String firstChoiceListString = buildStringFromChoiceList(choices); - backtrackSet.add(firstChoiceListString); + if (!isResetAfterAnalysis) { + 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 + choices = new Integer[cgChoices.length + 1]; + System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length); + choices[choices.length - 1] = -1; + String firstChoiceListString = buildStringFromChoiceList(choices); + backtrackSet.add(firstChoiceListString); + } + icsCG.setNewValues(choices); + icsCG.reset(); + // Advance the current Integer CG + // This way we explore all the event numbers in the first pass + icsCG.advance(choices[choiceCounter]); + cgMap.put(icsCG, choices[choiceCounter]); + } else { + // We repeat the same trace if a state match is not found yet + icsCG.setNewValues(choices); + icsCG.reset(); + // Use a modulo since choiceCounter is going to keep increasing + int choiceIndex = choiceCounter % (choices.length - 1); + icsCG.advance(choices[choiceIndex]); + unusedCG.add(icsCG); } - icsCG.setNewValues(choices); - icsCG.reset(); - // Advance the current Integer CG - // This way we explore all the event numbers in the first pass - icsCG.advance(choices[choiceCounter]); - cgMap.put(icsCG, choices[choiceCounter]); choiceCounter++; } else { - // Set done the subsequent CGs - // We only need n CGs (n is event numbers) + // Set new CGs to done so that the search algorithm explores the existing CGs icsCG.setDone(); } } @@ -168,6 +215,10 @@ public class StateReducer extends ListenerAdapter { 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 @@ -183,6 +234,31 @@ public class StateReducer extends ListenerAdapter { cg.setDone(); } } + // Set done every CG in the unused CG set + for (IntChoiceFromSet cg : unusedCG) { + cg.setDone(); + } + unusedCG.clear(); + } + + private void incrementVisitedStateCounter(int stId) { + // Increment counter for this state ID + if (visitedStateCounter.containsKey(stId)) { + int stateCount = visitedStateCounter.get(stId); + visitedStateCounter.put(stId, stateCount + 1); + } else { + // If we have seen it then the frequency is 2 + visitedStateCounter.put(stId, 2); + } + } + + private boolean isVisitedMultipleTimes(int stId) { + // Return true if the state has been visited more than once + if (visitedStateCounter.containsKey(stId) && + visitedStateCounter.get(stId) > 1) { + return true; + } + return false; } @Override @@ -210,34 +286,62 @@ public class StateReducer extends ListenerAdapter { readWriteFieldsMap.clear(); choiceCounter = 0; } - // Traverse the sub-graphs - if (isResetAfterAnalysis) { - // Advance choice counter for sub-graphs - choiceCounter++; - // Do this for every CG after finishing each backtrack list - if (icsCG.getNextChoice() == -1) { - 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 { - // Set done if this was the last backtrack list - icsCG.setDone(); + if (!vm.isNewState()) { + incrementVisitedStateCounter(stateId); + } + // Check if we have seen this state and it's not looping back to itself + if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) { + // Traverse the sub-graphs + if (isResetAfterAnalysis) { + // Advance choice counter for sub-graphs + choiceCounter++; + // 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)) { + 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 { + // Set done if this was the last backtrack list + icsCG.setDone(); + } } + } 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; } } - // Update and reset the CG if needed (do this for the first time after the analysis) - if (!isResetAfterAnalysis && icsCG.getNextChoice() == -1) { - resetAllCGs(); - isResetAfterAnalysis = true; - } } } } + public void updateVODGraph(int prevChoice, int currChoice) { + + HashSet choiceSet; + if (vodGraphMap.containsKey(prevChoice)) { + // If the key already exists, just retrieve it + choiceSet = vodGraphMap.get(prevChoice); + } else { + // Create a new entry + choiceSet = new HashSet<>(); + vodGraphMap.put(prevChoice, choiceSet); + } + choiceSet.add(currChoice); + } + + private void updateStateId(Search search) { + // Saving the previous state + prevStateId = stateId; + // Line 19 in the paper page 11 (see the heading note above) + stateId = search.getStateId(); + } + @Override public void stateAdvanced(Search search) { if (debugMode) { @@ -257,6 +361,31 @@ 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"); } + if (stateReductionMode) { + // Update vodGraph + int currChoice = choiceCounter - 1; + // Adjust currChoice with modulo + currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice; + if (currChoice < 0 || choices[currChoice] == -1 || + prevChoiceValue == choices[currChoice]) { +// || currChoice > choices.length - 1 || choices[currChoice] == -1 || +// prevChoiceValue == choices[currChoice]) { +// // When current choice is 0, previous choice could be -1 +// updateVODGraph(prevChoiceValue, choices[currChoice]); +// // Current choice becomes previous choice in the next iteration +// prevChoiceValue = choices[currChoice]; + // Update the state ID variables + updateStateId(search); + // Handle all corner cases (e.g., out of bound values) + return; + } + // When current choice is 0, previous choice could be -1 + updateVODGraph(prevChoiceValue, choices[currChoice]); + // Current choice becomes previous choice in the next iteration + prevChoiceValue = choices[currChoice]; + // Update the state ID variables + updateStateId(search); + } } @Override @@ -267,6 +396,12 @@ public class StateReducer extends ListenerAdapter { transition = search.getTransition(); detail = null; + // Update the state variables + // Saving the previous state + prevStateId = stateId; + // Line 19 in the paper page 11 (see the heading note above) + stateId = search.getStateId(); + out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition + " and depth: " + depth + "\n"); } @@ -425,7 +560,7 @@ public class StateReducer extends ListenerAdapter { // 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) { + if (currCG != null && cgMap.containsKey(currCG)) { int backtrackListIndex = cgMap.get(currCG); backtrackChoiceLists = backtrackMap.get(backtrackListIndex); int listLength = choices.length; @@ -487,11 +622,45 @@ public class StateReducer extends ListenerAdapter { return false; } + // 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) { + nodesToVisit.addLast(nextNode); + } + } + } + } + return false; + } + @Override public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { if (isInitialized) { - if (choiceCounter > choices.length - 1) { + if (choiceCounter <= 0 || choiceCounter > choices.length - 1) { // We do not compute the conflicts for the choice '-1' return; } @@ -514,13 +683,9 @@ public class StateReducer extends ListenerAdapter { String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); // We don't care about libraries if (!isFieldExcluded(fieldClass)) { - // For the main graph we go down to 0, but for subgraph, we only go down to 1 since 0 contains - // the reversed event -// int end = !isResetAfterAnalysis ? 0 : choiceListStartIndexMap.get(choices); // 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 >= end; eventNumber--) { for (int eventNumber = currentChoice - 1; eventNumber >= 0; eventNumber--) { // Skip if this event number does not have any Read/Write set if (!readWriteFieldsMap.containsKey(choices[eventNumber])) { @@ -536,9 +701,13 @@ public class StateReducer extends ListenerAdapter { // 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; + // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above) + if (vm.isNewState() || + (!vm.isNewState() && isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1]))) { + createBacktrackChoiceList(currentChoice, eventNumber); + // Break if a conflict is found! + break; + } } } }