private int choice; // Predecessor choice
private Execution execution; // Predecessor execution
- public Predecessor(int predChoice, Execution predExec) {
+ public Predecessor(Execution predExec, int predChoice) {
choice = predChoice;
execution = predExec;
}
return graph.get(stateId);
}
- public HashSet<TransitionEvent> getReachableTransitions(int stateId) {
- HashSet<TransitionEvent> 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<TransitionEvent> getReachableTransitions(int stateId) {
+// HashSet<TransitionEvent> 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<Integer, SummaryNode> getReachableTransitionsSummary(int stateId) {
+ public HashMap<Integer, SummaryNode> 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<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
- HashMap<String, Integer> writeMap = rwSet.getWriteMap();
- for(Map.Entry<String, Integer> 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<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
- HashMap<String, Integer> readMap = rwSet.getReadMap();
- for(Map.Entry<String, Integer> 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<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
+// HashMap<String, Integer> writeMap = rwSet.getWriteMap();
+// for(Map.Entry<String, Integer> 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<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
+// HashMap<String, Integer> readMap = rwSet.getReadMap();
+// for(Map.Entry<String, Integer> 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<Integer, SummaryNode> 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<Integer, SummaryNode> transitionSummary;
- if (graphSummary.containsKey(stateId)) {
- transitionSummary = graphSummary.get(stateId);
+ public void recordTransitionSummaryAtState(int stateId, HashMap<Integer, SummaryNode> transitionSummary) {
+ // Record transition summary into graphSummary
+ HashMap<Integer, SummaryNode> transSummary;
+ if (!graphSummary.containsKey(stateId)) {
+ transSummary = new HashMap<>(transitionSummary);
+ graphSummary.put(stateId, transSummary);
} else {
- transitionSummary = new HashMap<>();
- graphSummary.put(stateId, transitionSummary);
+ transSummary = graphSummary.get(stateId);
+ // Merge the two transition summaries
+ transSummary.putAll(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;
}
}
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)
+ // TODO: THIS IS THE ACCESS SUMMARY
+ private HashMap<Integer, SummaryNode> transitionSummary;
+ // Summary of pushed transitions at the current transition
+ 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<>();
+ transitionSummary = new HashMap<>();
+ recordedPredecessors = new HashMap<>();
stateId = 0;
transitionCG = null;
}
return stateId;
}
+ public HashMap<Integer, SummaryNode> getTransitionSummary() {
+ return transitionSummary;
+ }
+
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;
+ }
+
+ private ReadWriteSet performUnion(ReadWriteSet recordedRWSet, ReadWriteSet rwSet) {
+ // Combine the same write accesses and record in the recordedRWSet
+ HashMap<String, Integer> recordedWriteMap = recordedRWSet.getWriteMap();
+ HashMap<String, Integer> writeMap = rwSet.getWriteMap();
+ for(Map.Entry<String, Integer> 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).equals(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<String, Integer> recordedReadMap = recordedRWSet.getReadMap();
+ HashMap<String, Integer> readMap = rwSet.getReadMap();
+ for(Map.Entry<String, Integer> 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).equals(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) {
- predecessors.add(new Predecessor(choice, execution));
+ 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) {
Execution conflictExecution, int conflictChoice,
ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
+ if (visited.contains(currTrans)) {
+ 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(), currTrans, 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;
}
- if (visited.contains(currTrans)) {
- return;
- }
- visited.add(currTrans);
// Explore all predecessors
for (Predecessor predecessor : currTrans.getPredecessors()) {
// Get the predecessor (previous conflict choice)
// Check if a conflict is found
if (isConflictFound(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice, currRWSet)) {
createBacktrackingPoint(conflictExecution, conflictChoice, predecessorExecution, predecessorChoice);
- newConflictChoice = conflictChoice;
- newConflictExecution = conflictExecution;
+ newConflictChoice = predecessorChoice;
+ newConflictExecution = predecessorExecution;
}
// Continue performing DFS if conflict is not found
updateBacktrackSetRecursive(predecessorExecution, predecessorChoice, newConflictExecution, newConflictChoice,
private void updateBacktrackSetsFromPreviousExecution(Execution execution, int currentChoice, int stateId) {
// Collect all the reachable transitions from R-Graph
- HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionsSummary(stateId);
+ HashMap<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionSummary(stateId);
for(Map.Entry<Integer, SummaryNode> transition : reachableTransitions.entrySet()) {
- TransitionEvent reachableTransition = transition.getValue().getTransitionEvent();
+ SummaryNode summaryNode = transition.getValue();
+ TransitionEvent reachableTransition = summaryNode.getTransitionEvent();
Execution conflictExecution = reachableTransition.getExecution();
int conflictChoice = reachableTransition.getChoiceCounter();
// Copy ReadWriteSet object
- ReadWriteSet currRWSet = transition.getValue().getReadWriteSet();
+ 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