From ec75783ad3fb62f4bf53822da5cf2e7db0721891 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Tue, 14 Apr 2020 16:24:10 -0700 Subject: [PATCH] Adding reachability analysis when state matching occurs. --- main.jpf | 6 +- .../nasa/jpf/listener/DPORStateReducer.java | 179 +++++++++--------- 2 files changed, 94 insertions(+), 91 deletions(-) diff --git a/main.jpf b/main.jpf index 1742858..81a40dc 100644 --- a/main.jpf +++ b/main.jpf @@ -8,8 +8,8 @@ target = main #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer -listener=gov.nasa.jpf.listener.ConflictTrackerOld -#listener=gov.nasa.jpf.listener.DPORStateReducer +#listener=gov.nasa.jpf.listener.ConflictTrackerOld +listener=gov.nasa.jpf.listener.DPORStateReducer #listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld # Potentially conflicting variables @@ -48,7 +48,7 @@ debug_mode=true # Debug mode for StateReducer printout_state_transition=true -activate_state_reduction=false +#activate_state_reduction=false # Timeout in minutes (default is 0 which means no timeout) timeout=1440 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 22cc82f..c8c7806 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -39,12 +39,13 @@ import java.util.*; * 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. + * The algorithm is presented on page 11 of the paper. Basically, we have a graph G + * (i.e., visible operation dependency graph). + * This DPOR implementation actually fixes the algorithm in the SPIN paper that does not + * consider cases where a state could be matched early. In this new algorithm/implementation, + * each run is terminated iff: + * - we find a state that matches a state in a previous run, or + * - we have a matched state in the current run that consists of cycles that contain all choices/events. */ public class DPORStateReducer extends ListenerAdapter { @@ -74,14 +75,8 @@ public class DPORStateReducer extends ListenerAdapter { private ArrayList backtrackPointList; // Record backtrack points (CG, state Id, and choice) private HashMap> conflictPairMap; // Record conflicting events private HashSet doneBacktrackSet; // Record state ID and trace already constructed - private HashMap newStateEventMap; // Record event producing a new state ID private HashMap readWriteFieldsMap; // Record fields that are accessed - private HashMap restorableStateMap; // Maps state IDs to the restorable state object - - // Visible operation dependency graph implementation (SPIN paper) related fields - private int currChoiceValue; - private int prevChoiceValue; - private HashMap> vodGraphMap; // Visible operation dependency graph (VOD graph) + private HashMap restorableStateMap; // Maps state IDs to the restorable state object // Boolean states private boolean isBooleanCGFlipped; @@ -286,10 +281,7 @@ public class DPORStateReducer extends ListenerAdapter { // Check and record a backtrack set for just once! if (isConflictFound(nextInsn, eventCounter, currentChoice, fieldClass) && isNewConflict(currentChoice, eventCounter)) { - // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above) - if (vm.isNewState() || isReachableInVODGraph(currentChoice, vm)) { - createBacktrackingPoint(currentChoice, eventCounter); - } + createBacktrackingPoint(currentChoice, eventCounter); } } } @@ -325,6 +317,14 @@ public class DPORStateReducer extends ListenerAdapter { writeSet.put(field, objectId); } + public Set getReadSet() { + return readSet.keySet(); + } + + public Set getWriteSet() { + return writeSet.keySet(); + } + public boolean readFieldExists(String field) { return readSet.containsKey(field); } @@ -365,6 +365,25 @@ public class DPORStateReducer extends ListenerAdapter { } } + // This class compactly stores: 1) restorable VM state, and 2) global choice counter + private class RestorableState { + private RestorableVMState restorableState; + private int choiceCounter; + + public RestorableState (RestorableVMState restState, int choCtr) { + restorableState = restState; + choiceCounter = choCtr; + } + + public RestorableVMState getRestorableState() { + return restorableState; + } + + public int getChoiceCounter() { + return choiceCounter; + } + } + // -- CONSTANTS private final static String DO_CALL_METHOD = "doCall"; // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure @@ -397,14 +416,12 @@ public class DPORStateReducer extends ListenerAdapter { icsCG.setChoice(currCGIndex, expectedChoice); } } - // Update current choice - currChoiceValue = refChoices[choiceIndex]; // Record state ID and choice/event as backtrack point int stateId = vm.getStateId(); backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex])); // Store restorable state object for this state (always store the latest) RestorableVMState restorableState = vm.getRestorableState(); - restorableStateMap.put(stateId, restorableState); + restorableStateMap.put(stateId, new RestorableState(restorableState, choiceCounter)); } private Integer[] copyChoices(Integer[] choicesToCopy) { @@ -456,12 +473,7 @@ public class DPORStateReducer extends ListenerAdapter { backtrackPointList = new ArrayList<>(); conflictPairMap = new HashMap<>(); doneBacktrackSet = new HashSet<>(); - newStateEventMap = new HashMap<>(); readWriteFieldsMap = new HashMap<>(); - // VOD graph - currChoiceValue = 0; - prevChoiceValue = -1; - vodGraphMap = new HashMap<>(); // Booleans isEndOfExecution = false; } @@ -498,8 +510,7 @@ public class DPORStateReducer extends ListenerAdapter { stateToEventMap.put(stateId, eventSet); } justVisitedStates.add(stateId); - // Update the VOD graph when there is a new state - updateVODGraph(search.getVM()); + analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); } // --- Functions related to Read/Write access analysis on shared fields @@ -672,7 +683,7 @@ public class DPORStateReducer extends ListenerAdapter { int hiStateId = backtrackStateQ.peek(); // Restore the state first if necessary if (vm.getStateId() != hiStateId) { - RestorableVMState restorableState = restorableStateMap.get(hiStateId); + RestorableVMState restorableState = restorableStateMap.get(hiStateId).getRestorableState(); vm.restoreState(restorableState); } // Set the backtrack CG @@ -702,6 +713,39 @@ public class DPORStateReducer extends ListenerAdapter { return rwSet; } + private boolean isConflictFound(int eventCounter, int currentChoice) { + + int actualCurrCho = currentChoice % refChoices.length; + // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) + if (!readWriteFieldsMap.containsKey(eventCounter) || + choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) { + return false; + } + // Current R/W set + ReadWriteSet currRWSet = readWriteFieldsMap.get(currentChoice); + // R/W set of choice/event that may have a potential conflict + ReadWriteSet evtRWSet = readWriteFieldsMap.get(eventCounter); + // 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)) { + return true; + } + } + // Check for conflicts with Write fields for Read instructions + Set currReadSet = currRWSet.getReadSet(); + for(String readField : currReadSet) { + int currObjId = currRWSet.readFieldObjectId(readField); + if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) { + return true; + } + } + // Return false if no conflict is found + return false; + } + private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) { int actualCurrCho = currentChoice % refChoices.length; @@ -797,70 +841,29 @@ public class DPORStateReducer extends ListenerAdapter { } } - // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper - - // This method checks whether a choice/event (transition) is reachable from the choice/event that produces - // the state right before this state in the VOD graph - // We use a BFS algorithm for this purpose - private boolean isReachableInVODGraph(int currentChoice, VM vm) { - // Current event - int choiceIndex = currentChoice % refChoices.length; - int currEvent = refChoices[choiceIndex]; - // Previous event - int stateId = vm.getStateId(); // A state that has been seen - int prevEvent = newStateEventMap.get(stateId); - // Only start traversing the graph if prevEvent has an outgoing edge - if (vodGraphMap.containsKey(prevEvent)) { - // Record visited choices as we search in the graph - HashSet visitedChoice = new HashSet<>(); - visitedChoice.add(prevEvent); - // Get the first nodes to visit (the neighbors of prevEvent) - LinkedList nodesToVisit = new LinkedList<>(); - nodesToVisit.addAll(vodGraphMap.get(prevEvent)); - // Traverse the graph using BFS - while (!nodesToVisit.isEmpty()) { - int choice = nodesToVisit.removeFirst(); - if (choice == currEvent) { - return true; - } - if (visitedChoice.contains(choice)) { // If there is a loop then just continue the exploration - continue; - } - // Continue searching - visitedChoice.add(choice); - HashSet choiceNextNodes = vodGraphMap.get(choice); - if (choiceNextNodes != null) { - // Add only if there is a mapping for next nodes - for (Integer nextNode : choiceNextNodes) { - // Skip cycles - if (nextNode == choice) { - continue; + // --- Functions related to the reachability analysis when there is a state match + + // We use backtrackPointsList to analyze the reachable states/events when there is a state match: + // 1) Whenever there is state match, there is a cycle of events + // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle + // 3) Then we create a new backtrack point for every new conflict + private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { + // Perform this analysis only when there is a state match + if (!vm.isNewState()) { + if (restorableStateMap.containsKey(stateId)) { + // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts + int conflictChoice = restorableStateMap.get(stateId).getChoiceCounter(); + int currentChoice = choiceCounter - 1; + // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward) + while (conflictChoice < currentChoice) { + for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) { + if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) { + createBacktrackingPoint(conflictChoice, eventCounter); } - nodesToVisit.addLast(nextNode); } + conflictChoice++; } } } - return false; - } - - private void updateVODGraph(VM vm) { - // Do this only if it is a new state - if (vm.isNewState()) { - // Update the graph when we have the current choice value - HashSet choiceSet; - if (vodGraphMap.containsKey(prevChoiceValue)) { - // If the key already exists, just retrieve it - choiceSet = vodGraphMap.get(prevChoiceValue); - } else { - // Create a new entry - choiceSet = new HashSet<>(); - vodGraphMap.put(prevChoiceValue, choiceSet); - } - choiceSet.add(currChoiceValue); - prevChoiceValue = currChoiceValue; - // Map this state ID to the event (transition) that produces it - newStateEventMap.put(vm.getStateId(), currChoiceValue); - } } } -- 2.34.1