Reimplementing DPOR Phase 2: VOD graph building and traversal; completing R/W and...

diff --git a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
index a688754..8c6a1d6 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/DPORStateReducer.java
@@ -58,20 +58,27 @@ public class DPORStateReducer extends ListenerAdapter {
   private Transition transition;
 
   // DPOR-related fields
   private Transition transition;
 
   // DPOR-related fields

+  // Basic information

   private Integer[] choices;
   private Integer[] refChoices;
   private int choiceCounter;
   private int maxEventChoice;
   private Integer[] choices;
   private Integer[] refChoices;
   private int choiceCounter;
   private int maxEventChoice;

-  // Record CGs for backtracking points
-  private List<IntChoiceFromSet> cgList;

   // Data structure to track the events seen by each state to track cycles (containing all events) for termination
   // Data structure to track the events seen by each state to track cycles (containing all events) for termination

-  private HashMap<Integer, HashSet<Integer>> stateToEventMap;
+  private HashSet<Integer> currVisitedStates; // States being visited in the current execution

   private HashSet<Integer> justVisitedStates; // States just visited in the previous choice/event
   private HashSet<Integer> prevVisitedStates; // States visited in the previous execution
   private HashSet<Integer> justVisitedStates; // States just visited in the previous choice/event
   private HashSet<Integer> prevVisitedStates; // States visited in the previous execution

-  private HashSet<Integer> currVisitedStates; // States being visited in the current execution
-  // Data structure to analyze field Read/Write accesses
-  private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;
-  private HashMap<Integer, HashSet<Integer>> conflictPairMap;
+  private HashMap<Integer, HashSet<Integer>> stateToEventMap;
+  // Data structure to analyze field Read/Write accesses and conflicts
+  private HashMap<Integer, LinkedList<Integer[]>> backtrackMap; // Track created backtracking points
+  private Stack<BacktrackPoint> btrckPtsStack;                  // Stack that stores backtracking points
+  private List<IntChoiceFromSet> cgList;                        // Record CGs for backtracking points
+  private HashSet<IntChoiceFromSet> btrckCGSet;                 // Set that records all the backtrack CGs
+  private HashMap<Integer, HashSet<Integer>> conflictPairMap;   // Record conflicting events
+  private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;    // Record fields that are accessed
+
+  // Visible operation dependency graph implementation (SPIN paper) related fields
+  private int prevChoiceValue;
+  private HashMap<Integer, HashSet<Integer>> vodGraphMap; // Visible operation dependency graph (VOD graph)

 
   // Boolean states
   private boolean isBooleanCGFlipped;
 
   // Boolean states
   private boolean isBooleanCGFlipped;


@@ -89,13 +96,21 @@ public class DPORStateReducer extends ListenerAdapter {
     refChoices = null;
     choiceCounter = 0;
     maxEventChoice = 0;
     refChoices = null;
     choiceCounter = 0;
     maxEventChoice = 0;

-    cgList = new ArrayList<>();
-    stateToEventMap = new HashMap<>();
+    // Cycle tracking
+    currVisitedStates = new HashSet<>();

     justVisitedStates = new HashSet<>();
     prevVisitedStates = new HashSet<>();
     justVisitedStates = new HashSet<>();
     prevVisitedStates = new HashSet<>();

-    currVisitedStates = new HashSet<>();
-    readWriteFieldsMap = new HashMap<>();
+    stateToEventMap = new HashMap<>();
+    // Backtracking
+    backtrackMap = new HashMap<>();
+    btrckPtsStack = new Stack<>();
+    btrckCGSet = new HashSet<>();
+    cgList = new ArrayList<>();

     conflictPairMap = new HashMap<>();
     conflictPairMap = new HashMap<>();

+    readWriteFieldsMap = new HashMap<>();
+    // VOD graph
+    prevChoiceValue = -1;
+    vodGraphMap = new HashMap<>();

     // Booleans
     isBooleanCGFlipped = false;
   }
     // Booleans
     isBooleanCGFlipped = false;
   }


