From 44ce37fe4003c0096cec58a930e477fe2adc231e Mon Sep 17 00:00:00 2001 From: rtrimana Date: Wed, 23 Sep 2020 11:30:02 -0700 Subject: [PATCH 1/1] Removing dead/commented code. --- .../listener/DPORStateReducerEfficient.java | 162 +----------------- 1 file changed, 2 insertions(+), 160 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java index 5762ec5..31b4800 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java @@ -392,13 +392,10 @@ public class DPORStateReducerEfficient extends ListenerAdapter { private class RGraph { private int hiStateId; // Maximum state Id private HashMap> graph; // Reachable transitions from past executions - // TODO: THIS IS THE ACCESS SUMMARY - //private HashMap> graphSummary; public RGraph() { hiStateId = 0; graph = new HashMap<>(); - //graphSummary = new HashMap<>(); } public void addReachableTransition(int stateId, TransitionEvent transition) { @@ -429,96 +426,6 @@ 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 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)) { -// return new HashMap<>(); -// } -// 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); -// -// 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 -// HashMap transSummary; -// if (!graphSummary.containsKey(stateId)) { -// transSummary = new HashMap<>(transitionSummary); -// graphSummary.put(stateId, transSummary); -// } else { -// transSummary = graphSummary.get(stateId); -// // Merge the two transition summaries -// transSummary.putAll(transitionSummary); -// } -// } } // This class compactly stores Read and Write field sets @@ -631,7 +538,6 @@ 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; @@ -1279,41 +1185,10 @@ public class DPORStateReducerEfficient extends ListenerAdapter { // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle HashSet visited = new HashSet<>(); // Update backtrack set recursively - // TODO: The following is the call to the original version of the method -// updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited); - // TODO: The following is the call to the version of the method with pushing up happens-before transitions updateBacktrackSetRecursive(execution, currentChoice, execution, currentChoice, currRWSet, visited); } -// TODO: This is the original version of the recursive method -// private void updateBacktrackSetRecursive(Execution execution, int currentChoice, -// Execution conflictExecution, int conflictChoice, -// ReadWriteSet currRWSet, HashSet visited) { -// // Halt when we have found the first read/write conflicts for all memory locations -// if (currRWSet.isEmpty()) { -// return; -// } -// TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice); -// // Halt when we have visited this transition (in a cycle) -// if (visited.contains(confTrans)) { -// return; -// } -// visited.add(confTrans); -// // Explore all predecessors -// for (Predecessor predecessor : confTrans.getPredecessors()) { -// // Get the predecessor (previous conflict choice) -// conflictChoice = predecessor.getChoice(); -// conflictExecution = predecessor.getExecution(); -// // Check if a conflict is found -// if (isConflictFound(execution, currentChoice, conflictExecution, conflictChoice, currRWSet)) { -// createBacktrackingPoint(execution, currentChoice, conflictExecution, conflictChoice); -// } -// // Continue performing DFS if conflict is not found -// updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited); -// } -// } - - // TODO: This is the version of the method with pushing up happens-before transitions + // Recursive method to perform backward DFS to traverse the graph private void updateBacktrackSetRecursive(Execution execution, int currentChoice, Execution conflictExecution, int conflictChoice, ReadWriteSet currRWSet, HashSet visited) { @@ -1322,12 +1197,9 @@ public class DPORStateReducerEfficient extends ListenerAdapter { return; } visited.add(currTrans); - // 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 = 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; @@ -1356,36 +1228,7 @@ public class DPORStateReducerEfficient extends ListenerAdapter { } // --- Functions related to the reachability analysis when there is a state match - - /*private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { - // Perform this analysis only when: - // 1) this is not during a switch to a new execution, - // 2) at least 2 choices/events have been explored (choiceCounter > 1), - // 3) state > 0 (state 0 is for boolean CG) - if (!isEndOfExecution && choiceCounter > 1 && stateId > 0) { - if (currVisitedStates.contains(stateId) || prevVisitedStates.contains(stateId)) { - // Update reachable transitions in the graph with a predecessor - HashSet reachableTransitions = rGraph.getReachableTransitionsAtState(stateId); - for(TransitionEvent transition : reachableTransitions) { - transition.recordPredecessor(currentExecution, choiceCounter - 1); - } - updateBacktrackSetsFromPreviousExecution(stateId); - } - } - } - - // Update the backtrack sets from previous executions - private void updateBacktrackSetsFromPreviousExecution(int stateId) { - // Collect all the reachable transitions from R-Graph - HashSet reachableTransitions = rGraph.getReachableTransitions(stateId); - for(TransitionEvent transition : reachableTransitions) { - Execution execution = transition.getExecution(); - int currentChoice = transition.getChoiceCounter(); - updateBacktrackSet(execution, currentChoice); - } - }*/ - - // TODO: THIS IS THE ACCESS SUMMARY + private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) { // Perform this analysis only when: // 1) this is not during a switch to a new execution, @@ -1405,7 +1248,6 @@ public class DPORStateReducerEfficient extends ListenerAdapter { private void updateBacktrackSetsFromPreviousExecution(int stateId) { // Collect all the reachable transitions from R-Graph - //HashMap reachableTransitions = rGraph.getReachableTransitionSummary(stateId); HashSet reachableTransitions = rGraph.getReachableTransitionsAtState(stateId); for(TransitionEvent transition : reachableTransitions) { // Current transition that stems from this state ID -- 2.34.1