From c9b98285f5bd0c6e9f6577fd4fd564d3eab7ced0 Mon Sep 17 00:00:00 2001 From: rtrimana Date: Wed, 25 Mar 2020 15:43:13 -0700 Subject: [PATCH] Fixing bugs and cleaning up: making sure that the execution of the first trace has fair-scheduling with appropriate state-matching. --- main.jpf | 3 +- .../gov/nasa/jpf/listener/StateReducer.java | 121 ++++++++++++------ .../jpf/vm/choice/NumberChoiceFromList.java | 12 ++ 3 files changed, 94 insertions(+), 42 deletions(-) diff --git a/main.jpf b/main.jpf index 9ce7d13..5d32e0b 100644 --- a/main.jpf +++ b/main.jpf @@ -6,7 +6,8 @@ target = main #listener=gov.nasa.jpf.listener.StateReducerOld #listener=gov.nasa.jpf.listener.VariableConflictTracker,gov.nasa.jpf.listener.StateReducer #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer -listener=gov.nasa.jpf.listener.ConflictTracker +listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerSimple +#listener=gov.nasa.jpf.listener.ConflictTracker #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerClean #listener=gov.nasa.jpf.listener.StateReducerClean diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java index 0a27b5c..afa1f87 100644 --- a/src/main/gov/nasa/jpf/listener/StateReducer.java +++ b/src/main/gov/nasa/jpf/listener/StateReducer.java @@ -59,6 +59,7 @@ public class StateReducer extends ListenerAdapter { // State reduction fields private Integer[] choices; + private Integer[] refChoices; private IntChoiceFromSet currCG; private int choiceCounter; private Integer choiceUpperBound; @@ -83,7 +84,7 @@ public class StateReducer extends ListenerAdapter { // (i.e., hash table that records encountered states) // VOD graph is updated when the state has not yet been seen // Current state - private int stateId; + private HashSet justVisitedStates; // Previous choice number private int prevChoiceValue; // HashSet that stores references to unused CGs @@ -110,7 +111,7 @@ public class StateReducer extends ListenerAdapter { transition = null; isBooleanCGFlipped = false; vodGraphMap = new HashMap<>(); - stateId = -1; + justVisitedStates = new HashSet<>(); prevChoiceValue = -1; cgMap = new HashMap<>(); readWriteFieldsMap = new HashMap<>(); @@ -127,6 +128,7 @@ public class StateReducer extends ListenerAdapter { private void initializeStateReduction() { if (stateReductionMode) { choices = null; + refChoices = null; currCG = null; choiceCounter = 0; choiceUpperBound = 0; @@ -170,7 +172,7 @@ public class StateReducer extends ListenerAdapter { icsCG.setNewValues(choices); icsCG.reset(); // Use a modulo since choiceCounter is going to keep increasing - int choiceIndex = choiceCounter % (choices.length - 1); + int choiceIndex = choiceCounter % choices.length; icsCG.advance(choices[choiceIndex]); if (choiceIndex == 0) { resetReadWriteAnalysis(); @@ -178,6 +180,13 @@ public class StateReducer extends ListenerAdapter { return icsCG; } + private Integer[] copyChoices(Integer[] choicesToCopy) { + + Integer[] copyOfChoices = new Integer[choicesToCopy.length]; + System.arraycopy(choicesToCopy, 0, copyOfChoices, 0, choicesToCopy.length); + return copyOfChoices; + } + private void initializeChoiceGenerators(IntChoiceFromSet icsCG, Integer[] cgChoices) { if (choiceCounter <= choiceUpperBound && !cgMap.containsValue(choiceCounter)) { // Update the choices of the first CG and add '-1' @@ -185,14 +194,15 @@ public class StateReducer extends ListenerAdapter { // Initialize backtrack set that stores all the explored backtrack lists maxUpperBound = cgChoices.length; // All the choices are always the same so we only need to update it once - choices = new Integer[cgChoices.length + 1]; - System.arraycopy(cgChoices, 0, choices, 0, cgChoices.length); - choices[choices.length - 1] = -1; + // Get the choice array and final choice in the array + choices = cgChoices; + // Make a copy of choices as reference + refChoices = copyChoices(choices); String firstChoiceListString = buildStringFromChoiceList(choices); backtrackSet.add(firstChoiceListString); } IntChoiceFromSet setCG = setNewCG(icsCG); - cgMap.put(setCG, choices[choiceCounter]); + cgMap.put(setCG, refChoices[choiceCounter]); } else { // We repeat the same trace if a state match is not found yet IntChoiceFromSet setCG = setNewCG(icsCG); @@ -225,6 +235,14 @@ public class StateReducer extends ListenerAdapter { } } + private void setDoneUnusedCG() { + // Set done every CG in the unused CG set + for (IntChoiceFromSet cg : unusedCG) { + cg.setDone(); + } + unusedCG.clear(); + } + private void resetAllCGs() { // Extract the event numbers that have backtrack lists Set eventSet = backtrackMap.keySet(); @@ -249,11 +267,7 @@ public class StateReducer extends ListenerAdapter { cg.setDone(); } } - // Set done every CG in the unused CG set - for (IntChoiceFromSet cg : unusedCG) { - cg.setDone(); - } - unusedCG.clear(); + setDoneUnusedCG(); saveVisitedStates(); } @@ -293,10 +307,11 @@ public class StateReducer extends ListenerAdapter { currVisitedStates.clear(); } - private void updateChoices(IntChoiceFromSet icsCG) { + private void updateChoicesForNewExecution(IntChoiceFromSet icsCG) { if (choices == null || choices != icsCG.getAllChoices()) { currCG = icsCG; choices = icsCG.getAllChoices(); + refChoices = copyChoices(choices); // Reset a few things for the sub-graph resetReadWriteAnalysis(); choiceCounter = 0; @@ -310,7 +325,8 @@ public class StateReducer extends ListenerAdapter { choiceCounter++; // Do this for every CG after finishing each backtrack list // We try to update the CG with a backtrack list if the state has been visited multiple times - if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) { + //if ((icsCG.getNextChoice() == -1 || choiceCounter > 1) && cgMap.containsKey(icsCG)) { + if ((!icsCG.hasMoreChoices() || choiceCounter > 1) && cgMap.containsKey(icsCG)) { int event = cgMap.get(icsCG); LinkedList choiceLists = backtrackMap.get(event); if (choiceLists != null && choiceLists.peekFirst() != null) { @@ -332,6 +348,29 @@ public class StateReducer extends ListenerAdapter { } } + private void checkAndEnforceFairScheduling(IntChoiceFromSet icsCG) { + // Check the next choice and if the value is not the same as the expected then force the expected value + int choiceIndex = (choiceCounter - 1) % refChoices.length; + if (choices[choiceIndex] != icsCG.getNextChoiceIndex()) { + int expectedChoice = refChoices[choiceIndex]; + int currCGIndex = icsCG.getNextChoiceIndex(); + if ((currCGIndex >= 0) && (currCGIndex < refChoices.length)) { + icsCG.setChoice(currCGIndex, expectedChoice); + } + } + } + + private boolean terminateCurrentExecution() { + // We need to check all the states that have just been visited + // Often a transition (choice/event) can result into forwarding/backtracking to a number of states + for(Integer stateId : justVisitedStates) { + if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) { + return true; + } + } + return false; + } + @Override public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator currentCG) { @@ -349,11 +388,14 @@ public class StateReducer extends ListenerAdapter { if (currentCG instanceof IntChoiceFromSet) { IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG; // Update the current pointer to the current set of choices - updateChoices(icsCG); + updateChoicesForNewExecution(icsCG); // Check if we have seen this state or this state contains cycles that involve all events - if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) { + if (terminateCurrentExecution()) { exploreNextBacktrackSets(icsCG); } + justVisitedStates.clear(); + // If we don't see a fair scheduling of events/choices then we have to enforce it + checkAndEnforceFairScheduling(icsCG); // Update the VOD graph always with the latest updateVODGraph(icsCG.getNextChoice()); } @@ -375,7 +417,7 @@ public class StateReducer extends ListenerAdapter { prevChoiceValue = currChoiceValue; } - private void mapStateToEvent(Search search) { + private void mapStateToEvent(Search search, int stateId) { // Insert state ID and event choice into the map HashSet eventSet; if (stateToEventMap.containsKey(stateId)) { @@ -391,9 +433,10 @@ public class StateReducer extends ListenerAdapter { if (stateReductionMode) { // Update the state variables // Line 19 in the paper page 11 (see the heading note above) - stateId = search.getStateId(); + int stateId = search.getStateId(); currVisitedStates.add(stateId); - mapStateToEvent(search); + mapStateToEvent(search, stateId); + justVisitedStates.add(stateId); } } @@ -481,11 +524,11 @@ public class StateReducer extends ListenerAdapter { // Do the analysis to get Read and Write accesses to fields ReadWriteSet rwSet; // We already have an entry - if (readWriteFieldsMap.containsKey(choices[currentChoice])) { - rwSet = readWriteFieldsMap.get(choices[currentChoice]); + if (readWriteFieldsMap.containsKey(refChoices[currentChoice])) { + rwSet = readWriteFieldsMap.get(refChoices[currentChoice]); } else { // We need to create a new entry rwSet = new ReadWriteSet(); - readWriteFieldsMap.put(choices[currentChoice], rwSet); + readWriteFieldsMap.put(refChoices[currentChoice], rwSet); } int objectId = ((JVMFieldInstruction) executedInsn).getFieldInfo().getClassInfo().getClassObjectRef(); // Record the field in the map @@ -569,19 +612,17 @@ public class StateReducer extends ListenerAdapter { } int maxListLength = choiceUpperBound + 1; int listLength = maxListLength - conflictEventNumber; - Integer[] newChoiceList = new Integer[listLength + 1]; + Integer[] newChoiceList = new Integer[listLength]; // Put the conflicting event numbers first and reverse the order - newChoiceList[0] = choices[currentChoice]; - newChoiceList[1] = choices[conflictEventNumber]; + newChoiceList[0] = refChoices[currentChoice]; + newChoiceList[1] = refChoices[conflictEventNumber]; // Put the rest of the event numbers into the array starting from the minimum to the upper bound for (int i = conflictEventNumber + 1, j = 2; j < listLength; i++) { - if (choices[i] != choices[currentChoice]) { - newChoiceList[j] = choices[i]; + if (refChoices[i] != refChoices[currentChoice]) { + newChoiceList[j] = refChoices[i]; j++; } } - // Set the last element to '-1' as the end of the sequence - newChoiceList[newChoiceList.length - 1] = -1; checkAndAddBacktrackList(backtrackChoiceLists, newChoiceList); // The start index for the recursion is always 1 (from the main branch) } else { // This is a sub-graph @@ -589,24 +630,22 @@ public class StateReducer extends ListenerAdapter { if (currCG != null && cgMap.containsKey(currCG)) { int backtrackListIndex = cgMap.get(currCG); backtrackChoiceLists = backtrackMap.get(backtrackListIndex); - int listLength = choices.length; + int listLength = refChoices.length; Integer[] newChoiceList = new Integer[listLength]; // Copy everything before the conflict number for (int i = 0; i < conflictEventNumber; i++) { - newChoiceList[i] = choices[i]; + newChoiceList[i] = refChoices[i]; } // Put the conflicting events - newChoiceList[conflictEventNumber] = choices[currentChoice]; - newChoiceList[conflictEventNumber + 1] = choices[conflictEventNumber]; + newChoiceList[conflictEventNumber] = refChoices[currentChoice]; + newChoiceList[conflictEventNumber + 1] = refChoices[conflictEventNumber]; // Copy the rest for (int i = conflictEventNumber + 1, j = conflictEventNumber + 2; j < listLength - 1; i++) { - if (choices[i] != choices[currentChoice]) { - newChoiceList[j] = choices[i]; + if (refChoices[i] != refChoices[currentChoice]) { + newChoiceList[j] = refChoices[i]; j++; } } - // Set the last element to '-1' as the end of the sequence - newChoiceList[newChoiceList.length - 1] = -1; checkAndAddBacktrackList(backtrackChoiceLists, newChoiceList); } } @@ -690,7 +729,7 @@ public class StateReducer extends ListenerAdapter { public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) { if (stateReductionMode) { if (isInitialized) { - int currentChoice = (choiceCounter % (choices.length - 1)) - 1; + int currentChoice = (choiceCounter % refChoices.length) - 1; if (currentChoice < 0) { // We do not compute the conflicts for the choice '-1' return; @@ -718,10 +757,10 @@ public class StateReducer extends ListenerAdapter { // one by one as this recursively checks backward when backtrack set is revisited and executed. for (int eventNumber = currentChoice - 1; eventNumber >= 0; eventNumber--) { // Skip if this event number does not have any Read/Write set - if (!readWriteFieldsMap.containsKey(choices[eventNumber])) { + if (!readWriteFieldsMap.containsKey(refChoices[eventNumber])) { continue; } - ReadWriteSet rwSet = readWriteFieldsMap.get(choices[eventNumber]); + ReadWriteSet rwSet = readWriteFieldsMap.get(refChoices[eventNumber]); int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef(); // 1) Check for conflicts with Write fields for both Read and Write instructions if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) && @@ -732,7 +771,7 @@ public class StateReducer extends ListenerAdapter { // If it has been serviced before, we just skip this if (recordConflictPair(currentChoice, eventNumber)) { // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above) - if (vm.isNewState() || isReachableInVODGraph(choices[currentChoice], choices[currentChoice-1])) { + if (vm.isNewState() || isReachableInVODGraph(refChoices[currentChoice], refChoices[currentChoice-1])) { createBacktrackChoiceList(currentChoice, eventNumber); // Break if a conflict is found! break; diff --git a/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java b/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java index 8762ba0..4a7b442 100644 --- a/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java +++ b/src/main/gov/nasa/jpf/vm/choice/NumberChoiceFromList.java @@ -240,4 +240,16 @@ public abstract class NumberChoiceFromList extends ChoiceGener public void setNewValues(T[] vals) { values = vals; } + + public int getNextChoiceIndex() { + return count; + } + + public void setChoice(int idx, T value) { + if ((idx >= 0) && (idx < values.length)) { + values[idx] = value; + } else { + throw new JPFException("illegal value " + idx + " for array index"); + } + } } -- 2.34.1