From eb6b30d1c6511ae1a573419982947e4dea1a12e2 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 4 Sep 2020 12:34:24 -0700 Subject: [PATCH] Initial implementation of more efficient traversal with graph summary; pretty much untested and un-double-checked yet. --- .../listener/DPORStateReducerEfficient.java | 114 +++++++++++++++++- 1 file changed, 113 insertions(+), 1 deletion(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java index 876d34f..bb617af 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java @@ -392,13 +392,19 @@ 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; + private HashMap> eventSummary; public RGraph() { hiStateId = 0; graph = new HashMap<>(); + graphSummary = new HashMap<>(); + eventSummary = new HashMap<>(); } public void addReachableTransition(int stateId, TransitionEvent transition) { + // Record transition into graph HashSet transitionSet; if (graph.containsKey(stateId)) { transitionSet = graph.get(stateId); @@ -438,6 +444,73 @@ public class DPORStateReducerEfficient extends ListenerAdapter { } return reachableTransitions; } + + public HashMap getReachableSummaryTransitions(int stateId) { + return eventSummary.get(stateId); + } + + public HashMap getReachableSummaryRWSets(int stateId) { + 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 transitionMap; + if (graphSummary.containsKey(stateId)) { + transitionMap = graphSummary.get(stateId); + } else { + transitionMap = new HashMap<>(); + graphSummary.put(stateId, transitionMap); + } + int choice = transition.getChoice(); + ReadWriteSet recordedRWSet; + // Insert transition into the map if we haven't had this event number recorded + if (!transitionMap.containsKey(choice)) { + recordedRWSet = rwSet.getCopy(); + transitionMap.put(choice, recordedRWSet); + // Insert the actual TransitionEvent object into the map + HashMap eventMap = new HashMap<>(); + eventMap.put(choice, transition); + eventSummary.put(stateId, eventMap); + } else { + recordedRWSet = transitionMap.get(choice); + // Perform union and subtraction between the recorded and the given R/W sets + rwSet = performUnion(recordedRWSet, rwSet); + } + return rwSet; + } } // This class compactly stores Read and Write field sets @@ -1162,6 +1235,10 @@ public class DPORStateReducerEfficient extends ListenerAdapter { newConflictChoice = conflictChoice; newConflictExecution = conflictExecution; } + // TODO: THIS IS THE ACCESS SUMMARY + // Record this transition into rGraph summary + int stateId = predecessor.getExecution().getExecutionTrace().get(predecessorChoice).getStateId(); + currRWSet = rGraph.recordTransitionSummary(stateId, currTrans, currRWSet); // Continue performing DFS if conflict is not found updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice, currRWSet, visited); @@ -1173,7 +1250,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) { + /*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), @@ -1199,5 +1276,40 @@ public class DPORStateReducerEfficient extends ListenerAdapter { 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, + // 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(currentExecution, choiceCounter - 1, stateId); + } + } + } + + private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) { + // Collect all the reachable transitions from R-Graph + HashMap reachableTransitions = rGraph.getReachableSummaryTransitions(stateId); + HashMap reachableRWSets = rGraph.getReachableSummaryRWSets(stateId); + for(Map.Entry transition : reachableTransitions.entrySet()) { + TransitionEvent reachableTransition = transition.getValue(); + Execution conflictExecution = reachableTransition.getExecution(); + int conflictChoice = reachableTransition.getChoiceCounter(); + // Copy ReadWriteSet object + ReadWriteSet currRWSet = reachableRWSets.get(transition.getKey()); + currRWSet = currRWSet.getCopy(); + // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle + HashSet visited = new HashSet<>(); + updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited); + } } } -- 2.34.1