// DPOR-related fields
// Basic information
private Integer[] choices;
- private Integer[] refChoices;
+ private Integer[] refChoices; // Second reference to a copy of choices (choices may be modified for fair scheduling)
private int choiceCounter;
- private int lastCGStateId; // Record the state of the currently active CG
private int maxEventChoice;
// Data structure to track the events seen by each state to track cycles (containing all events) for termination
private HashSet<Integer> currVisitedStates; // States being visited in the current execution
// Data structure to analyze field Read/Write accesses and conflicts
private HashMap<Integer, LinkedList<Integer[]>> backtrackMap; // Track created backtracking points
private PriorityQueue<Integer> backtrackStateQ; // Heap that returns the latest state
- private ArrayList<IntChoiceFromSet> cgList; // Record CGs for backtracking points
+ private ArrayList<BacktrackPoint> backtrackPointList; // Record backtrack points (CG and choice)
private HashMap<Integer, IntChoiceFromSet> cgMap; // Maps state IDs to CGs
private HashMap<Integer, HashSet<Integer>> conflictPairMap; // Record conflicting events
private HashSet<String> doneBacktrackSet; // Record state ID and trace that are done
// Boolean states
private boolean isBooleanCGFlipped;
- private boolean isFirstResetDone;
private boolean isEndOfExecution;
public DPORStateReducer(Config config, JPF jpf) {
int choiceIndex = choiceCounter % choices.length;
icsCG.advance(choices[choiceIndex]);
// Index the ChoiceGenerator to set backtracking points
- cgList.add(icsCG);
+ BacktrackPoint backtrackPoint = new BacktrackPoint(icsCG, choices[choiceIndex]);
+ backtrackPointList.add(backtrackPoint);
} else {
// Set done all CGs while transitioning to a new execution
icsCG.setDone();
updateVODGraph(icsCG.getNextChoice());
// Check if we have seen this state or this state contains cycles that involve all events
if (terminateCurrentExecution()) {
- exploreNextBacktrackPoints(icsCG, vm);
+ exploreNextBacktrackPoints(icsCG);
}
justVisitedStates.clear();
choiceCounter++;
// This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices
private class BacktrackPoint {
private IntChoiceFromSet backtrackCG; // CG to backtrack from
- private Integer[] backtrackChoices; // Choices to set for this backtrack CG
+ private int choice; // Choice chosen at this backtrack point
- public BacktrackPoint(IntChoiceFromSet cg, Integer[] choices) {
+ public BacktrackPoint(IntChoiceFromSet cg, int cho) {
backtrackCG = cg;
- backtrackChoices = choices;
+ choice = cho;
}
public IntChoiceFromSet getBacktrackCG() {
return backtrackCG;
}
- public Integer[] getBacktrackChoices() {
- return backtrackChoices;
+ public int getChoice() {
+ return choice;
}
}
choices = null;
refChoices = null;
choiceCounter = 0;
- lastCGStateId = 0;
maxEventChoice = 0;
// Cycle tracking
currVisitedStates = new HashSet<>();
// Backtracking
backtrackMap = new HashMap<>();
backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder());
- cgList = new ArrayList<>();
+ backtrackPointList = new ArrayList<>();
cgMap = new HashMap<>();
conflictPairMap = new HashMap<>();
doneBacktrackSet = new HashSet<>();
vodGraphMap = new HashMap<>();
// Booleans
isEndOfExecution = false;
- isFirstResetDone = false;
}
private void mapStateToEvent(int nextChoiceValue) {
Integer[] newChoiceList = new Integer[refChoices.length];
// Put the conflicting event numbers first and reverse the order
int actualCurrCho = currentChoice % refChoices.length;
- int actualConfEvtNum = confEvtNum % refChoices.length;
- // We use the actual choices here in case they have been modified/adjusted
+ // We use the actual choices here in case they have been modified/adjusted by the fair scheduling method
newChoiceList[0] = choices[actualCurrCho];
- newChoiceList[1] = choices[actualConfEvtNum];
+ newChoiceList[1] = backtrackPointList.get(confEvtNum).getChoice();
// 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]) {
j++;
}
}
- // Record the backtracking point in the stack as well
- IntChoiceFromSet backtrackCG = cgList.get(confEvtNum);
+ // Get the backtrack CG for this backtrack point
+ IntChoiceFromSet backtrackCG = backtrackPointList.get(confEvtNum).getBacktrackCG();
// Check if this trace has been done starting from this state
if (isTraceConstructed(newChoiceList, backtrackCG)) {
return;
return false;
}
- private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG, VM vm) {
+ private void exploreNextBacktrackPoints(IntChoiceFromSet icsCG) {
// We can start exploring the next backtrack point after the current CG is advanced at least once
if (icsCG.getNextChoiceIndex() > 0) {
+ HashSet<IntChoiceFromSet> backtrackCGs = new HashSet<>(cgMap.values());
// Check if we are reaching the end of our execution: no more backtracking points to explore
- if (!backtrackMap.isEmpty()) {
- setNextBacktrackPoint(icsCG);
+ // cgMap, backtrackMap, backtrackStateQ are updated simultaneously (checking backtrackStateQ is enough)
+ if (!backtrackStateQ.isEmpty()) {
+ // Reset the next CG with the latest state
+ int hiStateId = backtrackStateQ.peek();
+ // Check with the current state and if it's lower than the highest state, we defer to this lower state
+ int currStateId = icsCG.getStateId();
+ if (currStateId < hiStateId && cgMap.keySet().contains(currStateId)) {
+ hiStateId = currStateId;
+ }
+ setBacktrackCG(hiStateId, backtrackCGs);
+ }
+ // Clear unused CGs
+ for (BacktrackPoint backtrackPoint : backtrackPointList) {
+ IntChoiceFromSet cg = backtrackPoint.getBacktrackCG();
+ if (!backtrackCGs.contains(cg)) {
+ cg.setDone();
+ }
}
+ backtrackPointList.clear();
// Save all the visited states when starting a new execution of trace
prevVisitedStates.addAll(currVisitedStates);
currVisitedStates.clear();
}
private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) {
- int actualEvtCntr = eventCounter % refChoices.length;
+
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] == choices[actualEvtCntr]) {
+ if (!readWriteFieldsMap.containsKey(eventCounter) ||
+ choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) {
return false;
}
ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter);
choiceCounter = 0;
choices = icsCG.getAllChoices();
refChoices = copyChoices(choices);
- lastCGStateId = icsCG.getStateId();
// Clearing data structures
conflictPairMap.clear();
readWriteFieldsMap.clear();
stateToEventMap.clear();
isEndOfExecution = false;
- // Adding this CG as the first CG for this execution
- cgList.add(icsCG);
+ // Adding this CG as the first backtrack point for this execution
+ backtrackPointList.add(new BacktrackPoint(icsCG, choices[0]));
}
}
- private void setBacktrackCG(int stateId) {
+ private void setBacktrackCG(int stateId, HashSet<IntChoiceFromSet> backtrackCGs) {
// Set a backtrack CG based on a state ID
IntChoiceFromSet backtrackCG = cgMap.get(stateId);
+ // Need to reset the CGs first so that the CG last reset will be chosen next
+ for (IntChoiceFromSet cg : backtrackCGs) {
+ if (cg != backtrackCG && cg.getNextChoiceIndex() > -1) {
+ cg.reset();
+ }
+ }
LinkedList<Integer[]> backtrackChoices = backtrackMap.get(stateId);
backtrackCG.setNewValues(backtrackChoices.removeLast()); // Get the last from the queue
backtrackCG.reset();
}
}
- private void setNextBacktrackPoint(IntChoiceFromSet icsCG) {
-
- HashSet<IntChoiceFromSet> backtrackCGs = new HashSet<>(cgMap.values());
- if (!isFirstResetDone) {
- // Reset the last CG of every LinkedList in the map and set done everything else
- for (Integer stateId : cgMap.keySet()) {
- setBacktrackCG(stateId);
- }
- isFirstResetDone = true;
- } else {
- // Check if we still have backtrack points for the last state after the last backtrack
- if (backtrackMap.containsKey(lastCGStateId)) {
- setBacktrackCG(lastCGStateId);
- } else {
- // We try to reset new CGs (if we do have) when we are running out of active CGs
- if (!backtrackStateQ.isEmpty()) {
- // Reset the next CG with the latest state
- int hiStateId = backtrackStateQ.peek();
- setBacktrackCG(hiStateId);
- }
- }
- }
- // Clear unused CGs
- for(IntChoiceFromSet cg : cgList) {
- if (!backtrackCGs.contains(cg)) {
- cg.setDone();
- }
- }
- cgList.clear();
- }
-
// --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper
// This method checks whether a choice is reachable in the VOD graph from a reference choice (BFS algorithm)