import gov.nasa.jpf.ListenerAdapter;
import gov.nasa.jpf.jvm.bytecode.INVOKEINTERFACE;
import gov.nasa.jpf.jvm.bytecode.JVMFieldInstruction;
+import gov.nasa.jpf.report.Publisher;
import gov.nasa.jpf.search.Search;
import gov.nasa.jpf.vm.*;
import gov.nasa.jpf.vm.bytecode.ReadInstruction;
public class DPORStateReducerWithSummary extends ListenerAdapter {
// Information printout fields for verbose mode
+ private long startTime;
+ private long timeout;
private boolean verboseMode;
private boolean stateReductionMode;
private final PrintWriter out;
private HashSet<ClassInfo> nonRelevantClasses;// Class info objects of non-relevant classes
private HashSet<FieldInfo> nonRelevantFields; // Field info objects of non-relevant fields
private HashSet<FieldInfo> relevantFields; // Field info objects of relevant fields
- private HashMap<Integer, HashSet<Integer>> stateToEventMap;
+ private HashMap<Integer, HashSet<Integer>> stateToEventMap; // Map state ID to events
// Data structure to analyze field Read/Write accesses and conflicts
private HashMap<Integer, LinkedList<BacktrackExecution>> backtrackMap; // Track created backtracking points
private PriorityQueue<Integer> backtrackStateQ; // Heap that returns the latest state
private Execution currentExecution; // Holds the information about the current execution
private HashMap<Integer, HashSet<Integer>> doneBacktrackMap; // Record state ID and trace already constructed
+ private MainSummary mainSummary; // Main summary (M) for state ID, event, and R/W set
+ private HashMap<Integer, PredecessorInfo> stateToPredInfo; // Predecessor info indexed by state ID
private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
private RGraph rGraph; // R-Graph for past executions
- private MainSummary mainSummary; // Main summary (M) for state ID, event, and R/W set
// Boolean states
private boolean isBooleanCGFlipped;
private boolean isEndOfExecution;
+ private boolean isNotCheckedForEventsYet;
// Statistics
private int numOfTransitions;
+ private HashMap<Integer, HashSet<Integer>> stateToUniqueTransMap;
public DPORStateReducerWithSummary(Config config, JPF jpf) {
verboseMode = config.getBoolean("printout_state_transition", false);
}
}
isBooleanCGFlipped = false;
- numOfTransitions = 0;
- nonRelevantClasses = new HashSet<>();
- nonRelevantFields = new HashSet<>();
- relevantFields = new HashSet<>();
- restorableStateMap = new HashMap<>();
+ isNotCheckedForEventsYet = true;
mainSummary = new MainSummary();
+ numOfTransitions = 0;
+ nonRelevantClasses = new HashSet<>();
+ nonRelevantFields = new HashSet<>();
+ relevantFields = new HashSet<>();
+ restorableStateMap = new HashMap<>();
+ stateToPredInfo = new HashMap<>();
+ stateToUniqueTransMap = new HashMap<>();
initializeStatesVariables();
+
+ // Timeout input from config is in minutes, so we need to convert into millis
+ timeout = config.getInt("timeout", 0) * 60 * 1000;
+ startTime = System.currentTimeMillis();
}
@Override
@Override
public void searchFinished(Search search) {
if (verboseMode) {
+ int summaryOfUniqueTransitions = summarizeUniqueTransitions();
out.println("\n==> DEBUG: ----------------------------------- search finished");
- out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode);
- out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
+ out.println("\n==> DEBUG: State reduction mode : " + stateReductionMode);
+ if (choices != null) {
+ out.println("\n==> DEBUG: Number of events : " + choices.length);
+ } else {
+ // Without DPOR we don't have choices being assigned with a CG
+ out.println("\n==> DEBUG: Number of events : 0");
+ }
+ out.println("\n==> DEBUG: Number of transitions : " + numOfTransitions);
+ out.println("\n==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
out.println("\n==> DEBUG: ----------------------------------- search finished" + "\n");
- fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode);
- fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+ fileWriter.println("==> DEBUG: State reduction mode : " + stateReductionMode);
+ if (choices != null) {
+ fileWriter.println("==> DEBUG: Number of events : " + choices.length);
+ } else {
+ // Without DPOR we don't have choices being assigned with a CG
+ fileWriter.println("==> DEBUG: Number of events : 0");
+ }
+ fileWriter.println("==> DEBUG: Number of transitions : " + numOfTransitions);
+ fileWriter.println("==> DEBUG: Number of unique transitions (DPOR) : " + summaryOfUniqueTransitions);
fileWriter.println();
fileWriter.close();
}
@Override
public void choiceGeneratorRegistered(VM vm, ChoiceGenerator<?> nextCG, ThreadInfo currentThread, Instruction executedInstruction) {
+ if (isNotCheckedForEventsYet) {
+ // Check if this benchmark has no events
+ if (nextCG instanceof IntChoiceFromSet) {
+ IntChoiceFromSet icsCG = (IntChoiceFromSet) nextCG;
+ Integer[] cgChoices = icsCG.getAllChoices();
+ if (cgChoices.length == 2 && cgChoices[0] == 0 && cgChoices[1] == -1) {
+ // This means the benchmark only has 2 choices, i.e., 0 and -1 which means that it has no events
+ stateReductionMode = false;
+ }
+ isNotCheckedForEventsYet = false;
+ }
+ }
if (stateReductionMode) {
// Initialize with necessary information from the CG
if (nextCG instanceof IntChoiceFromSet) {
// 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
- if (terminateCurrentExecution() && choiceCounter > 0) {
+ if (choiceCounter > 0 && terminateCurrentExecution()) {
exploreNextBacktrackPoints(vm, icsCG);
} else {
+ // We only count IntChoiceFromSet CGs
numOfTransitions++;
+ countUniqueTransitions(vm.getStateId(), icsCG.getNextChoice());
}
// Map state to event
mapStateToEvent(icsCG.getNextChoice());
choiceCounter++;
}
} else {
- numOfTransitions++;
+ // We only count IntChoiceFromSet CGs
+ if (currentCG instanceof IntChoiceFromSet) {
+ numOfTransitions++;
+ }
}
}
@Override
public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
+ // Check the timeout
+ if (timeout > 0) {
+ if (System.currentTimeMillis() - startTime > timeout) {
+ StringBuilder sbTimeOut = new StringBuilder();
+ sbTimeOut.append("Execution timeout: " + (timeout / (60 * 1000)) + " minutes have passed!");
+ Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sbTimeOut.toString());
+ ti.setNextPC(nextIns);
+ }
+ }
+
if (stateReductionMode) {
if (!isEndOfExecution) {
- // Has to be initialized and a integer CG
+ // Has to be initialized and it is a integer CG
ChoiceGenerator<?> cg = vm.getChoiceGenerator();
if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
int currentChoice = choiceCounter - 1; // Accumulative choice w.r.t the current trace
}
}
+ // This class is a representation of a state.
+ // It stores the predecessors to a state.
+ // TODO: We also have stateToEventMap, restorableStateMap, and doneBacktrackMap that has state Id as HashMap key.
+ private class PredecessorInfo {
+ private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
+ private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
+ // Memorize event and choice number to not record them twice
+
+ public PredecessorInfo() {
+ predecessors = new HashSet<>();
+ recordedPredecessors = new HashMap<>();
+ }
+
+ public HashSet<Predecessor> getPredecessors() {
+ return predecessors;
+ }
+
+ private boolean isRecordedPredecessor(Execution execution, int choice) {
+ // See if we have recorded this predecessor earlier
+ HashSet<Integer> recordedChoices;
+ if (recordedPredecessors.containsKey(execution)) {
+ recordedChoices = recordedPredecessors.get(execution);
+ if (recordedChoices.contains(choice)) {
+ return true;
+ }
+ } else {
+ recordedChoices = new HashSet<>();
+ recordedPredecessors.put(execution, recordedChoices);
+ }
+ // Record the choice if we haven't seen it
+ recordedChoices.add(choice);
+
+ return false;
+ }
+
+ public void recordPredecessor(Execution execution, int choice) {
+ if (!isRecordedPredecessor(execution, choice)) {
+ predecessors.add(new Predecessor(choice, execution));
+ }
+ }
+ }
+
// This class compactly stores transitions:
// 1) CG,
// 2) state ID,
private int choice; // Choice chosen at this transition
private int choiceCounter; // Choice counter at this transition
private Execution execution; // The execution where this transition belongs
- private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
- private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
- // Memorize event and choice number to not record them twice
private int stateId; // State at this transition
private IntChoiceFromSet transitionCG; // CG at this transition
choice = 0;
choiceCounter = 0;
execution = null;
- predecessors = new HashSet<>();
- recordedPredecessors = new HashMap<>();
stateId = 0;
transitionCG = null;
}
return execution;
}
- public HashSet<Predecessor> getPredecessors() {
- return predecessors;
- }
-
public int getStateId() {
return stateId;
}
public IntChoiceFromSet getTransitionCG() { return transitionCG; }
- private boolean isRecordedPredecessor(Execution execution, int choice) {
- // See if we have recorded this predecessor earlier
- HashSet<Integer> recordedChoices;
- if (recordedPredecessors.containsKey(execution)) {
- recordedChoices = recordedPredecessors.get(execution);
- if (recordedChoices.contains(choice)) {
- return true;
- }
- } else {
- recordedChoices = new HashSet<>();
- recordedPredecessors.put(execution, recordedChoices);
- }
- // Record the choice if we haven't seen it
- recordedChoices.add(choice);
-
- return false;
- }
-
- public void recordPredecessor(Execution execution, int choice) {
- if (!isRecordedPredecessor(execution, choice)) {
- predecessors.add(new Predecessor(choice, execution));
- }
- }
-
public void setChoice(int cho) {
choice = cho;
}
execution = exec;
}
- public void setPredecessors(HashSet<Predecessor> preds) {
- predecessors = new HashSet<>(preds);
- }
-
public void setStateId(int stId) {
stateId = stId;
}
public Set<Integer> getEventChoicesAtStateId(int stateId) {
HashMap<Integer, ReadWriteSet> stateSummary = mainSummary.get(stateId);
- return stateSummary.keySet();
+ // Return a new set since this might get updated concurrently
+ return new HashSet<>(stateSummary.keySet());
}
public ReadWriteSet getRWSetForEventChoiceAtState(int eventChoice, int stateId) {
return stateSummary.get(eventChoice);
}
+ public Set<Integer> getStateIds() {
+ return mainSummary.keySet();
+ }
+
private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
// Combine the same write accesses and record in the recordedRWSet
HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
// If the state Id has existed, find the event choice:
// 1) If the event choice has not existed, insert the ReadWriteSet object
// 2) If the event choice has existed, perform union between the two ReadWriteSet objects
- HashMap<Integer, ReadWriteSet> stateSummary;
- if (!mainSummary.containsKey(stateId)) {
- stateSummary = new HashMap<>();
- stateSummary.put(eventChoice, rwSet.getCopy());
- mainSummary.put(stateId, stateSummary);
- } else {
- stateSummary = mainSummary.get(stateId);
- if (!stateSummary.containsKey(eventChoice)) {
+ if (!rwSet.isEmpty()) {
+ HashMap<Integer, ReadWriteSet> stateSummary;
+ if (!mainSummary.containsKey(stateId)) {
+ stateSummary = new HashMap<>();
stateSummary.put(eventChoice, rwSet.getCopy());
+ mainSummary.put(stateId, stateSummary);
} else {
- rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
+ stateSummary = mainSummary.get(stateId);
+ if (!stateSummary.containsKey(eventChoice)) {
+ stateSummary.put(eventChoice, rwSet.getCopy());
+ } else {
+ rwSet = performUnion(stateSummary.get(eventChoice), rwSet);
+ }
}
}
return rwSet;
} else {
transition = new TransitionEvent();
currentExecution.addTransition(transition);
- transition.recordPredecessor(currentExecution, choiceCounter - 1);
+ addPredecessors(stateId);
}
transition.setExecution(currentExecution);
transition.setTransitionCG(icsCG);
return transition;
}
+ // --- Functions related to statistics counting
+ // Count unique state IDs
+ private void countUniqueTransitions(int stateId, int nextChoiceValue) {
+ HashSet<Integer> events;
+ // Get the set of events
+ if (!stateToUniqueTransMap.containsKey(stateId)) {
+ events = new HashSet<>();
+ stateToUniqueTransMap.put(stateId, events);
+ } else {
+ events = stateToUniqueTransMap.get(stateId);
+ }
+ // Insert the event
+ if (!events.contains(nextChoiceValue)) {
+ events.add(nextChoiceValue);
+ }
+ }
+
+ // Summarize unique state IDs
+ private int summarizeUniqueTransitions() {
+ // Just count the set size of each of entry map and sum them up
+ int numOfUniqueTransitions = 0;
+ for (Map.Entry<Integer,HashSet<Integer>> entry : stateToUniqueTransMap.entrySet()) {
+ numOfUniqueTransitions = numOfUniqueTransitions + entry.getValue().size();
+ }
+
+ return numOfUniqueTransitions;
+ }
+
// --- Functions related to cycle detection and reachability graph
// Detect cycles in the current execution/trace
choiceCounter = 0;
maxEventChoice = 0;
// Cycle tracking
- currVisitedStates = new HashMap<>();
- justVisitedStates = new HashSet<>();
- prevVisitedStates = new HashSet<>();
- stateToEventMap = new HashMap<>();
+ if (!isBooleanCGFlipped) {
+ currVisitedStates = new HashMap<>();
+ justVisitedStates = new HashSet<>();
+ prevVisitedStates = new HashSet<>();
+ stateToEventMap = new HashMap<>();
+ } else {
+ currVisitedStates.clear();
+ justVisitedStates.clear();
+ prevVisitedStates.clear();
+ stateToEventMap.clear();
+ }
// Backtracking
- backtrackMap = new HashMap<>();
+ if (!isBooleanCGFlipped) {
+ backtrackMap = new HashMap<>();
+ } else {
+ backtrackMap.clear();
+ }
backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
currentExecution = new Execution();
currentExecution.addTransition(new TransitionEvent()); // Always start with 1 backtrack point
- doneBacktrackMap = new HashMap<>();
+ if (!isBooleanCGFlipped) {
+ doneBacktrackMap = new HashMap<>();
+ } else {
+ doneBacktrackMap.clear();
+ }
rGraph = new RGraph();
// Booleans
isEndOfExecution = false;
// 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
boolean terminate = false;
+ Set<Integer> mainStateIds = mainSummary.getStateIds();
for(Integer stateId : justVisitedStates) {
- // We perform updates on backtrack sets for every
- if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
- updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
- terminate = true;
- }
- // If frequency > 1 then this means we have visited this stateId more than once
- if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
- updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+ // We exclude states that are produced by other CGs that are not integer CG
+ // When we encounter these states, then we should also encounter the corresponding integer CG state ID
+ if (mainStateIds.contains(stateId)) {
+ // We perform updates on backtrack sets for every
+ if (prevVisitedStates.contains(stateId) || completeFullCycle(stateId)) {
+ updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+ terminate = true;
+ }
+ // If frequency > 1 then this means we have visited this stateId more than once in the current execution
+ if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) {
+ updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1);
+ }
}
}
return terminate;
}
// Add the new backtrack execution object
TransitionEvent backtrackTransition = new TransitionEvent();
- backtrackTransition.setPredecessors(conflictTransition.getPredecessors());
backtrackExecList.addFirst(new BacktrackExecution(newChoiceList, backtrackTransition));
// Add to priority queue
if (!backtrackStateQ.contains(stateId)) {
}
}
+ private void addPredecessors(int stateId) {
+ PredecessorInfo predecessorInfo;
+ if (!stateToPredInfo.containsKey(stateId)) {
+ predecessorInfo = new PredecessorInfo();
+ stateToPredInfo.put(stateId, predecessorInfo);
+ } else { // This is a new state Id
+ predecessorInfo = stateToPredInfo.get(stateId);
+ }
+ predecessorInfo.recordPredecessor(currentExecution, choiceCounter - 1);
+ }
+
// Analyze Read/Write accesses that are directly invoked on fields
private void analyzeReadWriteAccesses(Instruction executedInsn, int currentChoice) {
// Get the field info
}
private void exploreNextBacktrackPoints(VM vm, IntChoiceFromSet icsCG) {
- // Check if we are reaching the end of our execution: no more backtracking points to explore
- // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
- if (!backtrackStateQ.isEmpty()) {
- // Set done all the other backtrack points
- for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
+ // Check if we are reaching the end of our execution: no more backtracking points to explore
+ // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
+ if (!backtrackStateQ.isEmpty()) {
+ // Set done all the other backtrack points
+ for (TransitionEvent backtrackTransition : currentExecution.getExecutionTrace()) {
backtrackTransition.getTransitionCG().setDone();
- }
- // Reset the next backtrack point with the latest state
- int hiStateId = backtrackStateQ.peek();
- // Restore the state first if necessary
- if (vm.getStateId() != hiStateId) {
- RestorableVMState restorableState = restorableStateMap.get(hiStateId);
- vm.restoreState(restorableState);
- }
- // Set the backtrack CG
- IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
- setBacktrackCG(hiStateId, backtrackCG);
- } else {
- // Set done this last CG (we save a few rounds)
- icsCG.setDone();
- }
- // Save all the visited states when starting a new execution of trace
- prevVisitedStates.addAll(currVisitedStates.keySet());
- // This marks a transitional period to the new CG
- isEndOfExecution = true;
+ }
+ // Reset the next backtrack point with the latest state
+ int hiStateId = backtrackStateQ.peek();
+ // Restore the state first if necessary
+ if (vm.getStateId() != hiStateId) {
+ RestorableVMState restorableState = restorableStateMap.get(hiStateId);
+ vm.restoreState(restorableState);
+ }
+ // Set the backtrack CG
+ IntChoiceFromSet backtrackCG = (IntChoiceFromSet) vm.getChoiceGenerator();
+ setBacktrackCG(hiStateId, backtrackCG);
+ } else {
+ // Set done this last CG (we save a few rounds)
+ icsCG.setDone();
+ }
+ // Save all the visited states when starting a new execution of trace
+ prevVisitedStates.addAll(currVisitedStates.keySet());
+ // This marks a transitional period to the new CG
+ isEndOfExecution = true;
}
private boolean isConflictFound(int eventChoice, Execution conflictExecution, int conflictChoice,
return false;
}
- private ReadWriteSet getReadWriteSet(int currentChoice) {
- // Do the analysis to get Read and Write accesses to fields
- ReadWriteSet rwSet;
- // We already have an entry
- HashMap<Integer, ReadWriteSet> currReadWriteFieldsMap = currentExecution.getReadWriteFieldsMap();
- if (currReadWriteFieldsMap.containsKey(currentChoice)) {
- rwSet = currReadWriteFieldsMap.get(currentChoice);
- } else { // We need to create a new entry
- rwSet = new ReadWriteSet();
- currReadWriteFieldsMap.put(currentChoice, rwSet);
- }
- return rwSet;
- }
-
private boolean isFieldExcluded(Instruction executedInsn) {
// Get the field info
FieldInfo fieldInfo = ((JVMFieldInstruction) executedInsn).getFieldInfo();
return false;
}
+ private HashSet<Predecessor> getPredecessors(int stateId) {
+ // Get a set of predecessors for this state ID
+ HashSet<Predecessor> predecessors;
+ if (stateToPredInfo.containsKey(stateId)) {
+ PredecessorInfo predecessorInfo = stateToPredInfo.get(stateId);
+ predecessors = predecessorInfo.getPredecessors();
+ } else {
+ predecessors = new HashSet<>();
+ }
+
+ return predecessors;
+ }
+
+ private ReadWriteSet getReadWriteSet(int currentChoice) {
+ // Do the analysis to get Read and Write accesses to fields
+ ReadWriteSet rwSet;
+ // We already have an entry
+ HashMap<Integer, ReadWriteSet> currReadWriteFieldsMap = currentExecution.getReadWriteFieldsMap();
+ if (currReadWriteFieldsMap.containsKey(currentChoice)) {
+ rwSet = currReadWriteFieldsMap.get(currentChoice);
+ } else { // We need to create a new entry
+ rwSet = new ReadWriteSet();
+ currReadWriteFieldsMap.put(currentChoice, rwSet);
+ }
+ return rwSet;
+ }
+
// Reset data structure for each new execution
private void resetStatesForNewExecution(IntChoiceFromSet icsCG, VM vm) {
if (choices == null || choices != icsCG.getAllChoices()) {
choices = icsCG.getAllChoices();
refChoices = copyChoices(choices);
// Clear data structures
- currVisitedStates = new HashMap<>();
- stateToEventMap = new HashMap<>();
+ currVisitedStates.clear();
+ stateToEventMap.clear();
isEndOfExecution = false;
}
}
private void updateBacktrackSetDFS(Execution execution, int currentChoice, int conflictEventChoice,
ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
- // Halt when we have found the first read/write conflicts for all memory locations
- if (currRWSet.isEmpty()) {
- return;
- }
TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
// Record this transition into the state summary of main summary
currRWSet = mainSummary.updateStateSummary(currTrans.getStateId(), conflictEventChoice, currRWSet);
return;
}
visited.add(currTrans);
- // Explore all predecessors
- for (Predecessor predecessor : currTrans.getPredecessors()) {
- // Get the predecessor (previous conflict choice)
- int predecessorChoice = predecessor.getChoice();
- Execution predecessorExecution = predecessor.getExecution();
- // Push up one happens-before transition
- int newConflictEventChoice = conflictEventChoice;
- // Check if a conflict is found
- if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, currRWSet)) {
- createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
- // We need to extract the pushed happens-before event choice from the predecessor execution and choice
- newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+ // Check the predecessors only if the set is not empty
+ if (!currRWSet.isEmpty()) {
+ // Explore all predecessors
+ for (Predecessor predecessor : getPredecessors(currTrans.getStateId())) {
+ // Get the predecessor (previous conflict choice)
+ int predecessorChoice = predecessor.getChoice();
+ Execution predecessorExecution = predecessor.getExecution();
+ // Push up one happens-before transition
+ int newConflictEventChoice = conflictEventChoice;
+ // Check if a conflict is found
+ ReadWriteSet newCurrRWSet = currRWSet.getCopy();
+ if (isConflictFound(conflictEventChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) {
+ createBacktrackingPoint(conflictEventChoice, predecessorExecution, predecessorChoice);
+ // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+ newConflictEventChoice = predecessorExecution.getExecutionTrace().get(predecessorChoice).getChoice();
+ }
+ // Continue performing DFS if conflict is not found
+ updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
+ newCurrRWSet, visited);
}
- // Continue performing DFS if conflict is not found
- updateBacktrackSetDFS(predecessorExecution, predecessorChoice, newConflictEventChoice,
- currRWSet, visited);
}
}
if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) {
if ((currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) ||
prevVisitedStates.contains(stateId)) {
- // Update reachable transitions in the graph with a predecessor
- HashSet<TransitionEvent> reachableTransitions = rGraph.getReachableTransitionsAtState(stateId);
- for (TransitionEvent transition : reachableTransitions) {
- transition.recordPredecessor(currentExecution, choiceCounter - 1);
- }
+ // Record a new predecessor for a revisited state
+ addPredecessors(stateId);
}
}
}
Set<Integer> eventChoicesAtStateId = mainSummary.getEventChoicesAtStateId(stateId);
for (Integer eventChoice : eventChoicesAtStateId) {
// Get the ReadWriteSet object for this event at state ID
- ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId);
+ ReadWriteSet rwSet = mainSummary.getRWSetForEventChoiceAtState(eventChoice, stateId).getCopy();
+ // We have to first check for conflicts between the event and the current transition
+ // Push up one happens-before transition
+ int conflictEventChoice = eventChoice;
+ if (isConflictFound(eventChoice, currExecution, currChoice, rwSet)) {
+ createBacktrackingPoint(eventChoice, currExecution, currChoice);
+ // We need to extract the pushed happens-before event choice from the predecessor execution and choice
+ conflictEventChoice = currExecution.getExecutionTrace().get(currChoice).getChoice();
+ }
// Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle
HashSet<TransitionEvent> visited = new HashSet<>();
// Update the backtrack sets recursively
- updateBacktrackSetDFS(currExecution, currChoice, eventChoice, rwSet, visited);
+ updateBacktrackSetDFS(currExecution, currChoice, conflictEventChoice, rwSet, visited);
}
}
}