From f53fb642df66f87fa641cfff7969d75c7c3fa576 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Fri, 15 May 2020 12:31:39 -0700 Subject: [PATCH] Tested backtrack in a cycle (local). --- .../nasa/jpf/listener/DPORStateReducer.java | 38 +++++++++---------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java index ee61c19..37353f3 100644 --- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java +++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java @@ -605,8 +605,8 @@ public class DPORStateReducer extends ListenerAdapter { stateToEventMap.put(stateId, eventSet); } saveExecutionToRGraph(stateId); - stateToChoiceCounterMap.put(stateId, choiceCounter); analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId); + stateToChoiceCounterMap.put(stateId, choiceCounter); justVisitedStates.add(stateId); currVisitedStates.add(stateId); } @@ -722,7 +722,7 @@ public class DPORStateReducer extends ListenerAdapter { return currentChoice; } - private void createBacktrackingPoint(int currentChoice, int conflictChoice, Execution execution) { + private void createBacktrackingPoint(int backtrackChoice, int conflictChoice, Execution execution) { // Create a new list of choices for backtrack based on the current choice and conflicting event number // E.g. if we have a conflict between 1 and 3, then we create the list {3, 1, 0, 2} @@ -731,14 +731,14 @@ public class DPORStateReducer extends ListenerAdapter { //int firstChoice = choices[actualChoice]; ArrayList pastTrace = execution.getExecutionTrace(); ArrayList currTrace = currentExecution.getExecutionTrace(); - int backtrackEvent = currTrace.get(currentChoice).getChoice(); + int btrackChoice = currTrace.get(backtrackChoice).getChoice(); int stateId = pastTrace.get(conflictChoice).getStateId(); // Check if this trace has been done from this state - if (isTraceAlreadyConstructed(backtrackEvent, stateId)) { + if (isTraceAlreadyConstructed(btrackChoice, stateId)) { return; } // Put the conflicting event numbers first and reverse the order - newChoiceList[0] = backtrackEvent; + newChoiceList[0] = btrackChoice; newChoiceList[1] = pastTrace.get(conflictChoice).getChoice(); // Put the rest of the event numbers into the array starting from the minimum to the upper bound for (int i = 0, j = 2; i < refChoices.length; i++) { @@ -803,7 +803,6 @@ public class DPORStateReducer extends ListenerAdapter { } // Save all the visited states when starting a new execution of trace prevVisitedStates.addAll(currVisitedStates); - currVisitedStates.clear(); // This marks a transitional period to the new CG isEndOfExecution = true; } @@ -866,19 +865,19 @@ public class DPORStateReducer extends ListenerAdapter { return false; } - private boolean isConflictFound(int currentChoice, int reachableEvent, Execution execution) { + private boolean isConflictFound(int reachableChoice, int conflictChoice, Execution execution) { ArrayList executionTrace = execution.getExecutionTrace(); HashMap execRWFieldsMap = execution.getReadWriteFieldsMap(); // Skip if this event does not have any Read/Write set or the two events are basically the same event (number) - if (!execRWFieldsMap.containsKey(reachableEvent) || - executionTrace.get(currentChoice).getChoice() == executionTrace.get(reachableEvent).getChoice()) { + if (!execRWFieldsMap.containsKey(conflictChoice) || + executionTrace.get(reachableChoice).getChoice() == executionTrace.get(conflictChoice).getChoice()) { return false; } // Current R/W set - ReadWriteSet currRWSet = execRWFieldsMap.get(currentChoice); + ReadWriteSet currRWSet = execRWFieldsMap.get(reachableChoice); // R/W set of choice/event that may have a potential conflict - ReadWriteSet evtRWSet = execRWFieldsMap.get(reachableEvent); + ReadWriteSet evtRWSet = execRWFieldsMap.get(conflictChoice); // Check for conflicts with Read and Write fields for Write instructions Set currWriteSet = currRWSet.getWriteSet(); for(String writeField : currWriteSet) { @@ -950,6 +949,7 @@ public class DPORStateReducer extends ListenerAdapter { choices = icsCG.getAllChoices(); refChoices = copyChoices(choices); // Clear data structures + currVisitedStates = new HashSet<>(); stateToChoiceCounterMap = new HashMap<>(); stateToEventMap = new HashMap<>(); isEndOfExecution = false; @@ -995,10 +995,10 @@ public class DPORStateReducer extends ListenerAdapter { if (currVisitedStates.contains(stateId)) { // Update the backtrack sets in the cycle updateBacktrackSetsInCycle(stateId); - } else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution + } /* else if (prevVisitedStates.contains(stateId)) { // We visit a state in a previous execution // Update the backtrack sets in a previous execution updateBacktrackSetsInPreviousExecution(stateId); - } + }*/ } } @@ -1034,16 +1034,16 @@ public class DPORStateReducer extends ListenerAdapter { // Update the backtrack sets in the cycle private void updateBacktrackSetsInCycle(int stateId) { // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts - int currentChoice = stateToChoiceCounterMap.get(stateId); + int reachableChoice = stateToChoiceCounterMap.get(stateId); int cycleEndChoice = choiceCounter - 1; // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward) - while (currentChoice < cycleEndChoice) { - for (int reachableEvent = currentChoice + 1; reachableEvent <= cycleEndChoice; reachableEvent++) { - if (isConflictFound(currentChoice, reachableEvent, currentExecution)) { - createBacktrackingPoint(currentChoice, reachableEvent, currentExecution); + while (reachableChoice < cycleEndChoice) { + for (int conflictChoice = reachableChoice + 1; conflictChoice <= cycleEndChoice; conflictChoice++) { + if (isConflictFound(reachableChoice, conflictChoice, currentExecution)) { + createBacktrackingPoint(reachableChoice, conflictChoice, currentExecution); } } - currentChoice++; + reachableChoice++; } } -- 2.34.1