Adding reachability analysis when state matching occurs.
authorrtrimana <rtrimana@uci.edu>
Tue, 14 Apr 2020 23:24:10 +0000 (16:24 -0700)
committerrtrimana <rtrimana@uci.edu>
Tue, 14 Apr 2020 23:24:10 +0000 (16:24 -0700)
main.jpf
src/main/gov/nasa/jpf/listener/DPORStateReducer.java

index 1742858..81a40dc 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -8,8 +8,8 @@ target = main
 #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducer
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.StateReducer
 ##listener=gov.nasa.jpf.listener.ConflictTrackerOld,gov.nasa.jpf.listener.DPORStateReducer
-listener=gov.nasa.jpf.listener.ConflictTrackerOld
-#listener=gov.nasa.jpf.listener.DPORStateReducer
+#listener=gov.nasa.jpf.listener.ConflictTrackerOld
+listener=gov.nasa.jpf.listener.DPORStateReducer
 #listener=gov.nasa.jpf.listener.DPORStateReducer,gov.nasa.jpf.listener.ConflictTrackerOld
 
 # Potentially conflicting variables
@@ -48,7 +48,7 @@ debug_mode=true
 
 # Debug mode for StateReducer
 printout_state_transition=true
-activate_state_reduction=false
+#activate_state_reduction=false
 
 # Timeout in minutes (default is 0 which means no timeout)
 timeout=1440
index 22cc82f..c8c7806 100644 (file)
@@ -39,12 +39,13 @@ import java.util.*;
  * This DPOR implementation is augmented by the algorithm presented in this SPIN paper:
  * http://spinroot.com/spin/symposia/ws08/spin2008_submission_33.pdf
  *
- * The algorithm is presented on page 11 of the paper. Basically, we create a graph G
- * (i.e., visible operation dependency graph)
- * that maps inter-related threads/sub-programs that trigger state changes.
- * The key to this approach is that we evaluate graph G in every iteration/recursion to
- * only update the backtrack sets of the threads/sub-programs that are reachable in graph G
- * from the currently running thread/sub-program.
+ * The algorithm is presented on page 11 of the paper. Basically, we have a graph G
+ * (i.e., visible operation dependency graph).
+ * This DPOR implementation actually fixes the algorithm in the SPIN paper that does not
+ * consider cases where a state could be matched early. In this new algorithm/implementation,
+ * each run is terminated iff:
+ * - we find a state that matches a state in a previous run, or
+ * - we have a matched state in the current run that consists of cycles that contain all choices/events.
  */
 public class DPORStateReducer extends ListenerAdapter {
 
@@ -74,14 +75,8 @@ public class DPORStateReducer extends ListenerAdapter {
   private ArrayList<BacktrackPoint> backtrackPointList;           // Record backtrack points (CG, state Id, and choice)
   private HashMap<Integer, HashSet<Integer>> conflictPairMap;     // Record conflicting events
   private HashSet<String> doneBacktrackSet;                       // Record state ID and trace already constructed
-  private HashMap<Integer,Integer> newStateEventMap;              // Record event producing a new state ID
   private HashMap<Integer, ReadWriteSet> readWriteFieldsMap;      // Record fields that are accessed
-  private HashMap<Integer, RestorableVMState> restorableStateMap; // Maps state IDs to the restorable state object
-
-  // Visible operation dependency graph implementation (SPIN paper) related fields
-  private int currChoiceValue;
-  private int prevChoiceValue;
-  private HashMap<Integer, HashSet<Integer>> vodGraphMap; // Visible operation dependency graph (VOD graph)
+  private HashMap<Integer, RestorableState> restorableStateMap;   // Maps state IDs to the restorable state object
 
   // Boolean states
   private boolean isBooleanCGFlipped;
@@ -286,10 +281,7 @@ public class DPORStateReducer extends ListenerAdapter {
                   // Check and record a backtrack set for just once!
                   if (isConflictFound(nextInsn, eventCounter, currentChoice, 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, vm)) {
-                      createBacktrackingPoint(currentChoice, eventCounter);
-                    }
+                    createBacktrackingPoint(currentChoice, eventCounter);
                   }
                 }
               }
@@ -325,6 +317,14 @@ public class DPORStateReducer extends ListenerAdapter {
       writeSet.put(field, objectId);
     }
 
