X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FDPORStateReducerEfficient.java;h=594829080a3ef30b4f04fe746f2ab4a38d4fb01e;hp=bb617af63c656f8efa9992e5938705c36f51f178;hb=ec609ae000b3f7bba0e2d6d4c12c0b4e86bd2bfe;hpb=eb6b30d1c6511ae1a573419982947e4dea1a12e2 diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java index bb617af..5948290 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducerEfficient.java @@ -393,14 +393,12 @@ public class DPORStateReducerEfficient extends ListenerAdapter { 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; + private HashMap> graphSummary; public RGraph() { hiStateId = 0; graph = new HashMap<>(); graphSummary = new HashMap<>(); - eventSummary = new HashMap<>(); } public void addReachableTransition(int stateId, TransitionEvent transition) { @@ -445,11 +443,12 @@ public class DPORStateReducerEfficient extends ListenerAdapter { return reachableTransitions; } - public HashMap getReachableSummaryTransitions(int stateId) { - return eventSummary.get(stateId); - } - - public HashMap getReachableSummaryRWSets(int stateId) { + public HashMap getReachableTransitionsSummary(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); } @@ -487,27 +486,23 @@ public class DPORStateReducerEfficient extends ListenerAdapter { 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; + HashMap transitionSummary; if (graphSummary.containsKey(stateId)) { - transitionMap = graphSummary.get(stateId); + transitionSummary = graphSummary.get(stateId); } else { - transitionMap = new HashMap<>(); - graphSummary.put(stateId, transitionMap); + transitionSummary = new HashMap<>(); + graphSummary.put(stateId, transitionSummary); } int choice = transition.getChoice(); - ReadWriteSet recordedRWSet; + SummaryNode summaryNode; // 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); + if (!transitionSummary.containsKey(choice)) { + summaryNode = new SummaryNode(transition, rwSet.getCopy()); + transitionSummary.put(choice, summaryNode); } else { - recordedRWSet = transitionMap.get(choice); + summaryNode = transitionSummary.get(choice); // Perform union and subtraction between the recorded and the given R/W sets - rwSet = performUnion(recordedRWSet, rwSet); + rwSet = performUnion(summaryNode.getReadWriteSet(), rwSet); } return rwSet; } @@ -594,6 +589,25 @@ public class DPORStateReducerEfficient extends ListenerAdapter { } } + // This class provides a data structure to store TransitionEvent and ReadWriteSet for a summary + private class SummaryNode { + private TransitionEvent transitionEvent; + private ReadWriteSet readWriteSet; + + public SummaryNode(TransitionEvent transEvent, ReadWriteSet rwSet) { + transitionEvent = transEvent; + readWriteSet = rwSet; + } + + public TransitionEvent getTransitionEvent() { + return transitionEvent; + } + + public ReadWriteSet getReadWriteSet() { + return readWriteSet; + } + } + // This class compactly stores transitions: // 1) CG, // 2) state ID, @@ -1211,12 +1225,15 @@ public class DPORStateReducerEfficient extends ListenerAdapter { private void updateBacktrackSetRecursive(Execution execution, int currentChoice, Execution conflictExecution, int conflictChoice, ReadWriteSet currRWSet, HashSet visited) { + // TODO: THIS IS THE ACCESS SUMMARY + TransitionEvent confTrans = conflictExecution.getExecutionTrace().get(conflictChoice); + // Record this transition into rGraph summary + currRWSet = rGraph.recordTransitionSummary(confTrans.getStateId(), confTrans, currRWSet); // Halt when we have found the first read/write conflicts for all memory locations if (currRWSet.isEmpty()) { return; } TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice); - // Halt when we have visited this transition (in a cycle) if (visited.contains(currTrans)) { return; } @@ -1235,10 +1252,6 @@ 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); @@ -1298,14 +1311,14 @@ 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.getReachableSummaryTransitions(stateId); - HashMap reachableRWSets = rGraph.getReachableSummaryRWSets(stateId); - for(Map.Entry transition : reachableTransitions.entrySet()) { - TransitionEvent reachableTransition = transition.getValue(); + HashMap reachableTransitions = rGraph.getReachableTransitionsSummary(stateId); + for(Map.Entry transition : reachableTransitions.entrySet()) { + SummaryNode summaryNode = transition.getValue(); + TransitionEvent reachableTransition = summaryNode.getTransitionEvent(); Execution conflictExecution = reachableTransition.getExecution(); int conflictChoice = reachableTransition.getChoiceCounter(); // Copy ReadWriteSet object - ReadWriteSet currRWSet = reachableRWSets.get(transition.getKey()); + ReadWriteSet currRWSet = summaryNode.getReadWriteSet(); currRWSet = currRWSet.getCopy(); // Memorize visited TransitionEvent object while performing backward DFS to avoid getting caught up in a cycle HashSet visited = new HashSet<>();