From 5bc20c4324f6268b3eed9705d28943621ff14181 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 20 Mar 2020 21:34:59 -0700 Subject: [PATCH] Refactoring; Finding cycles without traversing the entire state graph. --- .../gov/nasa/jpf/listener/StateReducer.java | 237 +++++++++++------- 1 file changed, 143 insertions(+), 94 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 532076b..3af3205 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -91,6 +91,8 @@ public class StateReducer extends ListenerAdapter { // Reference to the state graph in the ConflictTracker class 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; @@ -119,6 +121,7 @@ public class StateReducer extends ListenerAdapter { unusedCG = new HashSet<>(); // TODO: We are assuming that the StateReducer is always used together with the ConflictTracker stateGraph = ConflictTracker.nodes; + stateToEventMap = new HashMap<>(); prevVisitedStates = new HashSet<>(); currVisitedStates = new HashSet<>(); initializeStateReduction(); @@ -161,6 +164,39 @@ public class StateReducer extends ListenerAdapter { } } + 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 - 1); + icsCG.advance(choices[choiceIndex]); + return icsCG; + } + + 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 + 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); + } + IntChoiceFromSet setCG = setNewCG(icsCG); + cgMap.put(setCG, choices[choiceCounter]); + } else { + // We repeat the same trace if a state match is not found yet + IntChoiceFromSet setCG = setNewCG(icsCG); + unusedCG.add(setCG); + } + //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0; + choiceCounter++; + } + @Override public void choiceGeneratorRegistered(VM vm, ChoiceGenerator nextCG, ThreadInfo currentThread, Instruction executedInstruction) { if (stateReductionMode) { @@ -176,35 +212,7 @@ public class StateReducer extends ListenerAdapter { } // Record the subsequent Integer CGs only until we hit the upper bound 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); - } - //choiceCounter = choiceCounter < choiceUpperBound ? choiceCounter + 1 : 0; - choiceCounter++; + initializeChoiceGenerators(icsCG, cgChoices); } else { // Set new CGs to done so that the search algorithm explores the existing CGs icsCG.setDone(); @@ -249,13 +257,13 @@ public class StateReducer extends ListenerAdapter { // 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 visitingStates = new HashSet<>(); - HashSet visitedEvents = new HashSet<>(); + HashSet visitedEvents = stateToEventMap.get(stId); boolean containsCyclesWithAllEvts = false; - ConflictTracker.Node currNode = stateGraph.get(stId); - dfsFindCycles(currNode, visitingStates, visitedEvents, new HashSet<>()); if (checkIfAllEventsInvolved(visitedEvents)) { containsCyclesWithAllEvts = true; } @@ -263,22 +271,41 @@ public class StateReducer extends ListenerAdapter { return containsCyclesWithAllEvts; } - private void dfsFindCycles(ConflictTracker.Node currNode, HashSet visitingStates, - HashSet visitedEvents, HashSet visitingEvents) { - - // Stop when there is a cycle and record all the events - if (visitingStates.contains(currNode)) { - visitedEvents.addAll(visitingEvents); - } else { - visitingStates.add(currNode); - for(ConflictTracker.Edge edge : currNode.getOutEdges()) { - visitingEvents.add(edge.getEventNumber()); - dfsFindCycles(edge.getDst(), visitingStates, visitedEvents, visitingEvents); - visitingEvents.remove(edge.getEventNumber()); - } - visitingStates.remove(currNode); - } - } + // TODO: The following is a full-blown graph traversal that we can do if we need to in the future + // 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 +// private boolean containsCyclesWithAllEvents(int stId) { +// +// HashSet visitingStates = new HashSet<>(); +// HashSet visitedEvents = new HashSet<>(); +// boolean containsCyclesWithAllEvts = false; +// ConflictTracker.Node currNode = stateGraph.get(stId); +// dfsFindCycles(currNode, visitingStates, visitedEvents, new HashSet<>()); +// if (checkIfAllEventsInvolved(visitedEvents)) { +// containsCyclesWithAllEvts = true; +// } +// +// return containsCyclesWithAllEvts; +// } +// +// private void dfsFindCycles(ConflictTracker.Node currNode, HashSet visitingStates, +// HashSet visitedEvents, HashSet visitingEvents) { +// +// // Stop when there is a cycle and record all the events +// if (visitingStates.contains(currNode)) { +// visitedEvents.addAll(visitingEvents); +// } else { +// visitingStates.add(currNode); +// for(ConflictTracker.Edge edge : currNode.getOutEdges()) { +// visitingEvents.add(edge.getEventNumber()); +// dfsFindCycles(edge.getDst(), visitingStates, visitedEvents, visitingEvents); +// visitingEvents.remove(edge.getEventNumber()); +// } +// visitingStates.remove(currNode); +// } +// } private boolean checkIfAllEventsInvolved(HashSet visitedEvents) { @@ -299,6 +326,46 @@ public class StateReducer extends ListenerAdapter { currVisitedStates.clear(); } + private void updateChoices(IntChoiceFromSet icsCG) { + if (choices == null || choices != icsCG.getAllChoices()) { + currCG = icsCG; + choices = icsCG.getAllChoices(); + // Reset a few things for the sub-graph + conflictPairMap.clear(); + readWriteFieldsMap.clear(); + choiceCounter = 0; + } + } + + private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) { + // 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(); + } + 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; + } + } + @Override public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { @@ -316,42 +383,10 @@ public class StateReducer extends ListenerAdapter { if (currentCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; // Update the current pointer to the current set of choices - if (choices == null || choices != icsCG.getAllChoices()) { - currCG = icsCG; - choices = icsCG.getAllChoices(); - // Reset a few things for the sub-graph - conflictPairMap.clear(); - readWriteFieldsMap.clear(); - choiceCounter = 0; - } + updateChoices(icsCG); // Check if we have seen this state or this state contains cycles that involve all events if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(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(); - } - 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; - } + exploreNextBacktrackSets(icsCG); } // Update the VOD graph always with the latest updateVODGraph(icsCG.getNextChoice()); @@ -379,6 +414,28 @@ public class StateReducer extends ListenerAdapter { choiceSet.add(currChoice); } + private void mapStateToEvent(Search search) { + // 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) + stateId = search.getStateId(); + currVisitedStates.add(stateId); + mapStateToEvent(search); + } + } + @Override public void stateAdvanced(Search search) { if (debugMode) { @@ -398,11 +455,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"); } - if (stateReductionMode) { - // Update the state ID variables - stateId = search.getStateId(); - currVisitedStates.add(stateId); - } + updateStateInfo(search); } @Override @@ -413,14 +466,10 @@ public class StateReducer extends ListenerAdapter { transition = search.getTransition(); detail = null; - // Update the state variables - // Line 19 in the paper page 11 (see the heading note above) - stateId = search.getStateId(); - currVisitedStates.add(stateId); - out.println("\n==> DEBUG: The state is backtracked to state with id: " + id + " -- Transition: " + transition + " and depth: " + depth + "\n"); } + updateStateInfo(search); } @Override @@ -680,11 +729,11 @@ public class StateReducer extends ListenerAdapter { public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { if (isInitialized) { - if (choiceCounter <= 0 || choiceCounter > choices.length - 1) { + int currentChoice = (choiceCounter % (choices.length - 1)) - 1; + if (currentChoice < 0) { // We do not compute the conflicts for the choice '-1' return; } - int currentChoice = choiceCounter - 1; // Record accesses from executed instructions if (executedInsn instanceof JVMFieldInstruction) { // Analyze only after being initialized -- 2.34.1