+    public Set<String> getReadSet() {
+      return readSet.keySet();
+    }
+
+    public Set<String> getWriteSet() {
+      return writeSet.keySet();
+    }
+
     public boolean readFieldExists(String field) {
       return readSet.containsKey(field);
     }
@@ -365,6 +365,25 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
+  // This class compactly stores: 1) restorable VM state, and 2) global choice counter
+  private class RestorableState {
+    private RestorableVMState restorableState;
+    private int choiceCounter;
+
+    public RestorableState (RestorableVMState restState, int choCtr) {
+      restorableState = restState;
+      choiceCounter = choCtr;
+    }
+
+    public RestorableVMState getRestorableState() {
+      return restorableState;
+    }
+
+    public int getChoiceCounter() {
+      return choiceCounter;
+    }
+  }
+
   // -- CONSTANTS
   private final static String DO_CALL_METHOD = "doCall";
   // We exclude fields that come from libraries (Java and Groovy), and also the infrastructure
@@ -397,14 +416,12 @@ public class DPORStateReducer extends ListenerAdapter {
         icsCG.setChoice(currCGIndex, expectedChoice);
       }
     }
-    // Update current choice
-    currChoiceValue = refChoices[choiceIndex];
     // Record state ID and choice/event as backtrack point
     int stateId = vm.getStateId();
     backtrackPointList.add(new BacktrackPoint(icsCG, stateId, refChoices[choiceIndex]));
     // Store restorable state object for this state (always store the latest)
     RestorableVMState restorableState = vm.getRestorableState();
-    restorableStateMap.put(stateId, restorableState);
+    restorableStateMap.put(stateId, new RestorableState(restorableState, choiceCounter));
   }
 
   private Integer[] copyChoices(Integer[] choicesToCopy) {
@@ -456,12 +473,7 @@ public class DPORStateReducer extends ListenerAdapter {
     backtrackPointList = new ArrayList<>();
     conflictPairMap = new HashMap<>();
     doneBacktrackSet = new HashSet<>();
-    newStateEventMap = new HashMap<>();
     readWriteFieldsMap = new HashMap<>();
-    // VOD graph
-    currChoiceValue = 0;
-    prevChoiceValue = -1;
-    vodGraphMap = new HashMap<>();
     // Booleans
     isEndOfExecution = false;
   }
@@ -498,8 +510,7 @@ public class DPORStateReducer extends ListenerAdapter {
       stateToEventMap.put(stateId, eventSet);
     }
     justVisitedStates.add(stateId);
-    // Update the VOD graph when there is a new state
-    updateVODGraph(search.getVM());
+    analyzeReachabilityAndCreateBacktrackPoints(search.getVM(), stateId);
   }
 
   // --- Functions related to Read/Write access analysis on shared fields
