From 9d2c551068bfd05a35449ee29da5a70768e2adae Mon Sep 17 00:00:00 2001 From: rtrimana Date: Mon, 21 Sep 2020 15:01:05 -0700 Subject: [PATCH] Fixing a bug: summary of conflict transition and ReadWriteSet need to be stored in TransitionEvent; then summary of reachable transitions at a state can be stored in the RGraph object. --- .../listener/DPORStateReducerEfficient.java | 195 ++++++++++++------ 1 file changed, 129 insertions(+), 66 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java index 1f5408d..cdfdcdd 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java @@ -430,20 +430,20 @@ public class DPORStateReducerEfficient extends ListenerAdapter { return graph.get(stateId); } - public HashSet getReachableTransitions(int stateId) { - HashSet reachableTransitions = new HashSet<>(); - // All transitions from states higher than the given state ID (until the highest state ID) are reachable - for(int stId = stateId; stId <= hiStateId; stId++) { - // We might encounter state IDs from the first round of Boolean CG - // The second round of Boolean CG should consider these new states - if (graph.containsKey(stId)) { - reachableTransitions.addAll(graph.get(stId)); - } - } - return reachableTransitions; - } +// public HashSet getReachableTransitions(int stateId) { +// HashSet reachableTransitions = new HashSet<>(); +// // All transitions from states higher than the given state ID (until the highest state ID) are reachable +// for(int stId = stateId; stId <= hiStateId; stId++) { +// // We might encounter state IDs from the first round of Boolean CG +// // The second round of Boolean CG should consider these new states +// if (graph.containsKey(stId)) { +// reachableTransitions.addAll(graph.get(stId)); +// } +// } +// return reachableTransitions; +// } - public HashMap getReachableTransitionsSummary(int stateId) { + public HashMap getReachableTransitionSummary(int stateId) { // Just return an empty map if the state ID is not recorded yet // This means that there is no reachable transition from this state if (!graphSummary.containsKey(stateId)) { @@ -452,59 +452,64 @@ public class DPORStateReducerEfficient extends ListenerAdapter { return graphSummary.get(stateId); } - private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) { - // Combine the same write accesses and record in the recordedRWSet - HashMap recordedWriteMap = recordedRWSet.getWriteMap(); - HashMap writeMap = rwSet.getWriteMap(); - for(Map.Entry entry : recordedWriteMap.entrySet()) { - String writeField = entry.getKey(); - // Remove the entry from rwSet if both field and object ID are the same - if (writeMap.containsKey(writeField) && - (writeMap.get(writeField) == recordedWriteMap.get(writeField))) { - writeMap.remove(writeField); - } - } - // Then add everything into the recorded map because these will be traversed - recordedWriteMap.putAll(writeMap); - // Combine the same read accesses and record in the recordedRWSet - HashMap recordedReadMap = recordedRWSet.getReadMap(); - HashMap readMap = rwSet.getReadMap(); - for(Map.Entry entry : recordedReadMap.entrySet()) { - String readField = entry.getKey(); - // Remove the entry from rwSet if both field and object ID are the same - if (readMap.containsKey(readField) && - (readMap.get(readField) == recordedReadMap.get(readField))) { - readMap.remove(readField); - } - } - // Then add everything into the recorded map because these will be traversed - recordedReadMap.putAll(readMap); +// private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) { +// // Combine the same write accesses and record in the recordedRWSet +// HashMap recordedWriteMap = recordedRWSet.getWriteMap(); +// HashMap writeMap = rwSet.getWriteMap(); +// for(Map.Entry entry : recordedWriteMap.entrySet()) { +// String writeField = entry.getKey(); +// // Remove the entry from rwSet if both field and object ID are the same +// if (writeMap.containsKey(writeField) && +// (writeMap.get(writeField) == recordedWriteMap.get(writeField))) { +// writeMap.remove(writeField); +// } +// } +// // Then add everything into the recorded map because these will be traversed +// recordedWriteMap.putAll(writeMap); +// // Combine the same read accesses and record in the recordedRWSet +// HashMap recordedReadMap = recordedRWSet.getReadMap(); +// HashMap readMap = rwSet.getReadMap(); +// for(Map.Entry entry : recordedReadMap.entrySet()) { +// String readField = entry.getKey(); +// // Remove the entry from rwSet if both field and object ID are the same +// if (readMap.containsKey(readField) && +// (readMap.get(readField) == recordedReadMap.get(readField))) { +// readMap.remove(readField); +// } +// } +// // Then add everything into the recorded map because these will be traversed +// recordedReadMap.putAll(readMap); +// +// return rwSet; +// } - return rwSet; - } +// public ReadWriteSet recordTransitionSummary(int stateId, TransitionEvent transition, ReadWriteSet rwSet) { +// // Record transition into graphSummary +// // TransitionMap maps event (choice) number to a R/W set +// HashMap transitionSummary; +// if (graphSummary.containsKey(stateId)) { +// transitionSummary = graphSummary.get(stateId); +// } else { +// transitionSummary = new HashMap<>(); +// graphSummary.put(stateId, transitionSummary); +// } +// int choice = transition.getChoice(); +// SummaryNode summaryNode; +// // Insert transition into the map if we haven't had this event number recorded +// if (!transitionSummary.containsKey(choice)) { +// summaryNode = new SummaryNode(transition, rwSet.getCopy()); +// transitionSummary.put(choice, summaryNode); +// } else { +// summaryNode = transitionSummary.get(choice); +// // Perform union and subtraction between the recorded and the given R/W sets +// rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet); +// } +// return rwSet; +// } - public ReadWriteSet recordTransitionSummary(int stateId, TransitionEvent transition, ReadWriteSet rwSet) { - // Record transition into graphSummary - // TransitionMap maps event (choice) number to a R/W set - HashMap transitionSummary; - if (graphSummary.containsKey(stateId)) { - transitionSummary = graphSummary.get(stateId); - } else { - transitionSummary = new HashMap<>(); - graphSummary.put(stateId, transitionSummary); - } - int choice = transition.getChoice(); - SummaryNode summaryNode; - // Insert transition into the map if we haven't had this event number recorded - if (!transitionSummary.containsKey(choice)) { - summaryNode = new SummaryNode(transition, rwSet.getCopy()); - transitionSummary.put(choice, summaryNode); - } else { - summaryNode = transitionSummary.get(choice); - // Perform union and subtraction between the recorded and the given R/W sets - rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet); - } - return rwSet; + public void recordTransitionSummaryAtState(int stateId, HashMap transitionSummary) { + // Record transition summary into graphSummary + graphSummary.put(stateId, transitionSummary); } } @@ -618,6 +623,9 @@ public class DPORStateReducerEfficient extends ListenerAdapter { private int choiceCounter; // Choice counter at this transition private Execution execution; // The execution where this transition belongs private HashSet predecessors; // Maps incoming events/transitions (execution and choice) + // TODO: THIS IS THE ACCESS SUMMARY + private HashMap transitionSummary; + // Summary of pushed transitions at the current transition private HashMap> recordedPredecessors; // Memorize event and choice number to not record them twice private int stateId; // State at this transition @@ -628,6 +636,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter { choiceCounter = 0; execution = null; predecessors = new HashSet<>(); + transitionSummary = new HashMap<>(); recordedPredecessors = new HashMap<>(); stateId = 0; transitionCG = null; @@ -653,6 +662,10 @@ public class DPORStateReducerEfficient extends ListenerAdapter { return stateId; } + public HashMap getTransitionSummary() { + return transitionSummary; + } + public IntChoiceFromSet getTransitionCG() { return transitionCG; } private boolean isRecordedPredecessor(Execution execution, int choice) { @@ -673,12 +686,60 @@ public class DPORStateReducerEfficient extends ListenerAdapter { return false; } + private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) { + // Combine the same write accesses and record in the recordedRWSet + HashMap recordedWriteMap = recordedRWSet.getWriteMap(); + HashMap writeMap = rwSet.getWriteMap(); + for(Map.Entry entry : recordedWriteMap.entrySet()) { + String writeField = entry.getKey(); + // Remove the entry from rwSet if both field and object ID are the same + if (writeMap.containsKey(writeField) && + (writeMap.get(writeField) == recordedWriteMap.get(writeField))) { + writeMap.remove(writeField); + } + } + // Then add everything into the recorded map because these will be traversed + recordedWriteMap.putAll(writeMap); + // Combine the same read accesses and record in the recordedRWSet + HashMap recordedReadMap = recordedRWSet.getReadMap(); + HashMap readMap = rwSet.getReadMap(); + for(Map.Entry entry : recordedReadMap.entrySet()) { + String readField = entry.getKey(); + // Remove the entry from rwSet if both field and object ID are the same + if (readMap.containsKey(readField) && + (readMap.get(readField) == recordedReadMap.get(readField))) { + readMap.remove(readField); + } + } + // Then add everything into the recorded map because these will be traversed + recordedReadMap.putAll(readMap); + + return rwSet; + } + public void recordPredecessor(Execution execution, int choice) { if (!isRecordedPredecessor(execution, choice)) { predecessors.add(new Predecessor(execution, choice)); } } + public ReadWriteSet recordTransitionSummary(TransitionEvent transition, ReadWriteSet rwSet) { + // Record transition into reachability summary + // TransitionMap maps event (choice) number to a R/W set + int choice = transition.getChoice(); + SummaryNode summaryNode; + // Insert transition into the map if we haven't had this event number recorded + if (!transitionSummary.containsKey(choice)) { + summaryNode = new SummaryNode(transition, rwSet.getCopy()); + transitionSummary.put(choice, summaryNode); + } else { + summaryNode = transitionSummary.get(choice); + // Perform union and subtraction between the recorded and the given R/W sets + rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet); + } + return rwSet; + } + public void setChoice(int cho) { choice = cho; } @@ -1252,7 +1313,9 @@ public class DPORStateReducerEfficient extends ListenerAdapter { // TODO: THIS IS THE ACCESS SUMMARY TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice); // Record this transition into rGraph summary - currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), confTrans, currRWSet); + //currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), confTrans, currRWSet); + currRWSet = currTrans.recordTransitionSummary(confTrans, currRWSet); + rGraph.recordTransitionSummaryAtState(currTrans.getStateId(), currTrans.getTransitionSummary()); // Halt when we have found the first read/write conflicts for all memory locations if (currRWSet.isEmpty()) { return; @@ -1334,7 +1397,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter { private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) { // Collect all the reachable transitions from R-Graph - HashMap reachableTransitions = rGraph.getReachableTransitionsSummary(stateId); + HashMap reachableTransitions = rGraph.getReachableTransitionSummary(stateId); for(Map.Entry transition : reachableTransitions.entrySet()) { SummaryNode summaryNode = transition.getValue(); TransitionEvent reachableTransition = summaryNode.getTransitionEvent(); -- 2.34.1