From ed1e956e6aa9025c20aeaa521fb9b582aed771b1 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Tue, 7 Apr 2020 10:31:21 -0700 Subject: [PATCH 1/1] Fixing a potential bug: we now store the event number in the ArrayList together with the list of CGs for backtracking; getting the event number directly from the current array might be misleading because the array choices might have been modified for fair-scheduling. --- .../nasa/jpf/listener/DPORStateReducer.java | 39 ++++++++++--------- 1 file changed, 20 insertions(+), 19 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 72fc44e..53cd566 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -60,9 +60,9 @@ public class DPORStateReducer extends ListenerAdapter { // 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 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 currVisitedStates; // States being visited in the current execution @@ -72,7 +72,7 @@ public class DPORStateReducer extends ListenerAdapter { // Data structure to analyze field Read/Write accesses and conflicts private HashMap> backtrackMap; // Track created backtracking points private PriorityQueue backtrackStateQ; // Heap that returns the latest state - private ArrayList cgList; // Record CGs for backtracking points + private ArrayList backtrackPointList; // Record backtrack points (CG and choice) private HashMap cgMap; // Maps state IDs to CGs private HashMap> conflictPairMap; // Record conflicting events private HashSet doneBacktrackSet; // Record state ID and trace that are done @@ -188,7 +188,8 @@ public class DPORStateReducer extends ListenerAdapter { 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(); @@ -326,19 +327,19 @@ public class DPORStateReducer extends ListenerAdapter { // 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; } } @@ -423,7 +424,7 @@ public class DPORStateReducer extends ListenerAdapter { // Backtracking backtrackMap = new HashMap<>(); backtrackStateQ = new PriorityQueue<>(Collections.reverseOrder()); - cgList = new ArrayList<>(); + backtrackPointList = new ArrayList<>(); cgMap = new HashMap<>(); conflictPairMap = new HashMap<>(); doneBacktrackSet = new HashSet<>(); @@ -572,10 +573,9 @@ public class DPORStateReducer extends ListenerAdapter { 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]) { @@ -583,8 +583,8 @@ public class DPORStateReducer extends ListenerAdapter { 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; @@ -737,8 +737,8 @@ public class DPORStateReducer extends ListenerAdapter { 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])); } } @@ -779,12 +779,13 @@ public class DPORStateReducer extends ListenerAdapter { } } // Clear unused CGs - for(IntChoiceFromSet cg : cgList) { + for(BacktrackPoint backtrackPoint : backtrackPointList) { + IntChoiceFromSet cg = backtrackPoint.getBacktrackCG(); if (!backtrackCGs.contains(cg)) { cg.setDone(); } } - cgList.clear(); + backtrackPointList.clear(); } // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper -- 2.34.1