From d7f927a163c3cf8f1ca1e136433ac3d52f6c0f54 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Wed, 6 Jan 2021 14:19:32 -0800 Subject: [PATCH] Fixing bugs: the main one is to create a local copy of the set that contains accesses in updateBacktrackSetDFS(). --- .../nasa/jpf/listener/DPORStateReducer.java | 12 ++- .../listener/DPORStateReducerWithSummary.java | 75 ++++++++++++------- 2 files changed, 56 insertions(+), 31 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index 82f3db8..11d44ab 100755 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -681,6 +681,13 @@ public class DPORStateReducer extends ListenerAdapter { transition = new TransitionEvent(); currentExecution.addTransition(transition); transition.recordPredecessor(currentExecution, choiceCounter - 1); + // We have to check if there is a transition whose source state ID is the same + // If such exists, then we need to add its predecessors to the predecessor set of the current transition + for (TransitionEvent trans : rGraph.getReachableTransitionsAtState(stateId)) { + for (Predecessor pred : trans.getPredecessors()) { + transition.recordPredecessor(pred.getExecution(), pred.getChoice()); + } + } } transition.setExecution(currentExecution); transition.setTransitionCG(icsCG); @@ -1159,14 +1166,15 @@ public class DPORStateReducer extends ListenerAdapter { int newConflictChoice = conflictChoice; Execution newConflictExecution = conflictExecution; // Check if a conflict is found - if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) { + ReadWriteSet newCurrRWSet = currRWSet.getCopy(); + if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, newCurrRWSet)) { createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice); newConflictChoice = predecessorChoice; newConflictExecution = predecessorExecution; } // Continue performing DFS if conflict is not found updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice, - currRWSet, visited); + newCurrRWSet, visited); } } diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java index 39616d9..50e4061 100755 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerWithSummary.java @@ -259,7 +259,7 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { 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 @@ -632,7 +632,8 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { public Set getEventChoicesAtStateId(int stateId) { HashMap 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) { @@ -640,6 +641,10 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { return stateSummary.get(eventChoice); } + public Set getStateIds() { + return mainSummary.keySet(); + } + private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) { // Combine the same write accesses and record in the recordedRWSet HashMap recordedWriteMap = recordedRWSet.getWriteMap(); @@ -761,6 +766,13 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { transition = new TransitionEvent(); currentExecution.addTransition(transition); transition.recordPredecessor(currentExecution, choiceCounter - 1); + // We have to check if there is a transition whose source state ID is the same + // If such exists, then we need to add its predecessors to the predecessor set of the current transition + for (TransitionEvent trans : rGraph.getReachableTransitionsAtState(stateId)) { + for (Predecessor pred : trans.getPredecessors()) { + transition.recordPredecessor(pred.getExecution(), pred.getChoice()); + } + } } transition.setExecution(currentExecution); transition.setTransitionCG(icsCG); @@ -831,15 +843,20 @@ public class DPORStateReducerWithSummary 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 boolean terminate = false; + Set 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 + if (currVisitedStates.containsKey(stateId) && currVisitedStates.get(stateId) > 1) { + updateBacktrackSetsFromGraph(stateId, currentExecution, choiceCounter - 1); + } } } return terminate; @@ -1224,26 +1241,26 @@ public class DPORStateReducerWithSummary extends ListenerAdapter { return; } visited.add(currTrans); - // Halt if the set is empty - if (currRWSet.isEmpty()) { - return; - } - // 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 : 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 + 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); } } -- 2.34.1