Adding graph traversal to find cycles; adding debug mode for ConflictTracker.

diff --git a/main.jpf b/main.jpf
index 35b5ea4416cbd3dc5bec43696884389a0df22416..9ce7d13f67420d97c2fba09b1fbb5144ca71c35f 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -6,11 +6,11 @@ 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.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.StateReducerClean
 
 #listener=gov.nasa.jpf.listener.ConflictTracker,gov.nasa.jpf.listener.StateReducerClean

-#listener=gov.nasa.jpf.listener.ConflictTracker

 #listener=gov.nasa.jpf.listener.StateReducerClean
 #listener=gov.nasa.jpf.listener.StateReducerClean

-listener=gov.nasa.jpf.listener.StateReducer
+#listener=gov.nasa.jpf.listener.StateReducer

 
 # Potentially conflicting variables
 # Alarms
 
 # Potentially conflicting variables
 # Alarms


@@ -41,11 +41,12 @@ variables=currentLock
 # Potentially conflicting apps (we default to App1 and App2 for now)
 apps=App1,App2
 
 # Potentially conflicting apps (we default to App1 and App2 for now)
 apps=App1,App2
 

-# Tracking the location.mode variable conflict
-#track_location_var_conflict=true
+# Debug mode for ConflictTracker
+# We do not report any conflicts if the value is true
+debug_mode=true

 
 # Debug mode for StateReducer
 
 # Debug mode for StateReducer

-debug_state_transition=true
+#debug_state_transition=true

 #activate_state_reduction=true
 
 # Timeout in minutes (default is 0 which means no timeout)
 #activate_state_reduction=true
 
 # Timeout in minutes (default is 0 which means no timeout)

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index 384056ee12abc750d28c340af0749361d9d1237b..791a7dad4b2d67eb3e629a74f8bfb8d5b1158384 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -27,6 +27,7 @@ import gov.nasa.jpf.vm.bytecode.LocalVariableInstruction;
 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
 import gov.nasa.jpf.vm.bytecode.WriteInstruction;
 import gov.nasa.jpf.vm.bytecode.ReadInstruction;
 import gov.nasa.jpf.vm.bytecode.StoreInstruction;
 import gov.nasa.jpf.vm.bytecode.WriteInstruction;

+import gov.nasa.jpf.vm.choice.IntChoiceFromSet;

 
 import java.io.PrintWriter;
 
 
 import java.io.PrintWriter;
 


