private class RGraph {
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, SummaryNode>> graphSummary;
public RGraph() {
hiStateId = 0;
graph = new HashMap<>();
+ graphSummary = new HashMap<>();
}
public void addReachableTransition(int stateId, TransitionEvent transition) {
+ // Record transition into graph
HashSet<TransitionEvent> transitionSet;
if (graph.containsKey(stateId)) {
transitionSet = graph.get(stateId);
}
return reachableTransitions;
}
+
+ public HashMap<Integer, SummaryNode> getReachableTransitionsSummary(int stateId) {
+ 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);
+
+ 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;
+ }
}
// This class compactly stores Read and Write field sets
}
}
+ // 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 void updateBacktrackSetRecursive(Execution execution, int currentChoice,
Execution conflictExecution, int conflictChoice,
ReadWriteSet currRWSet, HashSet<TransitionEvent> visited) {
+ TransitionEvent currTrans = execution.getExecutionTrace().get(currentChoice);
+ // TODO: THIS IS THE ACCESS SUMMARY
+ // Record this transition into rGraph summary
+ currRWSet = rGraph.recordTransitionSummary(currTrans.getStateId(), currTrans, 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;
}
// --- 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),
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<TransitionEvent> 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<Integer, SummaryNode> reachableTransitions = rGraph.getReachableTransitionsSummary(stateId);
+ for(Map.Entry<Integer, SummaryNode> transition : reachableTransitions.entrySet()) {
+ TransitionEvent reachableTransition = transition.getValue().getTransitionEvent();
+ Execution conflictExecution = reachableTransition.getExecution();
+ int conflictChoice = reachableTransition.getChoiceCounter();
+ // Copy ReadWriteSet object
+ ReadWriteSet currRWSet = transition.getValue().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<>();
+ updateBacktrackSetRecursive(execution, currentChoice, conflictExecution, conflictChoice, currRWSet, visited);
+ }
}
}
projects / jpf-core.git / blobdiff