@@ -672,7 +683,7 @@ public class DPORStateReducer extends ListenerAdapter {
                        int hiStateId = backtrackStateQ.peek();
                        // Restore the state first if necessary
                        if (vm.getStateId() != hiStateId) {
-                               RestorableVMState restorableState = restorableStateMap.get(hiStateId);
+                               RestorableVMState restorableState = restorableStateMap.get(hiStateId).getRestorableState();
                                vm.restoreState(restorableState);
                        }
                        // Set the backtrack CG
@@ -702,6 +713,39 @@ public class DPORStateReducer extends ListenerAdapter {
     return rwSet;
   }
 
+  private boolean isConflictFound(int eventCounter, int currentChoice) {
+
+    int actualCurrCho = currentChoice % refChoices.length;
+    // Skip if this event does not have any Read/Write set or the two events are basically the same event (number)
+    if (!readWriteFieldsMap.containsKey(eventCounter) ||
+            choices[actualCurrCho] == backtrackPointList.get(eventCounter).getChoice()) {
+      return false;
+    }
+    // Current R/W set
+    ReadWriteSet currRWSet = readWriteFieldsMap.get(currentChoice);
+    // R/W set of choice/event that may have a potential conflict
+    ReadWriteSet evtRWSet = readWriteFieldsMap.get(eventCounter);
+    // Check for conflicts with Read and Write fields for Write instructions
+    Set<String> currWriteSet = currRWSet.getWriteSet();
+    for(String writeField : currWriteSet) {
+      int currObjId = currRWSet.writeFieldObjectId(writeField);
+      if ((evtRWSet.readFieldExists(writeField) && evtRWSet.readFieldObjectId(writeField) == currObjId) ||
+          (evtRWSet.writeFieldExists(writeField) && evtRWSet.writeFieldObjectId(writeField) == currObjId)) {
+        return true;
+      }
+    }
+    // Check for conflicts with Write fields for Read instructions
+    Set<String> currReadSet = currRWSet.getReadSet();
+    for(String readField : currReadSet) {
+      int currObjId = currRWSet.readFieldObjectId(readField);
+      if (evtRWSet.writeFieldExists(readField) && evtRWSet.writeFieldObjectId(readField) == currObjId) {
+        return true;
+      }
+    }
+    // Return false if no conflict is found
+    return false;
+  }
+
   private boolean isConflictFound(Instruction nextInsn, int eventCounter, int currentChoice, String fieldClass) {
 
     int actualCurrCho = currentChoice % refChoices.length;
@@ -797,70 +841,29 @@ public class DPORStateReducer extends ListenerAdapter {
     }
   }
 
-  // --- Functions related to the visible operation dependency graph implementation discussed in the SPIN paper
-
-  // This method checks whether a choice/event (transition) is reachable from the choice/event that produces
-  // the state right before this state in the VOD graph
-  // We use a BFS algorithm for this purpose
-  private boolean isReachableInVODGraph(int currentChoice, VM vm) {
-    // Current event
-    int choiceIndex = currentChoice % refChoices.length;
-    int currEvent = refChoices[choiceIndex];
-    // Previous event
-    int stateId = vm.getStateId();  // A state that has been seen
-    int prevEvent = newStateEventMap.get(stateId);
-    // Only start traversing the graph if prevEvent has an outgoing edge
-    if (vodGraphMap.containsKey(prevEvent)) {
-      // Record visited choices as we search in the graph
-      HashSet<Integer> visitedChoice = new HashSet<>();
-      visitedChoice.add(prevEvent);
-      // Get the first nodes to visit (the neighbors of prevEvent)
-      LinkedList<Integer> nodesToVisit = new LinkedList<>();
-      nodesToVisit.addAll(vodGraphMap.get(prevEvent));
-      // Traverse the graph using BFS
-      while (!nodesToVisit.isEmpty()) {
-        int choice = nodesToVisit.removeFirst();
-        if (choice == currEvent) {
-          return true;
-        }
-        if (visitedChoice.contains(choice)) { // If there is a loop then just continue the exploration
-          continue;
-        }
-        // 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;
+  // --- Functions related to the reachability analysis when there is a state match
+
+  // We use backtrackPointsList to analyze the reachable states/events when there is a state match:
+  // 1) Whenever there is state match, there is a cycle of events
+  // 2) We need to analyze and find conflicts for the reachable choices/events in the cycle
+  // 3) Then we create a new backtrack point for every new conflict
+  private void analyzeReachabilityAndCreateBacktrackPoints(VM vm, int stateId) {
+    // Perform this analysis only when there is a state match
+    if (!vm.isNewState()) {
+      if (restorableStateMap.containsKey(stateId)) {
+        // Find the choice/event that marks the start of this cycle: first choice we explore for conflicts
+        int conflictChoice = restorableStateMap.get(stateId).getChoiceCounter();
+        int currentChoice = choiceCounter - 1;
+        // Find conflicts between choices/events in this cycle (we scan forward in the cycle, not backward)
+        while (conflictChoice < currentChoice) {
+          for (int eventCounter = conflictChoice + 1; eventCounter <= currentChoice; eventCounter++) {
+            if (isConflictFound(eventCounter, conflictChoice) && isNewConflict(conflictChoice, eventCounter)) {
+              createBacktrackingPoint(conflictChoice, eventCounter);
             }
-            nodesToVisit.addLast(nextNode);
           }
+          conflictChoice++;
         }
       }
     }
-    return false;
-  }
-
-  private void updateVODGraph(VM vm) {
-    // Do this only if it is a new state
-    if (vm.isNewState()) {
-      // 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;
-      // Map this state ID to the event (transition) that produces it
-      newStateEventMap.put(vm.getStateId(), currChoiceValue);
-    }
   }
 }