private boolean debugMode;
private boolean stateReductionMode;
private final PrintWriter out;
- volatile private String detail;
- volatile private int depth;
- volatile private int id;
- Transition transition;
+ private String detail;
+ private int depth;
+ private int id;
+ private Transition transition;
// State reduction fields
private Integer[] choices;
// Stores explored backtrack lists in the form of HashSet of Strings
private HashSet<String> backtrackSet;
private HashMap<Integer, HashSet<Integer>> conflictPairMap;
- // Map choicelist with start index
- // private HashMap<Integer[],Integer> choiceListStartIndexMap;
// Map that represents graph G
// (i.e., visible operation dependency graph (VOD Graph)
// VOD graph is updated when the state has not yet been seen
// Current state
private int stateId;
- // Previous state
- private int prevStateId;
// Previous choice number
private int prevChoiceValue;
- // Counter for a visited state
- private HashMap<Integer, Integer> visitedStateCounter;
// HashSet that stores references to unused CGs
private HashSet<IntChoiceFromSet> unusedCG;
+ // Reference to the state graph in the ConflictTracker class
+ private HashMap<Integer, ConflictTracker.Node> stateGraph;
+ // Visited states in the previous and current executions/traces for terminating condition
+ private HashSet<Integer> prevVisitedStates;
+ private HashSet<Integer> currVisitedStates;
+
public StateReducer(Config config, JPF jpf) {
debugMode = config.getBoolean("debug_state_transition", false);
stateReductionMode = config.getBoolean("activate_state_reduction", true);
isBooleanCGFlipped = false;
vodGraphMap = new HashMap<>();
stateId = -1;
- prevStateId = -1;
prevChoiceValue = -1;
cgMap = new HashMap<>();
readWriteFieldsMap = new HashMap<>();
backtrackSet = new HashSet<>();
conflictPairMap = new HashMap<>();
unusedCG = new HashSet<>();
- visitedStateCounter = new HashMap<>();
+ // TODO: We are assuming that the StateReducer is always used together with the ConflictTracker
+ stateGraph = ConflictTracker.nodes;
+ prevVisitedStates = new HashSet<>();
+ currVisitedStates = new HashSet<>();
initializeStateReduction();
}
unusedCG.clear();
}
- private void incrementVisitedStateCounter(int stId) {
- // Increment counter for this state ID
- if (visitedStateCounter.containsKey(stId)) {
- int stateCount = visitedStateCounter.get(stId);
- visitedStateCounter.put(stId, stateCount + 1);
+ // Detect cycles in the current execution/trace
+ // We terminate the execution iff:
+ // (1) the state has been visited in the current execution
+ // (2) the state has one or more cycles that involve all the events
+ private boolean containsCyclesWithAllEvents(int stId) {
+
+ HashSet<Integer> visitedEvents = new HashSet<>();
+ boolean containsCyclesWithAllEvts = false;
+ ConflictTracker.Node currNode = stateGraph.get(stId);
+ for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
+ dfsFindCycles(edge.getDst(), visitedEvents, new HashSet<>());
+ }
+ if (checkIfAllEventsInvolved(visitedEvents)) {
+ containsCyclesWithAllEvts = true;
+ }
+
+ return containsCyclesWithAllEvts;
+ }
+
+ private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<Integer> visitedEvents,
+ HashSet<Integer> visitingEvents) {
+
+ // Stop when there is a cycle and record all the events
+ if (visitingEvents.contains(currNode.getId())) {
+ visitedEvents.addAll(visitingEvents);
} else {
- // If we have seen it then the frequency is 2
- visitedStateCounter.put(stId, 2);
+ for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
+ visitingEvents.add(edge.getEventNumber());
+ dfsFindCycles(edge.getDst(), visitedEvents, visitingEvents);
+ visitingEvents.remove(edge.getEventNumber());
+ }
}
}
- private boolean isVisitedMultipleTimes(int stId) {
- // Return true if the state has been visited more than once
- if (visitedStateCounter.containsKey(stId) &&
- visitedStateCounter.get(stId) > 1) {
- return true;
+ private boolean checkIfAllEventsInvolved(HashSet<Integer> visitedEvents) {
+
+ // Check if this set contains all the event choices
+ // If not then this is not the terminating condition
+ for(int i=0; i<=choiceUpperBound; i++) {
+ if (!visitedEvents.contains(i)) {
+ return false;
+ }
}
- return false;
+ return true;
}
@Override
readWriteFieldsMap.clear();
choiceCounter = 0;
}
- if (!vm.isNewState()) {
- incrementVisitedStateCounter(stateId);
- }
- // Check if we have seen this state and it's not looping back to itself
- if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
+ // Check if we have seen this state or this state contains cycles that involve all events
+// if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
+ if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {
// Traverse the sub-graphs
if (isResetAfterAnalysis) {
// Advance choice counter for sub-graphs
resetAllCGs();
isResetAfterAnalysis = true;
}
+ // Save all the visited states
+ prevVisitedStates.addAll(currVisitedStates);
}
}
}
}
- public void updateVODGraph(int prevChoice, int currChoice) {
+ private void updateVODGraph(int prevChoice, int currChoice) {
HashSet<Integer> choiceSet;
if (vodGraphMap.containsKey(prevChoice)) {
choiceSet.add(currChoice);
}
- private void updateStateId(Search search) {
- // Saving the previous state
- prevStateId = stateId;
- // Line 19 in the paper page 11 (see the heading note above)
- stateId = search.getStateId();
- }
-
@Override
public void stateAdvanced(Search search) {
if (debugMode) {
currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice;
if (currChoice < 0 || choices[currChoice] == -1 ||
prevChoiceValue == choices[currChoice]) {
-// || currChoice > choices.length - 1 || choices[currChoice] == -1 ||
-// prevChoiceValue == choices[currChoice]) {
-// // When current choice is 0, previous choice could be -1
+ // When current choice is 0, previous choice could be -1
// updateVODGraph(prevChoiceValue, choices[currChoice]);
-// // Current choice becomes previous choice in the next iteration
-// prevChoiceValue = choices[currChoice];
// Update the state ID variables
- updateStateId(search);
- // Handle all corner cases (e.g., out of bound values)
+ stateId = search.getStateId();
+ currVisitedStates.add(stateId);
return;
}
// When current choice is 0, previous choice could be -1
// Current choice becomes previous choice in the next iteration
prevChoiceValue = choices[currChoice];
// Update the state ID variables
- updateStateId(search);
+ stateId = search.getStateId();
+ currVisitedStates.add(stateId);
}
}
detail = null;
// Update the state variables
- // Saving the previous state
- prevStateId = stateId;
// Line 19 in the paper page 11 (see the heading note above)
stateId = search.getStateId();
projects / jpf-core.git / blobdiff