private int hiStateId; // Maximum state Id
private HashMap<Integer, HashSet<TransitionEvent>> graph; // Reachable transitions from past executions
// TODO: THIS IS THE ACCESS SUMMARY
- private HashMap<Integer, HashMap<Integer, ReadWriteSet>> graphSummary;
- private HashMap<Integer, HashMap<Integer, TransitionEvent>> eventSummary;
+ private HashMap<Integer, HashMap<Integer, SummaryNode>> graphSummary;
public RGraph() {
hiStateId = 0;
graph = new HashMap<>();
graphSummary = new HashMap<>();
- eventSummary = new HashMap<>();
}
public void addReachableTransition(int stateId, TransitionEvent transition) {
return reachableTransitions;
}
- public HashMap<Integer, TransitionEvent> getReachableSummaryTransitions(int stateId) {
- return eventSummary.get(stateId);
- }
-
- public HashMap<Integer, ReadWriteSet> getReachableSummaryRWSets(int stateId) {
+ public HashMap<Integer, SummaryNode> 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);
}
public ReadWriteSet recordTransitionSummary(int stateId, TransitionEvent transition, ReadWriteSet rwSet) {
// Record transition into graphSummary
// TransitionMap maps event (choice) number to a R/W set
- HashMap<Integer, ReadWriteSet> transitionMap;
+ HashMap<Integer, SummaryNode> 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<Integer, TransitionEvent> 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;
}
}
}
+ // 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,
private int choiceCounter; // Choice counter at this transition
private Execution execution; // The execution where this transition belongs
private HashSet<Predecessor> predecessors; // Maps incoming events/transitions (execution and choice)
+ private HashMap<Execution, HashSet<Integer>> recordedPredecessors;
+ // Memorize event and choice number to not record them twice
private int stateId; // State at this transition
private IntChoiceFromSet transitionCG; // CG at this transition
choiceCounter = 0;
execution = null;
predecessors = new HashSet<>();
+ recordedPredecessors = new HashMap<>();
stateId = 0;
transitionCG = null;
}
public IntChoiceFromSet getTransitionCG() { return transitionCG; }
+ private boolean isRecordedPredecessor(Execution execution, int choice) {
+ // See if we have recorded this predecessor earlier
+ HashSet<Integer> recordedChoices;
+ if (recordedPredecessors.containsKey(execution)) {
+ recordedChoices = recordedPredecessors.get(execution);
+ if (recordedChoices.contains(choice)) {
+ return true;
+ }
+ } else {
+ recordedChoices = new HashSet<>();
+ recordedPredecessors.put(execution, recordedChoices);
+ }
+ // Record the choice if we haven't seen it
+ recordedChoices.add(choice);
+
+ return false;
+ }
+
public void recordPredecessor(Execution execution, int choice) {
- predecessors.add(new Predecessor(choice, execution));
+ if (!isRecordedPredecessor(execution, choice)) {
+ predecessors.add(new Predecessor(choice, execution));
+ }
}
public void setChoice(int cho) {
private void updateBacktrackSetRecursive(Execution execution, int currentChoice,
Execution conflictExecution, int conflictChoice,
ReadWriteSet currRWSet, HashSet<TransitionEvent> 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;
}
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);
private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) {
// Collect all the reachable transitions from R-Graph
- HashMap<Integer, TransitionEvent> reachableTransitions = rGraph.getReachableSummaryTransitions(stateId);
- HashMap<Integer, ReadWriteSet> reachableRWSets = rGraph.getReachableSummaryRWSets(stateId);
- for(Map.Entry<Integer, TransitionEvent> transition : reachableTransitions.entrySet()) {
- TransitionEvent reachableTransition = transition.getValue();
+ HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionsSummary(stateId);
+ for(Map.Entry<Integer, SummaryNode> 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<TransitionEvent> visited = new HashSet<>();
projects / jpf-core.git / blobdiff