From 9ec360a1ff7dab0435778fc07216add56ebb0c9e Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 5 Jun 2020 13:45:40 -0700 Subject: [PATCH] New algorithm implementation; without pushing forward hb transaction; untested/undebugged yet. --- .../nasa/jpf/listener/DPORStateReducer.java | 620 +++++++++--------- 1 file changed, 326 insertions(+), 294 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index bc42a46..f503dfa 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -34,19 +34,9 @@ import java.util.*; import java.util.logging.Logger; import java.io.IOException; -// 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. - * - * 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 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: + * This a DPOR implementation for event-driven applications with loops that create cycles of state matching + * In this new DPOR 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. */ @@ -80,7 +70,7 @@ public class DPORStateReducer extends ListenerAdapter { private HashSet doneBacktrackSet; // Record state ID and trace already constructed private HashMap restorableStateMap; // Maps state IDs to the restorable state object private HashMap stateToChoiceCounterMap; // Maps state IDs to the choice counter - private HashMap> rGraph; // Create a reachability graph for past executions + private HashMap> rGraph; // Reachability graph for past executions // Boolean states private boolean isBooleanCGFlipped; @@ -151,6 +141,8 @@ public class DPORStateReducer extends ListenerAdapter { " which is " + detail + " Transition: " + transition + "\n"); } if (stateReductionMode) { + // Only add a transition into R-Graph when it advances the state + addTransitionToRGRaph(); updateStateInfo(search); } } @@ -245,7 +237,9 @@ public class DPORStateReducer extends ListenerAdapter { // If this is a new CG then we need to update data structures resetStatesForNewExecution(icsCG, vm); // If we don't see a fair scheduling of events/choices then we have to enforce it - fairSchedulingAndBacktrackPoint(icsCG, vm); + fairSchedulingAndTransition(icsCG, vm); + // Update backtrack set of an executed event (transition): one transition before this one + updateBacktrackSet(currentExecution, choiceCounter - 1); // Explore the next backtrack point: // 1) if we have seen this state or this state contains cycles that involve all events, and // 2) after the current CG is advanced at least once @@ -288,16 +282,6 @@ public class DPORStateReducer extends ListenerAdapter { // Handle the read/write accesses that occur through iterators analyzeReadWriteAccesses(executedInsn, ti, currentChoice); } - // Analyze conflicts from next instructions - if (nextInsn instanceof JVMFieldInstruction) { - // Skip the constructor because it is called once and does not have shared access with other objects - if (!nextInsn.getMethodInfo().getName().equals("")) { - String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName(); - if (!isFieldExcluded(fieldClass)) { - findFirstConflictAndCreateBacktrackPoint(currentChoice, nextInsn, fieldClass); - } - } - } } } } @@ -310,67 +294,44 @@ public class DPORStateReducer extends ListenerAdapter { // This class compactly stores backtrack execution: // 1) backtrack choice list, and - // 2) backtrack execution + // 2) first backtrack point (linking with predecessor execution) private class BacktrackExecution { private Integer[] choiceList; - private Execution execution; + private TransitionEvent firstTransition; - public BacktrackExecution(Integer[] choList, Execution exec) { + public BacktrackExecution(Integer[] choList, TransitionEvent fTransition) { choiceList = choList; - execution = exec; + firstTransition = fTransition; } public Integer[] getChoiceList() { return choiceList; } - public Execution getExecution() { - return execution; - } - } - - // This class compactly stores backtrack points: - // 1) backtrack state ID, and - // 2) backtracking choices - private class BacktrackPoint { - private IntChoiceFromSet backtrackCG; // CG at this backtrack point - private int stateId; // State at this backtrack point - private int choice; // Choice chosen at this backtrack point - - public BacktrackPoint(IntChoiceFromSet cg, int stId, int cho) { - backtrackCG = cg; - stateId = stId; - choice = cho; - } - - public IntChoiceFromSet getBacktrackCG() { return backtrackCG; } - - public int getStateId() { - return stateId; - } - - public int getChoice() { - return choice; + public TransitionEvent getFirstTransition() { + return firstTransition; } } // This class stores a representation of the execution graph node + // TODO: We can modify this class to implement some optimization (e.g., clock-vector) + // TODO: We basically need to keep track of: + // TODO: (1) last read/write access to each memory location + // TODO: (2) last state with two or more incoming events (transitions) private class Execution { private HashMap cgToChoiceMap; // Map between CG to choice numbers for O(1) access - private ArrayList executionTrace; // The BacktrackPoint objects of this execution - private int parentChoice; // The parent's choice that leads to this execution - private Execution parent; // Store the parent for backward DFS to find conflicts + private ArrayList executionTrace; // The BacktrackPoint objects of this execution private HashMap readWriteFieldsMap; // Record fields that are accessed + private HashMap stateToTransitionMap; // For O(1) access to backtrack point public Execution() { cgToChoiceMap = new HashMap<>(); executionTrace = new ArrayList<>(); - parentChoice = -1; - parent = null; readWriteFieldsMap = new HashMap<>(); + stateToTransitionMap = new HashMap<>(); } - public void addBacktrackPoint(BacktrackPoint newBacktrackPoint) { + public void addTransition(TransitionEvent newBacktrackPoint) { executionTrace.add(newBacktrackPoint); } @@ -378,36 +339,133 @@ public class DPORStateReducer extends ListenerAdapter { cgToChoiceMap = null; } - public ArrayList getExecutionTrace() { - return executionTrace; + public TransitionEvent getTransitionFromState(int stateId) { + if (stateToTransitionMap.containsKey(stateId)) { + return stateToTransitionMap.get(stateId); + } + return null; } public int getChoiceFromCG(IntChoiceFromSet icsCG) { return cgToChoiceMap.get(icsCG); } - public int getParentChoice() { - return parentChoice; - } - - public Execution getParent() { - return parent; + public ArrayList getExecutionTrace() { + return executionTrace; } public HashMap getReadWriteFieldsMap() { return readWriteFieldsMap; } + public TransitionEvent getFirstTransition() { + return executionTrace.get(0); + } + + public TransitionEvent getLastTransition() { + return executionTrace.get(executionTrace.size() - 1); + } + + public boolean isNew() { + return executionTrace.size() == 1; + } + public void mapCGToChoice(IntChoiceFromSet icsCG, int choice) { cgToChoiceMap.put(icsCG, choice); } - public void setParentChoice(int parChoice) { - parentChoice = parChoice; + public void mapStateToTransition(int stateId, TransitionEvent backtrackPoint) { + stateToTransitionMap.put(stateId, backtrackPoint); + } + } + + // This class compactly stores a predecessor + // 1) a predecessor execution + // 2) the predecessor choice in that predecessor execution + private class Predecessor { + private int predecessorChoice; // Predecessor choice + private Execution predecessorExecution; // Predecessor execution + + public Predecessor(int predChoice, Execution predExec) { + predecessorChoice = predChoice; + predecessorExecution = predExec; + } + + public int getPredecessorChoice() { + return predecessorChoice; + } + + public Execution getPredecessorExecution() { + return predecessorExecution; + } + } + + // This class compactly stores backtrack points: + // 1) CG, + // 2) state ID, + // 3) choice, + // 4) predecessors (for backward DFS). + private class TransitionEvent { + private IntChoiceFromSet transitionCG; // CG at this transition + private int stateId; // State at this transition + private int choice; // Choice chosen at this transition + private Execution execution; // The execution where this transition belongs + private int choiceCounter; // Choice counter at this transition + private HashSet predecessors; // Maps incoming events/transitions (execution and choice) + + public TransitionEvent() { + transitionCG = null; + stateId = -1; + choice = -1; + execution = null; + choiceCounter = -1; + predecessors = new HashSet<>(); + } + + public void setTransitionCG(IntChoiceFromSet cg) { + transitionCG = cg; + } + + public void setStateId(int stId) { + stateId = stId; } - public void setParent(Execution par) { - parent = par; + public void setChoice(int cho) { + choice = cho; + } + + public void setChoiceCounter(int choCounter) { + choiceCounter = choCounter; + } + + public IntChoiceFromSet getTransitionCG() { return transitionCG; } + + public int getStateId() { + return stateId; + } + + public int getChoice() { + return choice; + } + + public int getChoiceCounter() { + return choiceCounter; + } + + public void setExecution(Execution exec) { + execution = exec; + } + + public Execution getExecution() { + return execution; + } + + public HashSet getPredecessors() { + return predecessors; + } + + public void recordPredecessor(Execution execution, int choice) { + predecessors.add(new Predecessor(choice, execution)); } } @@ -415,44 +473,80 @@ public class DPORStateReducer extends ListenerAdapter { // We store the field name and its object ID // Sharing the same field means the same field name and object ID private class ReadWriteSet { - private HashMap readSet; - private HashMap writeSet; + private HashMap readMap; + private HashMap writeMap; public ReadWriteSet() { - readSet = new HashMap<>(); - writeSet = new HashMap<>(); + readMap = new HashMap<>(); + writeMap = new HashMap<>(); } public void addReadField(String field, int objectId) { - readSet.put(field, objectId); + readMap.put(field, objectId); } public void addWriteField(String field, int objectId) { - writeSet.put(field, objectId); + writeMap.put(field, objectId); + } + + public void removeReadField(String field) { + readMap.remove(field); + } + + public void removeWriteField(String field) { + writeMap.remove(field); + } + + public boolean isEmpty() { + return readMap.isEmpty() && writeMap.isEmpty(); + } + + public ReadWriteSet getCopy() { + ReadWriteSet copyRWSet = new ReadWriteSet(); + // Copy the maps in the set into the new object copy + copyRWSet.setReadMap(new HashMap<>(this.getReadMap())); + copyRWSet.setWriteMap(new HashMap<>(this.getWriteMap())); + return copyRWSet; } public Set getReadSet() { - return readSet.keySet(); + return readMap.keySet(); } public Set getWriteSet() { - return writeSet.keySet(); + return writeMap.keySet(); } public boolean readFieldExists(String field) { - return readSet.containsKey(field); + return readMap.containsKey(field); } public boolean writeFieldExists(String field) { - return writeSet.containsKey(field); + return writeMap.containsKey(field); } public int readFieldObjectId(String field) { - return readSet.get(field); + return readMap.get(field); } public int writeFieldObjectId(String field) { - return writeSet.get(field); + return writeMap.get(field); + } + + private HashMap getReadMap() { + return readMap; + } + + private HashMap getWriteMap() { + return writeMap; + } + + private void setReadMap(HashMap rMap) { + readMap = rMap; + } + + private void setWriteMap(HashMap wMap) { + writeMap = wMap; } } @@ -477,7 +571,7 @@ public class DPORStateReducer extends ListenerAdapter { private final static String JAVA_STRING_LIB = "java.lang.String"; // -- FUNCTIONS - private void fairSchedulingAndBacktrackPoint(IntChoiceFromSet icsCG, VM vm) { + private void fairSchedulingAndTransition(IntChoiceFromSet icsCG, VM vm) { // Check the next choice and if the value is not the same as the expected then force the expected value int choiceIndex = choiceCounter % refChoices.length; int nextChoice = icsCG.getNextChoice(); @@ -488,9 +582,25 @@ public class DPORStateReducer extends ListenerAdapter { icsCG.setChoice(currCGIndex, expectedChoice); } } - // Record state ID and choice/event as backtrack point + // Get state ID and associate it with this transition int stateId = vm.getStateId(); - currentExecution.addBacktrackPoint(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex])); + // Get a new transition + TransitionEvent transition; + if (currentExecution.isNew()) { + // We need to handle the first transition differently because this has a predecessor execution + transition = currentExecution.getFirstTransition(); + } else { + transition = new TransitionEvent(); + transition.recordPredecessor(currentExecution, choiceCounter - 1); + } + transition.setExecution(currentExecution); + transition.setTransitionCG(icsCG); + transition.setStateId(stateId); + transition.setChoice(refChoices[choiceIndex]); + transition.setChoiceCounter(choiceCounter); + // Add new transition to the current execution + currentExecution.mapStateToTransition(stateId, transition); + currentExecution.addTransition(transition); currentExecution.mapCGToChoice(icsCG, choiceCounter); // Store restorable state object for this state (always store the latest) RestorableVMState restorableState = vm.getRestorableState(); @@ -512,7 +622,7 @@ public class DPORStateReducer extends ListenerAdapter { // (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) { + private boolean completeFullCycle(int stId) { // False if the state ID hasn't been recorded if (!stateToEventMap.containsKey(stId)) { @@ -544,6 +654,7 @@ public class DPORStateReducer extends ListenerAdapter { backtrackMap = new HashMap<>(); backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); currentExecution = new Execution(); + currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point doneBacktrackSet = new HashSet<>(); stateToChoiceCounterMap = new HashMap<>(); rGraph = new HashMap<>(); @@ -561,20 +672,23 @@ public class DPORStateReducer extends ListenerAdapter { } } - private void saveExecutionToRGraph(int stateId) { - // Save execution state into the reachability graph only if - // (1) It is not a revisited state from a past execution, or - // (2) It is just a new backtracking point - if (!prevVisitedStates.contains(stateId) || - choiceCounter <= 1) { - ArrayList reachableExecutions; - if (!prevVisitedStates.contains(stateId)) { - reachableExecutions = new ArrayList<>(); - rGraph.put(stateId, reachableExecutions); - } else { - reachableExecutions = rGraph.get(stateId); - } - reachableExecutions.add(currentExecution); + // Save the current transition into R-Graph + // Basically the current transition is reachable from the final state of the previous transition in this execution + private void addTransitionToRGRaph() { + // Get the current transition + TransitionEvent currTrans = currentExecution.getLastTransition(); + // This transition is reachable from this source state when it has advanced the state + int stateId = currTrans.getStateId(); + // Add transition into R-Graph + HashSet transitionSet; + if (rGraph.containsKey(stateId)) { + transitionSet = rGraph.get(stateId); + } else { + transitionSet = new HashSet<>(); + } + // Insert into the set if it does not contain it yet + if (!transitionSet.contains(currTrans)) { + transitionSet.add(currTrans); } } @@ -582,7 +696,7 @@ public class DPORStateReducer 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 for(Integer stateId : justVisitedStates) { - if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) { + if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) { return true; } } @@ -598,7 +712,6 @@ public class DPORStateReducer extends ListenerAdapter { HashSet eventSet = new HashSet<>(); stateToEventMap.put(stateId, eventSet); } - saveExecutionToRGraph(stateId); analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); stateToChoiceCounterMap.put(stateId, choiceCounter); justVisitedStates.add(stateId); @@ -617,10 +730,9 @@ public class DPORStateReducer extends ListenerAdapter { backtrackMap.put(stateId, backtrackExecList); } // Add the new backtrack execution object - Execution newExecution = new Execution(); - newExecution.setParent(parentExecution); - newExecution.setParentChoice(parentChoice); - backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, newExecution)); + TransitionEvent backtrackTransition = new TransitionEvent(); + backtrackTransition.recordPredecessor(parentExecution, parentChoice); + backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition)); // Add to priority queue if (!backtrackStateQ.contains(stateId)) { backtrackStateQ.add(stateId); @@ -705,27 +817,26 @@ public class DPORStateReducer extends ListenerAdapter { return currentChoice; } - private void createBacktrackingPoint(int backtrackChoice, int conflictChoice, Execution execution) { + private void createBacktrackingPoint(Execution execution, int currentChoice, int conflictChoice) { // Create a new list of choices for backtrack based on the current choice and conflicting event number // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2} // for the original set {0, 1, 2, 3} Integer[] newChoiceList = new Integer[refChoices.length]; //int firstChoice = choices[actualChoice]; - ArrayList pastTrace = execution.getExecutionTrace(); - ArrayList currTrace = currentExecution.getExecutionTrace(); - int btrackChoice = currTrace.get(backtrackChoice).getChoice(); + ArrayList pastTrace = execution.getExecutionTrace(); + ArrayList currTrace = currentExecution.getExecutionTrace(); + int currChoice = currTrace.get(currentChoice).getChoice(); int stateId = pastTrace.get(conflictChoice).getStateId(); // Check if this trace has been done from this state - if (isTraceAlreadyConstructed(btrackChoice, stateId)) { + if (isTraceAlreadyConstructed(currChoice, stateId)) { return; } // Put the conflicting event numbers first and reverse the order - newChoiceList[0] = btrackChoice; - newChoiceList[1] = pastTrace.get(conflictChoice).getChoice(); + newChoiceList[0] = currChoice; // Put the rest of the event numbers into the array starting from the minimum to the upper bound - for (int i = 0, j = 2; i < refChoices.length; i++) { - if (refChoices[i] != newChoiceList[0] && refChoices[i] != newChoiceList[1]) { + for (int i = 0, j = 1; i < refChoices.length; i++) { + if (refChoices[i] != newChoiceList[0]) { newChoiceList[j] = refChoices[i]; j++; } @@ -767,8 +878,8 @@ public class DPORStateReducer extends ListenerAdapter { // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough) if (!backtrackStateQ.isEmpty()) { // Set done all the other backtrack points - for (BacktrackPoint backtrackPoint : currentExecution.getExecutionTrace()) { - backtrackPoint.getBacktrackCG().setDone(); + for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) { + backtrackTransition.getTransitionCG().setDone(); } // Reset the next backtrack point with the latest state int hiStateId = backtrackStateQ.peek(); @@ -790,64 +901,49 @@ public class DPORStateReducer extends ListenerAdapter { isEndOfExecution = true; } - private void findFirstConflictAndCreateBacktrackPoint(int currentChoice, Instruction nextInsn, String fieldClass) { - // Check for conflict (go backward from current choice and get the first conflict) - Execution execution = currentExecution; - // Choice/event we want to check for conflict against (start from actual choice) - int pastChoice = currentChoice; - // Perform backward DFS through the execution graph - while (true) { - // Get the next conflict choice - if (pastChoice > 0) { - // Case #1: check against a previous choice in the same execution for conflict - pastChoice = pastChoice - 1; - } else { // pastChoice == 0 means we are at the first BacktrackPoint of this execution path - // Case #2: check against a previous choice in a parent execution - int parentChoice = execution.getParentChoice(); - if (parentChoice > -1) { - // Get the parent execution - execution = execution.getParent(); - pastChoice = execution.getParentChoice(); - } else { - // If parent is -1 then this is the first execution (it has no parent) and we stop here - break; - } - } - // Check if a conflict is found - if (isConflictFound(nextInsn, fieldClass, currentChoice, pastChoice, execution)) { - createBacktrackingPoint(currentChoice, pastChoice, execution); - break; // Stop at the first found conflict - } - } - } + private boolean isConflictFound(Execution execution, int reachableChoice, int conflictChoice, + ReadWriteSet currRWSet) { - private boolean isConflictFound(Instruction nextInsn, String fieldClass, int currentChoice, - int pastChoice, Execution pastExecution) { - - HashMap pastRWFieldsMap = pastExecution.getReadWriteFieldsMap(); - ArrayList pastTrace = pastExecution.getExecutionTrace(); - ArrayList currTrace = currentExecution.getExecutionTrace(); + ArrayList executionTrace = execution.getExecutionTrace(); + HashMap execRWFieldsMap = execution.getReadWriteFieldsMap(); // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) - if (!pastRWFieldsMap.containsKey(pastChoice) || - currTrace.get(currentChoice).getChoice() == pastTrace.get(pastChoice).getChoice()) { + if (!execRWFieldsMap.containsKey(conflictChoice) || + executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) { return false; } - HashMap currRWFieldsMap = pastExecution.getReadWriteFieldsMap(); - ReadWriteSet rwSet = currRWFieldsMap.get(pastChoice); - int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef(); - // Check for conflicts with Write fields for both Read and Write instructions - if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) && - rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) || - (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) && - rwSet.readFieldObjectId(fieldClass) == currObjId)) { - return true; + // R/W set of choice/event that may have a potential conflict + ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice); + // 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) { + // Remove this from the read set as we are tracking per memory location + evtRWSet.removeWriteField(writeField); + return true; + } else if (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId) { + // Remove this from the write set as we are tracking per memory location + evtRWSet.removeReadField(writeField); + 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) { + // Remove this from the write set as we are tracking per memory location + evtRWSet.removeWriteField(readField); + return true; + } } + // Return false if no conflict is found return false; } - private boolean isConflictFound(int reachableChoice, int conflictChoice, Execution execution) { + private boolean isConflictFound(Execution execution, int reachableChoice, int conflictChoice) { - ArrayList executionTrace = execution.getExecutionTrace(); + ArrayList executionTrace = execution.getExecutionTrace(); HashMap execRWFieldsMap = execution.getReadWriteFieldsMap(); // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) if (!execRWFieldsMap.containsKey(conflictChoice) || @@ -947,12 +1043,9 @@ public class DPORStateReducer extends ListenerAdapter { backtrackCG.setStateId(stateId); backtrackCG.reset(); // Update current execution with this new execution - Execution newExecution = backtrackExecution.getExecution(); - if (newExecution.getParentChoice() == -1) { - // If it is -1 then that means we should start from the end of the parent trace for backward DFS - ArrayList parentTrace = newExecution.getParent().getExecutionTrace(); - newExecution.setParentChoice(parentTrace.size() - 1); - } + Execution newExecution = new Execution(); + TransitionEvent firstTransition = backtrackExecution.getFirstTransition(); + newExecution.addTransition(firstTransition); // Try to free some memory since this map is only used for the current execution currentExecution.clearCGToChoiceMap(); currentExecution = newExecution; @@ -963,142 +1056,81 @@ public class DPORStateReducer extends ListenerAdapter { } } - // --- Functions related to the reachability analysis when there is a state match + // Update backtrack sets + // 1) recursively, and + // 2) track accesses per memory location (per shared variable/field) + private void updateBacktrackSet(Execution execution, int currentChoice) { + // Choice/event we want to check for conflict against (start from actual choice) + int conflictChoice = currentChoice; + // Copy ReadWriteSet object + HashMap currRWFieldsMap = execution.getReadWriteFieldsMap(); + ReadWriteSet currRWSet = currRWFieldsMap.get(currentChoice).getCopy(); + // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle + HashSet visited = new HashSet<>(); + // Update backtrack set recursively + updateBacktrackSetRecursive(execution, currentChoice, conflictChoice, currRWSet, visited); + } - // TODO: OPTIMIZATION! - // Check and make sure that state ID and choice haven't been explored for this trace - private boolean isAlreadyChecked(HashSet checkedStateIdAndChoice, BacktrackPoint backtrackPoint) { - int stateId = backtrackPoint.getStateId(); - int choice = backtrackPoint.getChoice(); - StringBuilder sb = new StringBuilder(); - sb.append(stateId); - sb.append(':'); - sb.append(choice); - // Check if the trace has been constructed as a backtrack point for this state - if (checkedStateIdAndChoice.contains(sb.toString())) { - return true; + private void updateBacktrackSetRecursive(Execution execution, int currentChoice, int conflictChoice, + ReadWriteSet currRWSet, HashSet visited) { + // Halt when we have found the first read/write conflicts for all memory locations + if (currRWSet.isEmpty()) { + return; + } + TransitionEvent confTrans = execution.getExecutionTrace().get(conflictChoice); + // Halt when we have visited this transition (in a cycle) + if (visited.contains(confTrans)) { + return; + } + visited.add(confTrans); + // Explore all predecessors + for (Predecessor predecessor : confTrans.getPredecessors()) { + // Get the predecessor (previous conflict choice) + conflictChoice = predecessor.getPredecessorChoice(); + execution = predecessor.getPredecessorExecution(); + // Check if a conflict is found + if (isConflictFound(execution, currentChoice, conflictChoice, currRWSet)) { + createBacktrackingPoint(execution, currentChoice, conflictChoice); + } + // Continue performing DFS if conflict is not found + updateBacktrackSetRecursive(execution, currentChoice, conflictChoice, currRWSet, visited); } - checkedStateIdAndChoice.add(sb.toString()); - return false; } - // 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 + // --- Functions related to the reachability analysis when there is a state match + private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { // Perform this analysis only when: // 1) there is a state match, // 2) this is not during a switch to a new execution, // 3) at least 2 choices/events have been explored (choiceCounter > 1), - // 4) the matched state has been encountered in the current execution, and - // 5) state > 0 (state 0 is for boolean CG) + // 4) state > 0 (state 0 is for boolean CG) if (!vm.isNewState() && !isEndOfExecution && choiceCounter > 1 && (stateId > 0)) { if (currVisitedStates.contains(stateId)) { - // Update the backtrack sets in the cycle - updateBacktrackSetsInCycle(stateId); + // Get the backtrack point from the current execution + TransitionEvent transition = currentExecution.getTransitionFromState(stateId); + transition.recordPredecessor(currentExecution, choiceCounter - 1); + updateBacktrackSetsFromPreviousExecution(stateId); } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution - // Update the backtrack sets in a previous execution - updateBacktrackSetsInPreviousExecutions(stateId); - } - } - } - - // Get the start event for the past execution trace when there is a state matched from a past execution - private int getPastConflictChoice(int stateId, ArrayList pastBacktrackPointList) { - // Iterate and find the first occurrence of the state ID - // It is guaranteed that a choice should be found because the state ID is in the list - int pastConfChoice = 0; - for(int i = 0; i getReachableStateIds(Set stateIds, int stateId) { - // Only include state IDs equal or greater than the input stateId: these are reachable states - ArrayList sortedStateIds = new ArrayList<>(); - for(Integer stId : stateIds) { - if (stId >= stateId) { - sortedStateIds.add(stId); - } - } - Collections.sort(sortedStateIds); - return sortedStateIds; - } - - // Update the backtrack sets in the cycle - private void updateBacktrackSetsInCycle(int stateId) { - // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts - int reachableChoice = stateToChoiceCounterMap.get(stateId); - int cycleEndChoice = choiceCounter - 1; - // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward) - while (reachableChoice < cycleEndChoice) { - for (int conflictChoice = reachableChoice + 1; conflictChoice <= cycleEndChoice; conflictChoice++) { - if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) { - createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution); - } - } - reachableChoice++; - } - } - - // Update the backtrack sets in a previous execution - private void updateBacktrackSetsInPreviousExecution(Execution rExecution, int stateId, - HashSet checkedStateIdAndChoice) { - // Find the choice/event that marks the start of the subtrace from the previous execution - ArrayList pastExecutionTrace = rExecution.getExecutionTrace(); - HashMap pastReadWriteFieldsMap = rExecution.getReadWriteFieldsMap(); - int pastConfChoice = getPastConflictChoice(stateId, pastExecutionTrace); - int reachableChoice = choiceCounter; - // Iterate from the starting point until the end of the past execution trace - while (pastConfChoice < pastExecutionTrace.size() - 1) { // BacktrackPoint list always has a surplus of 1 - // Get the info of the event from the past execution trace - BacktrackPoint confBtrackPoint = pastExecutionTrace.get(pastConfChoice); - if (!isAlreadyChecked(checkedStateIdAndChoice, confBtrackPoint)) { - ReadWriteSet rwSet = pastReadWriteFieldsMap.get(pastConfChoice); - // Append this event to the current list and map - ArrayList currentTrace = currentExecution.getExecutionTrace(); - HashMap currRWFieldsMap = currentExecution.getReadWriteFieldsMap(); - currentTrace.add(confBtrackPoint); - currRWFieldsMap.put(choiceCounter, rwSet); - for (int conflictChoice = reachableChoice - 1; conflictChoice >= 0; conflictChoice--) { - if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) { - createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution); - } + // Update past executions with a predecessor + HashSet reachableTransitions = rGraph.get(stateId); + for(TransitionEvent transition : reachableTransitions) { + Execution execution = transition.getExecution(); + transition.recordPredecessor(execution, choiceCounter - 1); } - // Remove this event to replace it with a new one - currentTrace.remove(currentTrace.size() - 1); - currRWFieldsMap.remove(choiceCounter); + updateBacktrackSetsFromPreviousExecution(stateId); } - pastConfChoice++; } } - // Update the backtrack sets in previous executions - private void updateBacktrackSetsInPreviousExecutions(int stateId) { - // Don't check a past trace twice! - HashSet checkedTrace = new HashSet<>(); - // Don't check the same event twice for a revisited state - HashSet checkedStateIdAndChoice = new HashSet<>(); - // Get sorted reachable state IDs - ArrayList reachableStateIds = getReachableStateIds(rGraph.keySet(), stateId); - // Iterate from this state ID until the biggest state ID - for(Integer stId : reachableStateIds) { - // Find the right reachability graph object that contains the stateId - ArrayList rExecutions = rGraph.get(stId); - for (Execution rExecution : rExecutions) { - if (!checkedTrace.contains(rExecution)) { - updateBacktrackSetsInPreviousExecution(rExecution, stateId, checkedStateIdAndChoice); - checkedTrace.add(rExecution); - } - } + // Update the backtrack sets from previous executions + private void updateBacktrackSetsFromPreviousExecution(int stateId) { + // Collect all the reachable transitions from R-Graph + HashSet reachableTransitions = rGraph.get(stateId); + for(TransitionEvent transition : reachableTransitions) { + Execution execution = transition.getExecution(); + int currentChoice = transition.getChoiceCounter(); + updateBacktrackSet(execution, currentChoice); } } } -- 2.34.1