From ca18eccfbdf9e4102ee3de05efded9d4b68f1334 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Thu, 30 Jan 2020 12:08:01 -0800 Subject: [PATCH] Adding the first implementation of visible operation dependency graph for stateful DPOR: need to do more test to make sure that it's really working. --- .../gov/nasa/jpf/listener/StateReducer.java | 109 ++++++++++++++++-- 1 file changed, 101 insertions(+), 8 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index f70c992..6d5a026 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 { @@ -68,6 +78,16 @@ public class StateReducer extends ListenerAdapter { // Map choicelist with start index // 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 + private HashSet visitedStateSet; + // Current state + private int stateId; + public StateReducer(Config config, JPF jpf) { debugMode = config.getBoolean("debug_state_transition", false); stateReductionMode = config.getBoolean("activate_state_reduction", true); @@ -81,6 +101,9 @@ public class StateReducer extends ListenerAdapter { id = 0; transition = null; isBooleanCGFlipped = false; + vodGraphMap = new HashMap<>(); + visitedStateSet = new HashSet<>(); + stateId = -1; initializeStateReduction(); } @@ -238,6 +261,20 @@ public class StateReducer extends ListenerAdapter { } } + 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); + } + @Override public void stateAdvanced(Search search) { if (debugMode) { @@ -257,6 +294,28 @@ 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) { + // Line 19 in the paper page 11 (see the heading note above) + stateId = search.getStateId(); + if (visitedStateSet.contains(stateId)) { + // VOD graph is not updated if the "new" state has been seen earlier + return; + } + // Add state ID into the visited state set + visitedStateSet.add(stateId); + // Update vodGraph + int currChoice = choiceCounter - 1; + int prevChoice = currChoice - 1; + if (currChoice < 0) { + // Current choice has to be at least 0 (initial case can be -1) + return; + } + // Current choice and previous choice values could be -1 (since we use -1 as the end-of-array condition) + int currChoiceValue = (choices[currChoice] == -1) ? 0 : choices[currChoice]; + // When current choice is 0, previous choice could be -1 + int prevChoiceValue = (prevChoice == -1) ? -1 : choices[prevChoice]; + updateVODGraph(prevChoiceValue, currChoiceValue); + } } @Override @@ -487,6 +546,40 @@ 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) { @@ -514,13 +607,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 +625,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 (!visitedStateSet.contains(stateId)|| + (visitedStateSet.contains(stateId) && isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1]))) { + createBacktrackChoiceList(currentChoice, eventNumber); + // Break if a conflict is found! + break; + } } } } -- 2.34.1