@@ -37,11 +38,13 @@ import java.util.*;
  **/
 
 public class ConflictTracker extends ListenerAdapter {
  **/
 
 public class ConflictTracker extends ListenerAdapter {

+  // Public graph: to allow the StateReducer class to access it
+  public static final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph
+  // Private

   private final PrintWriter out;
   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
   private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions
   private final PrintWriter out;
   private final HashSet<String> conflictSet = new HashSet<String>(); // Variables we want to track
   private final HashSet<String> appSet = new HashSet<String>(); // Apps we want to find their conflicts
   private final HashSet<String> manualSet = new HashSet<String>(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions

-  private final HashMap<Integer, Node> nodes = new HashMap<Integer, Node>(); // Nodes of a graph

   private HashSet<Transition> transitions = new HashSet<Transition>();
   private ArrayList<Update> currUpdates = new ArrayList<Update>();
   private long timeout;
   private HashSet<Transition> transitions = new HashSet<Transition>();
   private ArrayList<Update> currUpdates = new ArrayList<Update>();
   private long timeout;


@@ -54,12 +57,15 @@ public class ConflictTracker extends ListenerAdapter {
   private int id;
   private boolean manual = false;
   private boolean conflictFound = false;
   private int id;
   private boolean manual = false;
   private boolean conflictFound = false;

+  private int currentEvent = -1;
+  private boolean debugMode = false;

 
   private final String SET_LOCATION_METHOD = "setLocationMode";
   private final String LOCATION_VAR = "locationMode";
 
   public ConflictTracker(Config config, JPF jpf) {
     out = new PrintWriter(System.out, true);
 
   private final String SET_LOCATION_METHOD = "setLocationMode";
   private final String LOCATION_VAR = "locationMode";
 
   public ConflictTracker(Config config, JPF jpf) {
     out = new PrintWriter(System.out, true);

+    debugMode = config.getBoolean("debug_mode", false);

 
     String[] conflictVars = config.getStringArray("variables");
     // We are not tracking anything if it is null
 
     String[] conflictVars = config.getStringArray("variables");
     // We are not tracking anything if it is null


@@ -124,7 +130,8 @@ public class ConflictTracker extends ListenerAdapter {
       }
 
       //Check for conflict with the appropriate update set if we are not a manual transition
       }
 
       //Check for conflict with the appropriate update set if we are not a manual transition

-      if (confupdates != null && !u.isManual()) {
+      //If this is debug mode, then we do not report any conflicts
+      if (!debugMode && confupdates != null && !u.isManual()) {

         for(Update u2: confupdates) {
           if (conflicts(u, u2)) {
             //throw new RuntimeException(createErrorMessage(u, u2));
         for(Update u2: confupdates) {
           if (conflicts(u, u2)) {
             //throw new RuntimeException(createErrorMessage(u, u2));


@@ -174,13 +181,13 @@ public class ConflictTracker extends ListenerAdapter {
     return message;
   }
 
     return message;
   }
 

-  Edge createEdge(Node parent, Node current, Transition transition) {
+  Edge createEdge(Node parent, Node current, Transition transition, int evtNum) {

     //Check if this transition is explored.  If so, just skip everything
     if (transitions.contains(transition))
       return null;
 
     //Create edge
     //Check if this transition is explored.  If so, just skip everything
     if (transitions.contains(transition))
       return null;
 
     //Create edge

-    Edge e = new Edge(parent, current, transition, currUpdates);
+    Edge e = new Edge(parent, current, transition, evtNum, currUpdates);

     parent.addOutEdge(e);
 
     //Mark transition as explored
     parent.addOutEdge(e);
 
     //Mark transition as explored


@@ -218,12 +225,14 @@ public class ConflictTracker extends ListenerAdapter {
   static class Edge {
     Node source, destination;
     Transition transition;
   static class Edge {
     Node source, destination;
     Transition transition;

+    int eventNumber;

     ArrayList<Update> updates = new ArrayList<Update>();
     
     ArrayList<Update> updates = new ArrayList<Update>();
     

-    Edge(Node src, Node dst, Transition t, ArrayList<Update> _updates) {
+    Edge(Node src, Node dst, Transition t, int evtNum, ArrayList<Update> _updates) {

       this.source = src;
       this.destination = dst;
       this.transition = t;
       this.source = src;
       this.destination = dst;
       this.transition = t;

+      this.eventNumber = evtNum;

       this.updates.addAll(_updates);
     }
 
       this.updates.addAll(_updates);
     }
 


@@ -239,6 +248,8 @@ public class ConflictTracker extends ListenerAdapter {
       return transition;
     }
 
       return transition;
     }
 

+    int getEventNumber() { return eventNumber; }
+

     ArrayList<Update> getUpdates() {
       return updates;
     }
     ArrayList<Update> getUpdates() {
       return updates;
     }


@@ -371,6 +382,15 @@ public class ConflictTracker extends ListenerAdapter {
 
     System.out.println("}");
   }
 
     System.out.println("}");
   }

+
+  @Override
+  public void choiceGeneratorAdvanced(VM vm, ChoiceGenerator<?> currentCG) {
+
+    if (currentCG instanceof IntChoiceFromSet) {
+      IntChoiceFromSet icsCG = (IntChoiceFromSet) currentCG;
+      currentEvent = icsCG.getNextChoice();
+    }
+  }

   
   @Override
   public void stateAdvanced(Search search) {
   
   @Override
   public void stateAdvanced(Search search) {


@@ -384,7 +404,7 @@ public class ConflictTracker extends ListenerAdapter {
     Node currentNode = getNode(id);
 
     // Create an edge based on the current transition
     Node currentNode = getNode(id);
 
     // Create an edge based on the current transition

-    Edge newEdge = createEdge(parentNode, currentNode, transition);
+    Edge newEdge = createEdge(parentNode, currentNode, transition, currentEvent);

 
     // Reset the temporary variables and flags
     currUpdates.clear();
 
     // Reset the temporary variables and flags
     currUpdates.clear();

diff --git a/src/main/gov/nasa/jpf/listener/StateReducer.java b/src/main/gov/nasa/jpf/listener/StateReducer.java
index 71eaf325f2022190bd8da2d1e3f4aa5ba612107e..ec2fe98df4e7a8d043ce554241e283b000fa47f9 100644 (file)
--- a/src/main/gov/nasa/jpf/listener/StateReducer.java
+++ b/src/main/gov/nasa/jpf/listener/StateReducer.java
@@ -52,10 +52,10 @@ public class StateReducer extends ListenerAdapter {
   private boolean debugMode;
   private boolean stateReductionMode;
   private final PrintWriter out;
   private boolean debugMode;
   private boolean stateReductionMode;
   private final PrintWriter out;

-  volatile private String detail;
-  volatile private int depth;
-  volatile private int id;
-  Transition transition;
+  private String detail;
+  private int depth;
+  private int id;
+  private Transition transition;

 
   // State reduction fields
   private Integer[] choices;
 
   // State reduction fields
   private Integer[] choices;


@@ -75,8 +75,6 @@ public class StateReducer extends ListenerAdapter {
   // Stores explored backtrack lists in the form of HashSet of Strings
   private HashSet<String> backtrackSet;
   private HashMap<Integer, HashSet<Integer>> conflictPairMap;
   // Stores explored backtrack lists in the form of HashSet of Strings
   private HashSet<String> backtrackSet;
   private HashMap<Integer, HashSet<Integer>> conflictPairMap;

-  // Map choicelist with start index
-  //  private HashMap<Integer[],Integer> choiceListStartIndexMap;

 
   // Map that represents graph G
   // (i.e., visible operation dependency graph (VOD Graph)
 
   // Map that represents graph G
   // (i.e., visible operation dependency graph (VOD Graph)


@@ -86,15 +84,17 @@ public class StateReducer extends ListenerAdapter {
   // VOD graph is updated when the state has not yet been seen
   // Current state
   private int stateId;
   // VOD graph is updated when the state has not yet been seen
   // Current state
   private int stateId;

-  // Previous state
-  private int prevStateId;

   // Previous choice number
   private int prevChoiceValue;
   // Previous choice number
   private int prevChoiceValue;

-  // Counter for a visited state
-  private HashMap<Integer, Integer> visitedStateCounter;

   // HashSet that stores references to unused CGs
   private HashSet<IntChoiceFromSet> unusedCG;
 
   // HashSet that stores references to unused CGs
   private HashSet<IntChoiceFromSet> unusedCG;
 

+  // Reference to the state graph in the ConflictTracker class
+  private HashMap<Integer, ConflictTracker.Node> stateGraph;
+  // Visited states in the previous and current executions/traces for terminating condition
+  private HashSet<Integer> prevVisitedStates;
+  private HashSet<Integer> currVisitedStates;
+

   public StateReducer(Config config, JPF jpf) {
     debugMode = config.getBoolean("debug_state_transition", false);
     stateReductionMode = config.getBoolean("activate_state_reduction", true);
   public StateReducer(Config config, JPF jpf) {
     debugMode = config.getBoolean("debug_state_transition", false);
     stateReductionMode = config.getBoolean("activate_state_reduction", true);


@@ -110,7 +110,6 @@ public class StateReducer extends ListenerAdapter {
     isBooleanCGFlipped = false;
     vodGraphMap = new HashMap<>();
     stateId = -1;
     isBooleanCGFlipped = false;
     vodGraphMap = new HashMap<>();
     stateId = -1;

-    prevStateId = -1;

     prevChoiceValue = -1;
     cgMap = new HashMap<>();
     readWriteFieldsMap = new HashMap<>();
     prevChoiceValue = -1;
     cgMap = new HashMap<>();
     readWriteFieldsMap = new HashMap<>();


@@ -118,7 +117,10 @@ public class StateReducer extends ListenerAdapter {
     backtrackSet = new HashSet<>();
     conflictPairMap = new HashMap<>();
     unusedCG = new HashSet<>();
     backtrackSet = new HashSet<>();
     conflictPairMap = new HashMap<>();
     unusedCG = new HashSet<>();

-    visitedStateCounter = new HashMap<>();
+    // TODO: We are assuming that the StateReducer is always used together with the ConflictTracker
+    stateGraph = ConflictTracker.nodes;
+    prevVisitedStates = new HashSet<>();
+    currVisitedStates = new HashSet<>();

     initializeStateReduction();
   }
 
     initializeStateReduction();
   }
 


@@ -241,24 +243,50 @@ public class StateReducer extends ListenerAdapter {
     unusedCG.clear();
   }
 
     unusedCG.clear();
   }
 

-  private void incrementVisitedStateCounter(int stId) {
-    // Increment counter for this state ID
-    if (visitedStateCounter.containsKey(stId)) {
-      int stateCount = visitedStateCounter.get(stId);
-      visitedStateCounter.put(stId, stateCount + 1);
+  // Detect cycles in the current execution/trace
+  // We terminate the execution iff:
+  // (1) the state has been visited in the current execution
+  // (2) the state has one or more cycles that involve all the events
+  private boolean containsCyclesWithAllEvents(int stId) {
+
+    HashSet<Integer> visitedEvents = new HashSet<>();
+    boolean containsCyclesWithAllEvts = false;
+    ConflictTracker.Node currNode = stateGraph.get(stId);
+    for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
+      dfsFindCycles(edge.getDst(), visitedEvents, new HashSet<>());
+    }
+    if (checkIfAllEventsInvolved(visitedEvents)) {
+      containsCyclesWithAllEvts = true;
+    }
+
+    return containsCyclesWithAllEvts;
+  }
+
+  private void dfsFindCycles(ConflictTracker.Node currNode, HashSet<Integer> visitedEvents,
+                             HashSet<Integer> visitingEvents) {
+
+    // Stop when there is a cycle and record all the events
+    if (visitingEvents.contains(currNode.getId())) {
+      visitedEvents.addAll(visitingEvents);

     } else {
     } else {

-      // If we have seen it then the frequency is 2
-      visitedStateCounter.put(stId, 2);
+      for(ConflictTracker.Edge edge : currNode.getOutEdges()) {
+        visitingEvents.add(edge.getEventNumber());
+        dfsFindCycles(edge.getDst(), visitedEvents, visitingEvents);
+        visitingEvents.remove(edge.getEventNumber());
+      }

     }
   }
 
     }
   }
 

-  private boolean isVisitedMultipleTimes(int stId) {
-    // Return true if the state has been visited more than once
-    if (visitedStateCounter.containsKey(stId) &&
-            visitedStateCounter.get(stId) > 1) {
-      return true;
+  private boolean checkIfAllEventsInvolved(HashSet<Integer> visitedEvents) {
+
+    // Check if this set contains all the event choices
+    // If not then this is not the terminating condition
+    for(int i=0; i<=choiceUpperBound; i++) {
+      if (!visitedEvents.contains(i)) {
+        return false;
+      }

     }
     }

-    return false;
+    return true;

   }
 
   @Override
   }
 
   @Override


@@ -286,11 +314,9 @@ public class StateReducer extends ListenerAdapter {
           readWriteFieldsMap.clear();
           choiceCounter = 0;
         }
           readWriteFieldsMap.clear();
           choiceCounter = 0;
         }

-        if (!vm.isNewState()) {
-          incrementVisitedStateCounter(stateId);
-        }
-        // Check if we have seen this state and it's not looping back to itself
-        if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
+        // Check if we have seen this state or this state contains cycles that involve all events
+//        if (prevStateId != -1 && stateId != prevStateId && isVisitedMultipleTimes(stateId)) {
+        if (prevVisitedStates.contains(stateId) || containsCyclesWithAllEvents(stateId)) {

           // Traverse the sub-graphs
           if (isResetAfterAnalysis) {
             // Advance choice counter for sub-graphs
           // Traverse the sub-graphs
           if (isResetAfterAnalysis) {
             // Advance choice counter for sub-graphs


@@ -316,12 +342,14 @@ public class StateReducer extends ListenerAdapter {
             resetAllCGs();
             isResetAfterAnalysis = true;
           }
             resetAllCGs();
             isResetAfterAnalysis = true;
           }

+          // Save all the visited states
+          prevVisitedStates.addAll(currVisitedStates);

         }
       }
     }
   }
 
         }
       }
     }
   }
 

-  public void updateVODGraph(int prevChoice, int currChoice) {
+  private void updateVODGraph(int prevChoice, int currChoice) {

 
     HashSet<Integer> choiceSet;
     if (vodGraphMap.containsKey(prevChoice)) {
 
     HashSet<Integer> choiceSet;
     if (vodGraphMap.containsKey(prevChoice)) {


@@ -335,13 +363,6 @@ public class StateReducer extends ListenerAdapter {
     choiceSet.add(currChoice);
   }
 
     choiceSet.add(currChoice);
   }
 

-  private void updateStateId(Search search) {
-    // Saving the previous state
-    prevStateId = stateId;
-    // Line 19 in the paper page 11 (see the heading note above)
-    stateId = search.getStateId();
-  }
-

   @Override
   public void stateAdvanced(Search search) {
     if (debugMode) {
   @Override
   public void stateAdvanced(Search search) {
     if (debugMode) {


@@ -368,15 +389,11 @@ public class StateReducer extends ListenerAdapter {
       currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice;
       if (currChoice < 0 || choices[currChoice] == -1 ||
               prevChoiceValue == choices[currChoice]) {
       currChoice = currChoice >= 0 ? currChoice % (choices.length -1) : currChoice;
       if (currChoice < 0 || choices[currChoice] == -1 ||
               prevChoiceValue == choices[currChoice]) {

-//              || currChoice > choices.length - 1 || choices[currChoice] == -1 ||
-//              prevChoiceValue == choices[currChoice]) {
-//        // When current choice is 0, previous choice could be -1
+        // When current choice is 0, previous choice could be -1

 //        updateVODGraph(prevChoiceValue, choices[currChoice]);
 //        updateVODGraph(prevChoiceValue, choices[currChoice]);

-//        // Current choice becomes previous choice in the next iteration
-//        prevChoiceValue = choices[currChoice];

         // Update the state ID variables
         // Update the state ID variables

-        updateStateId(search);
-        // Handle all corner cases (e.g., out of bound values)
+        stateId = search.getStateId();
+        currVisitedStates.add(stateId);

         return;
       }
       // When current choice is 0, previous choice could be -1
         return;
       }
       // When current choice is 0, previous choice could be -1


@@ -384,7 +401,8 @@ public class StateReducer extends ListenerAdapter {
       // Current choice becomes previous choice in the next iteration
       prevChoiceValue = choices[currChoice];
       // Update the state ID variables
       // Current choice becomes previous choice in the next iteration
       prevChoiceValue = choices[currChoice];
       // Update the state ID variables

-      updateStateId(search);
+      stateId = search.getStateId();
+      currVisitedStates.add(stateId);

     }
   }
 
     }
   }
 


@@ -397,8 +415,6 @@ public class StateReducer extends ListenerAdapter {
       detail = null;
 
       // Update the state variables
       detail = null;
 
       // Update the state variables

-      // Saving the previous state
-      prevStateId = stateId;

       // Line 19 in the paper page 11 (see the heading note above)
       stateId = search.getStateId();
 
       // Line 19 in the paper page 11 (see the heading note above)
       stateId = search.getStateId();