@@ -182,6 +197,8 @@ public class DPORStateReducer extends ListenerAdapter {
           // Record the max event choice (the last element of the choice array)
           maxEventChoice = choices[choices.length - 1];
         }
           // Record the max event choice (the last element of the choice array)
           maxEventChoice = choices[choices.length - 1];
         }

+        icsCG.setNewValues(choices);
+        icsCG.reset();

         // Use a modulo since choiceCounter is going to keep increasing
         int choiceIndex = choiceCounter % choices.length;
         icsCG.advance(choices[choiceIndex]);
         // Use a modulo since choiceCounter is going to keep increasing
         int choiceIndex = choiceCounter % choices.length;
         icsCG.advance(choices[choiceIndex]);


@@ -210,6 +227,8 @@ public class DPORStateReducer extends ListenerAdapter {
         checkAndEnforceFairScheduling(icsCG);
         // Map state to event
         mapStateToEvent(icsCG.getNextChoice());
         checkAndEnforceFairScheduling(icsCG);
         // Map state to event
         mapStateToEvent(icsCG.getNextChoice());

+        // Update the VOD graph always with the latest
+        updateVODGraph(icsCG.getNextChoice());

         // Check if we have seen this state or this state contains cycles that involve all events
         if (terminateCurrentExecution()) {
           exploreNextBacktrackSets(icsCG);
         // Check if we have seen this state or this state contains cycles that involve all events
         if (terminateCurrentExecution()) {
           exploreNextBacktrackSets(icsCG);


@@ -227,10 +246,10 @@ public class DPORStateReducer extends ListenerAdapter {
       ChoiceGenerator<?> cg = vm.getChoiceGenerator();
       if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
         int currentChoice = choiceCounter - 1;  // Accumulative choice w.r.t the current trace
       ChoiceGenerator<?> cg = vm.getChoiceGenerator();
       if (cg instanceof IntChoiceFromSet || cg instanceof IntIntervalGenerator) {
         int currentChoice = choiceCounter - 1;  // Accumulative choice w.r.t the current trace

-        //if (getCurrentChoice(vm) < 0) { // If choice is -1 then skip

         if (currentChoice < 0) { // If choice is -1 then skip
           return;
         }
         if (currentChoice < 0) { // If choice is -1 then skip
           return;
         }

+        currentChoice = checkAndAdjustChoice(currentChoice, vm);

         // Record accesses from executed instructions
         if (executedInsn instanceof JVMFieldInstruction) {
           // Analyze only after being initialized
         // Record accesses from executed instructions
         if (executedInsn instanceof JVMFieldInstruction) {
           // Analyze only after being initialized


@@ -250,23 +269,13 @@ public class DPORStateReducer extends ListenerAdapter {
             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
             if (!isFieldExcluded(fieldClass)) {
               // Check for conflict (go backward from current choice and get the first conflict)
             String fieldClass = ((JVMFieldInstruction) nextInsn).getFieldInfo().getFullName();
             if (!isFieldExcluded(fieldClass)) {
               // Check for conflict (go backward from current choice and get the first conflict)

-              for (int evtCntr = currentChoice - 1; evtCntr >= 0; evtCntr--) {
-                if (!readWriteFieldsMap.containsKey(evtCntr)) { // Skip if this event does not have any Read/Write set
-                  continue;
-                }
-                ReadWriteSet rwSet = readWriteFieldsMap.get(evtCntr);
-                int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
+              for (int eventCounter = currentChoice - 1; eventCounter >= 0; eventCounter--) {

                 // Check for conflicts with Write fields for both Read and Write instructions
                 // Check for conflicts with Write fields for both Read and Write instructions

-                if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
-                      rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
-                     (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
-                      rwSet.readFieldObjectId(fieldClass) == currObjId)) {
-                  // Check and record a backtrack set for just once!
-                  if (successfullyRecordConflictPair(currentChoice, evtCntr)) {
-                    // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
-//                    if (vm.isNewState() || isReachableInVODGraph(refChoices[currentChoice], refChoices[currentChoice-1])) {
-//                      createBacktrackChoiceList(currentChoice, eventNumber);
-//                    }
+                // Check and record a backtrack set for just once!
+                if (isConflictFound(nextInsn, eventCounter, fieldClass) && isNewConflict(currentChoice, eventCounter)) {
+                  // Lines 4-8 of the algorithm in the paper page 11 (see the heading note above)
+                  if (vm.isNewState() || isReachableInVODGraph(currentChoice)) {
+                    createBacktrackingPoint(currentChoice, eventCounter);

                   }
                 }
               }
                   }
                 }
               }


@@ -279,7 +288,9 @@ public class DPORStateReducer extends ListenerAdapter {
 
 
   // == HELPERS
 
 
   // == HELPERS

-  // -- INNER CLASS
+
+  // -- INNER CLASSES
+

   // This class compactly stores Read and Write field sets
   // We store the field name and its object ID
   // Sharing the same field means the same field name and object ID
   // This class compactly stores Read and Write field sets
   // We store the field name and its object ID
   // Sharing the same field means the same field name and object ID


@@ -317,6 +328,25 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

+  // This class compactly stores backtracking points: 1) backtracking ChoiceGenerator, and 2) backtracking choices
+  private class BacktrackPoint {
+    private IntChoiceFromSet backtrackCG; // CG to backtrack from
+    private Integer[] backtrackChoices;   // Choices to set for this backtrack CG
+
+    public BacktrackPoint(IntChoiceFromSet cg, Integer[] choices) {
+      backtrackCG = cg;
+      backtrackChoices = choices;
+    }
+
+    public IntChoiceFromSet getBacktrackCG() {
+      return backtrackCG;
+    }
+
+    public Integer[] getBacktrackChoices() {
+      return backtrackChoices;
+    }
+  }
+

   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure


@@ -455,6 +485,9 @@ public class DPORStateReducer extends ListenerAdapter {
       }
       // Get the iterated object whose property is accessed
       ElementInfo eiAccessObj = VM.getVM().getHeap().get(frameSlots[1]);
       }
       // Get the iterated object whose property is accessed
       ElementInfo eiAccessObj = VM.getVM().getHeap().get(frameSlots[1]);

+      if (eiAccessObj == null) {
+        return;
+      }

       // We exclude library classes (they start with java, org, etc.) and some more
       String objClassName = eiAccessObj.getClassInfo().getName();
       if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName) ||
       // We exclude library classes (they start with java, org, etc.) and some more
       String objClassName = eiAccessObj.getClassInfo().getName();
       if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, objClassName) ||


@@ -476,6 +509,43 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
     }
   }
 

+  private int checkAndAdjustChoice(int currentChoice, VM vm) {
+    // If current choice is not the same, then this is caused by the firing of IntIntervalGenerator
+    // for certain method calls in the infrastructure, e.g., eventSince()
+    int currChoiceInd = currentChoice % refChoices.length;
+    int currChoiceFromCG = getCurrentChoice(vm);
+    if (currChoiceInd != currChoiceFromCG) {
+      currentChoice = (currentChoice - currChoiceInd) + currChoiceFromCG;
+    }
+    return currentChoice;
+  }
+
+  private void createBacktrackingPoint(int currentChoice, int confEvtNum) {
+
+    // 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}
+    // for the original set {0, 1, 2, 3}
+    Integer[] newChoiceList = new Integer[refChoices.length];
+    // Put the conflicting event numbers first and reverse the order
+    int actualCurrCho = currentChoice % refChoices.length;
+    int actualConfEvtNum = confEvtNum % refChoices.length;
+    newChoiceList[0] = refChoices[actualCurrCho];
+    newChoiceList[1] = refChoices[actualConfEvtNum];
+    // 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++) {
+      if (refChoices[i] != newChoiceList[0] && refChoices[i] != newChoiceList[1]) {
+        newChoiceList[j] = refChoices[i];
+        j++;
+      }
+    }
+    // Record the backtracking point in the stack as well
+    IntChoiceFromSet backtrackCG = cgList.get(confEvtNum);
+    BacktrackPoint backtrackPoint = new BacktrackPoint(backtrackCG, newChoiceList);
+    btrckPtsStack.push(backtrackPoint);
+    // Also record the CG in the set
+    btrckCGSet.add(backtrackCG);
+  }
+

   private boolean excludeThisForItContains(String[] excludedStrings, String className) {
     for (String excludedField : excludedStrings) {
       if (className.contains(excludedField)) {
   private boolean excludeThisForItContains(String[] excludedStrings, String className) {
     for (String excludedField : excludedStrings) {
       if (className.contains(excludedField)) {


@@ -503,11 +573,32 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
     return false;
   }
 

+  // TODO: THIS METHOD IS STILL UNTESTED AT THIS POINT

   private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {
   private void exploreNextBacktrackSets(IntChoiceFromSet icsCG) {

-    // Save all the visited states when starting a new execution of trace
-    prevVisitedStates.addAll(currVisitedStates);
-    currVisitedStates.clear();
-
+    // We try to update the CG with a backtrack list if the state has been visited multiple times
+    if (icsCG.getNextChoiceIndex() > 0) {
+      if (btrckPtsStack.empty()) {
+        // TODO: PROBABLY NEED TO DO CONTEXT SWITCHING HERE
+        return;
+      }
+      BacktrackPoint backtrackPoint = btrckPtsStack.pop();
+      Integer[] choiceList = backtrackPoint.getBacktrackChoices();
+      IntChoiceFromSet backtrackCG = backtrackPoint.getBacktrackCG();
+      // Deploy the new choice list for this CG
+      backtrackCG.setNewValues(choiceList);
+      backtrackCG.reset();
+      // Clear unused CGs
+      for(IntChoiceFromSet cg : cgList) {
+        if (!btrckCGSet.contains(cg)) {
+          cg.setDone();
+        }
+      }
+      cgList.clear();
+      btrckCGSet.clear();
+      // Save all the visited states when starting a new execution of trace
+      prevVisitedStates.addAll(currVisitedStates);
+      currVisitedStates.clear();
+    }

   }
 
   private int getCurrentChoice(VM vm) {
   }
 
   private int getCurrentChoice(VM vm) {


@@ -535,6 +626,23 @@ public class DPORStateReducer extends ListenerAdapter {
     return rwSet;
   }
 
     return rwSet;
   }
 

+  private boolean isConflictFound(Instruction nextInsn, int eventCounter, String fieldClass) {
+    // Skip if this event does not have any Read/Write set
+    if (!readWriteFieldsMap.containsKey(eventCounter)) {
+      return false;
+    }
+    ReadWriteSet rwSet = readWriteFieldsMap.get(eventCounter);
+    int currObjId = ((JVMFieldInstruction) nextInsn).getFieldInfo().getClassInfo().getClassObjectRef();
+    // Check for conflicts with Write fields for both Read and Write instructions
+    if (((nextInsn instanceof WriteInstruction || nextInsn instanceof ReadInstruction) &&
+          rwSet.writeFieldExists(fieldClass) && rwSet.writeFieldObjectId(fieldClass) == currObjId) ||
+         (nextInsn instanceof WriteInstruction && rwSet.readFieldExists(fieldClass) &&
+          rwSet.readFieldObjectId(fieldClass) == currObjId)) {
+      return true;
+    }
+    return false;
+  }
+

   private boolean isFieldExcluded(String field) {
     // Check against "starts-with", "ends-with", and "contains" list
     if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) ||
   private boolean isFieldExcluded(String field) {
     // Check against "starts-with", "ends-with", and "contains" list
     if (excludeThisForItStartsWith(EXCLUDED_FIELDS_STARTS_WITH_LIST, field) ||


@@ -546,7 +654,7 @@ public class DPORStateReducer extends ListenerAdapter {
     return false;
   }
 
     return false;
   }
 

-  private boolean successfullyRecordConflictPair(int currentEvent, int eventNumber) {
+  private boolean isNewConflict(int currentEvent, int eventNumber) {

     HashSet<Integer> conflictSet;
     if (!conflictPairMap.containsKey(currentEvent)) {
       conflictSet = new HashSet<>();
     HashSet<Integer> conflictSet;
     if (!conflictPairMap.containsKey(currentEvent)) {
       conflictSet = new HashSet<>();


@@ -555,7 +663,7 @@ public class DPORStateReducer extends ListenerAdapter {
       conflictSet = conflictPairMap.get(currentEvent);
     }
     // If this conflict has been recorded before, we return false because
       conflictSet = conflictPairMap.get(currentEvent);
     }
     // If this conflict has been recorded before, we return false because

-    // we don't want to service this backtrack point twice
+    // we don't want to save this backtrack point twice

     if (conflictSet.contains(eventNumber)) {
       return false;
     }
     if (conflictSet.contains(eventNumber)) {
       return false;
     }


@@ -563,4 +671,62 @@ public class DPORStateReducer extends ListenerAdapter {
     conflictSet.add(eventNumber);
     return true;
   }
     conflictSet.add(eventNumber);
     return true;
   }

+
+  // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper
+
+  // This method checks whether a choice is reachable in the VOD graph from a reference choice (BFS algorithm)
+  //private boolean isReachableInVODGraph(int checkedChoice, int referenceChoice) {
+  private boolean isReachableInVODGraph(int currentChoice) {
+    // Extract previous and current events
+    int choiceIndex = currentChoice % refChoices.length;
+    int currEvent = refChoices[choiceIndex];
+    int prevEvent = refChoices[choiceIndex - 1];
+    // Record visited choices as we search in the graph
+    HashSet<Integer> visitedChoice = new HashSet<>();
+    visitedChoice.add(prevEvent);
+    LinkedList<Integer> nodesToVisit = new LinkedList<>();
+    // If the state doesn't advance as the threads/sub-programs are executed (basically there is no new state),
+    // there is a chance that the graph doesn't have new nodes---thus this check will return a null.
+    if (vodGraphMap.containsKey(prevEvent)) {
+      nodesToVisit.addAll(vodGraphMap.get(prevEvent));
+      while(!nodesToVisit.isEmpty()) {
+        int choice = nodesToVisit.getFirst();
+        if (choice == currEvent) {
+          return true;
+        }
+        if (visitedChoice.contains(choice)) { // If there is a loop then we don't find it
+          return false;
+        }
+        // Continue searching
+        visitedChoice.add(choice);
+        HashSet<Integer> choiceNextNodes = vodGraphMap.get(choice);
+        if (choiceNextNodes != null) {
+          // Add only if there is a mapping for next nodes
+          for (Integer nextNode : choiceNextNodes) {
+            // Skip cycles
+            if (nextNode == choice) {
+              continue;
+            }
+            nodesToVisit.addLast(nextNode);
+          }
+        }
+      }
+    }
+    return false;
+  }
+
+  private void updateVODGraph(int currChoiceValue) {
+    // Update the graph when we have the current choice value
+    HashSet<Integer> choiceSet;
+    if (vodGraphMap.containsKey(prevChoiceValue)) {
+      // If the key already exists, just retrieve it
+      choiceSet = vodGraphMap.get(prevChoiceValue);
+    } else {
+      // Create a new entry
+      choiceSet = new HashSet<>();
+      vodGraphMap.put(prevChoiceValue, choiceSet);
+    }
+    choiceSet.add(currChoiceValue);
+    prevChoiceValue = currChoiceValue;
+  }

 }
 }