X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Fmain%2Fgov%2Fnasa%2Fjpf%2Flistener%2FConflictTracker.java;h=b28d65bf52a2dd377088091b1bda937f91ec7773;hp=db478369ff5368eafb6a1f6e6e75c7af43ff6b84;hb=6a0130156602669e2f61bc2ebe4dd6918b2f21b3;hpb=6c123799fabcbe17c1f46842c846892b6cf84f62

diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
index db47836..b28d65b 100644
--- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java
+++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java
@@ -37,13 +37,12 @@ import java.util.*;
  **/
 
 public class ConflictTracker extends ListenerAdapter {
-
   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<NameValuePair> tempSetSet = new HashSet<NameValuePair>();
+  private ArrayList<NameValuePair> tempSetSet = new ArrayList<NameValuePair>();
   private long timeout;
   private long startTime;
   private Node parentNode = new Node(-2);
@@ -53,7 +52,6 @@ public class ConflictTracker extends ListenerAdapter {
   private int depth;
   private int id;
   private boolean conflictFound = false;
-  private boolean isSet = false;
   private boolean manual = false;
 
   private final String SET_LOCATION_METHOD = "setLocationMode";
@@ -91,125 +89,211 @@ public class ConflictTracker extends ListenerAdapter {
 
   boolean propagateTheChange(Node currentNode) {
 	HashSet<Node> changed = new HashSet<Node>(currentNode.getSuccessors());
+	HashMap<Node, HashSet<Node>> parentQueueMap = new HashMap<Node, HashSet<Node>>();
+	HashSet<Node> parents = new HashSet<Node>();
+	parents.add(currentNode);
+
+	for (Node node : currentNode.getSuccessors()) {
+		parentQueueMap.put(node, parents);
+	}
 
 	while(!changed.isEmpty()) {
-      // Get the first element of HashSet and remove it from the changed set
-      Node nodeToProcess = changed.iterator().next();
-      changed.remove(nodeToProcess);
-
-      // Update the sets, store the outSet to temp before its changes
-      boolean isChanged = updateSets(nodeToProcess);
-
-      // Check for a conflict
-      if (checkForConflict(nodeToProcess))
-        return true;
-
-      // Checking if the out set has changed or not(Add its successors to the change list!)
-      if (isChanged) {
-        for (Node i : nodeToProcess.getSuccessors()) {
-          if (!changed.contains(i))
-            changed.add(i);
-        }
+        	// Get the first element of the changed set and remove it
+      		Node nodeToProcess = changed.iterator().next();
+      		changed.remove(nodeToProcess);
+
+		// Update the changed parents
+		parents = parentQueueMap.get(nodeToProcess);
+		boolean isChanged = false;
+
+		for (Node node : parents) {
+			// Update the edge
+      			isChanged |= updateTheOutSet(node, nodeToProcess);
+		}
+
+      		// Check for a conflict if the outSet of nodeToProcess is changed
+      		if (isChanged) {
+			for (Node node : nodeToProcess.getSuccessors()) {
+				HashMap<Transition, ArrayList<NameValuePair>> setSets = nodeToProcess.getOutgoingEdges().get(node).getSetSetMap();
+				for (Map.Entry mapElement : setSets.entrySet()) {
+					Transition transition = (Transition)mapElement.getKey();
+					if (checkForConflict(nodeToProcess, node, transition))
+						return true;
+				}
+			}
+		}
+
+		// Update the parents list for the successors of the current node
+		parents = new HashSet<Node>();
+		parents.add(nodeToProcess);
+
+      		// Checking if the out set has changed or not(Add its successors to the change list!)
+      		if (isChanged) {
+			for (Node i : nodeToProcess.getSuccessors()) {
+          			if (!changed.contains(i))
+            				changed.add(i);
+
+				// Update the list of updated parents for the current node
+				if (parentQueueMap.containsKey(i))
+					parentQueueMap.get(i).add(nodeToProcess);
+				else
+					parentQueueMap.put(i, parents);
+        		}
+      		}
       }
-	}
 
-	return false;
+      return false;
   }
 
-  boolean setOutSet(Node currentNode) {
-	Integer prevSize = currentNode.getOutSet().size();
+  String createErrorMessage(NameValuePair pair, HashMap<String, String> valueMap, HashMap<String, Integer> writerMap) {
+	String message = "Conflict found between the two apps. App"+pair.getAppNum()+
+			 " has written the value: "+pair.getValue()+
+			 " to the variable: "+pair.getVarName()+" while App"
+			 +writerMap.get(pair.getVarName())+" is overwriting the value: "
+			 +valueMap.get(pair.getVarName())+" to the same variable!";
+	System.out.println(message);	
+	return message;
+  }
 
-	// Update based on setSet
-	for (NameValuePair i : currentNode.getSetSet()) {
-      if (currentNode.getOutSet().contains(i))
-        currentNode.getOutSet().remove(i);
-      currentNode.getOutSet().add(i);
+  boolean checkForConflict(Node parentNode, Node currentNode, Transition currentTransition) {
+	ArrayList<NameValuePair> setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap().get(currentTransition);
+	HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
+	HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); //  HashMap from varName to appNum
+
+	// Update the valueMap and writerMap + check for conflict between the elements of setSet
+	for (int i = 0;i < setSet.size();i++) {
+            NameValuePair nameValuePair = setSet.get(i);
+	    String varName = nameValuePair.getVarName();
+	    String value = nameValuePair.getValue();
+	    Integer appNum = nameValuePair.getAppNum();
+
+	    if (valueMap.containsKey(varName)) {
+		// Check if we have a same writer
+		if (!writerMap.get(varName).equals(appNum)) {
+			// Check if we have a conflict or not
+			if (!valueMap.get(varName).equals(value)) {
+				errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
+				return true;
+			} else { // We have two writers writing the same value
+				writerMap.put(varName, 3); // 3 represents both apps
+			}
+		} else {
+			// Check if we have more than one value with the same writer
+			if (!valueMap.get(varName).equals(value)) {
+				// We have one writer writing more than one value in a same event
+				valueMap.put(varName, "twoValue");
+			}
+		}
+	     } else {
+		valueMap.put(varName, value);
+		writerMap.put(varName, appNum);
+	     }
 	}
 
-	// Add all the inSet
-	currentNode.getOutSet().addAll(currentNode.getInSet());
-
-	// Check if the outSet is changed
-	if (!prevSize.equals(currentNode.getOutSet().size()))
-      return true;
-	
-	return false;
-  }
-
-  void setInSet(Node currentNode) {
-	for (Node i : currentNode.getPredecessors()) {
-      currentNode.getInSet().addAll(i.getOutSet());
-    }
+	// Check for conflict between outSet and this transition setSet
+	for (NameValuePair i : currentNode.getOutSet()) {
+	     if (valueMap.containsKey(i.getVarName())) {
+	         String value = valueMap.get(i.getVarName());
+		 Integer writer = writerMap.get(i.getVarName());
+		     if ((value != null)&&(writer != null)) {
+		         if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { 
+			     // We have different values and different writers
+			     errorMessage = createErrorMessage(i, valueMap, writerMap);
+			     return true;
+			 }
+		     }
+	     }
+       }
+
+       return false;
   }
 
-  boolean checkForConflict(Node currentNode) {
-	HashMap<String, String> valueMap = new HashMap<String, String>(); // HashMap from varName to value
-	HashMap<String, Integer> writerMap = new HashMap<String, Integer>(); // HashMap from varName to appNum
+  boolean updateTheOutSet(Node parentNode, Node currentNode) {
+	HashMap<Transition, ArrayList<NameValuePair>> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
+	HashSet<String> updatedVarNames = new HashSet<String>();
+	Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+	HashMap<String, Integer> lastWriter = currentEdge.getLastWriter();
+	HashMap<String, String> lastValue = currentEdge.getLastValue();
+	HashMap<String, Integer> outSetVarMap = new HashMap<String, Integer>();
+	boolean isChanged = false;
+
+        for (Map.Entry mapElement : setSets.entrySet()) {
+            ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
+  
+            for (int i = 0;i < setSet.size();i++) {
+			updatedVarNames.add(setSet.get(i).getVarName());
+	    }
+        }
 
-	for (NameValuePair i : currentNode.getSetSet()) {
-      if (i.getIsManual()) // Manual input: we have no conflict
-        continue;
 
-      valueMap.put(i.getVarName(), i.getValue());
-      if (writerMap.containsKey(i.getVarName()))
-        writerMap.put(i.getVarName(), i.getAppNum()+writerMap.get(i.getVarName())); // We have two writers?
-      else
-        writerMap.put(i.getVarName(), i.getAppNum());
+	for (NameValuePair i : parentNode.getOutSet()) {
+		outSetVarMap.put(i.getVarName(), i.getAppNum());
+		if (!updatedVarNames.contains(i.getVarName()))
+			isChanged |= currentNode.getOutSet().add(i);
 	}
 
-	// Comparing the inSet and setSet to find the conflict
-	for (NameValuePair i : currentNode.getInSet()) {
-      if (valueMap.containsKey(i.getVarName())) {
-        String value = valueMap.get(i.getVarName());
-        Integer writer = writerMap.get(i.getVarName());
-        if ((value != null)&&(writer != null)) {
-          if (!value.equals(i.getValue())&&!writer.equals(i.getAppNum())) { // We have different values
-            errorMessage = "Conflict found between the two apps. App"+i.getAppNum()+" has written the value: "+i.getValue()+
-                    " to the variable: "+i.getVarName()+" while App"+writerMap.get(i.getVarName())+" is overwriting the value: "
-                    +valueMap.get(i.getVarName())+" to the same variable!";
-            return true;
-          }
+
+	for (Map.Entry mapElement : setSets.entrySet()) {
+            ArrayList<NameValuePair> setSet = (ArrayList<NameValuePair>)mapElement.getValue();
+  
+            for (int i = 0;i < setSet.size();i++) {
+			String varName = setSet.get(i).getVarName();
+			Integer writer = lastWriter.get(varName);
+			String value = lastValue.get(varName);
+
+			if (setSet.get(i).getAppNum().equals(writer) 
+			    && setSet.get(i).getValue().equals(value)) {
+				if (outSetVarMap.containsKey(varName)) {
+					Integer hashCode = outSetVarMap.get(varName).hashCode() * 31 +
+							   varName.hashCode();
+					currentNode.getOutSet().remove(hashCode);
+				}
+				isChanged |= currentNode.getOutSet().add(setSet.get(i));
+			}
+	    }
         }
-      }
-	}
 
-	return false;
+	return isChanged;
   }
 
-  boolean updateSets(Node currentNode) {
-	// Set input set according to output set of pred states of current state
-    setInSet(currentNode);
+  void updateTheEdge(Node currentNode, Transition transition) {
+  	if (parentNode.getOutgoingEdges().containsKey(currentNode)) {
+		Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+		if (currentEdge.getSetSetMap().containsKey(transition)) { // Update the transition
+			if (manual)
+				currentEdge.getSetSetMap().put(transition, tempSetSet);
+			else
+				currentEdge.getSetSetMap().get(transition).addAll(tempSetSet);
+		} else { // Add a new transition
+			currentEdge.getSetSetMap().put(transition, tempSetSet);
+		}
+        } else {
+    		parentNode.getOutgoingEdges().put(currentNode, new Edge(parentNode, currentNode));
+		Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+		currentEdge.getSetSetMap().put(transition, tempSetSet);
+        }
 
-	// Set outSet according to inSet, and setSet of current node, check if there is a change
-    return setOutSet(currentNode);
+	// Update the last writer and last value for this edge for each varName
+	Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+	ArrayList<NameValuePair> setSet = currentEdge.getSetSetMap().get(transition);
+	for (int i = 0;i < setSet.size();i++) {
+		NameValuePair nameValuePair = setSet.get(i);
+		currentEdge.getLastWriter().put(nameValuePair.getVarName(), nameValuePair.getAppNum());
+		currentEdge.getLastValue().put(nameValuePair.getVarName(), nameValuePair.getValue());
+	}
   }
 
+  
+
   static class Node {
-	Integer id;
+        Integer id;
 	HashSet<Node> predecessors = new HashSet<Node>();
 	HashSet<Node> successors = new HashSet<Node>();
-	HashSet<NameValuePair> inSet = new HashSet<NameValuePair>();
-	HashSet<NameValuePair> setSet = new HashSet<NameValuePair>();
 	HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
+	HashMap<Node, Edge> outgoingEdges = new HashMap<Node, Edge>();
 
 	Node(Integer id) {
-		this.id = id;
-	}
-
-	void addPredecessor(Node node) {
-		predecessors.add(node);
-	}
-
-	void addSuccessor(Node node) {
-		successors.add(node);
-	}
-
-	void setSetSet(HashSet<NameValuePair> setSet, boolean isManual) {
-      if (isManual)
-        this.setSet = new HashSet<NameValuePair>();
-      for (NameValuePair i : setSet) {
-        this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual()));
-      }
+	  this.id = id;
 	}
 
 	Integer getId() {
@@ -224,16 +308,44 @@ public class ConflictTracker extends ListenerAdapter {
 		return successors;
 	}
 
-	HashSet<NameValuePair> getInSet() {
-		return inSet;
+	HashSet<NameValuePair> getOutSet() {
+		return outSet;
 	}
 
-	HashSet<NameValuePair> getSetSet() {
-		return setSet;
+	HashMap<Node, Edge> getOutgoingEdges() {
+		return outgoingEdges;
 	}
+  }
 
-	HashSet<NameValuePair> getOutSet() {
-		return outSet;
+  static class Edge {
+	Node source, destination;
+	HashMap<String, Integer> lastWriter = new HashMap<String, Integer>();
+	HashMap<String, String> lastValue = new HashMap<String, String>();
+	HashMap<Transition, ArrayList<NameValuePair>> setSetMap = new HashMap<Transition, ArrayList<NameValuePair>>();
+
+	Edge(Node source, Node destination) {
+		this.source = source;
+		this.destination = destination;
+	}
+
+	Node getSource() {
+		return source;
+	}
+
+	Node getDestination() {
+		return destination;
+	}
+
+	HashMap<Transition, ArrayList<NameValuePair>> getSetSetMap() {
+		return setSetMap;
+	}
+
+	HashMap<String, Integer> getLastWriter() {
+		return lastWriter;
+	}
+
+	HashMap<String, String> getLastValue() {
+		return lastValue;
 	}
   }
 
@@ -244,10 +356,10 @@ public class ConflictTracker extends ListenerAdapter {
 	boolean isManual;
 
 	NameValuePair(Integer appNum, String value, String varName, boolean isManual) {
-      this.appNum = appNum;
-      this.value = value;
-      this.varName = varName;
-      this.isManual = isManual;
+      		this.appNum = appNum;
+      		this.value = value;
+      		this.varName = varName;
+      		this.isManual = isManual;
 	}
 
 	void setAppNum(Integer appNum) {
@@ -262,7 +374,7 @@ public class ConflictTracker extends ListenerAdapter {
 		this.varName = varName;
 	}
 
-    void setIsManual(String varName) {
+        void setIsManual(String varName) {
 		this.isManual = isManual;
 	}
 
@@ -324,21 +436,26 @@ public class ConflictTracker extends ListenerAdapter {
   @Override
   public void stateAdvanced(Search search) {
     String theEnd = null;
+    Transition transition = search.getTransition();
     id = search.getStateId();
     depth = search.getDepth();
     operation = "forward";
 
-    // Add the node to the list of nodes	
-    nodes.put(id, new Node(id));
+    // Add the node to the list of nodes
+    if (nodes.get(id) == null)
+	nodes.put(id, new Node(id));
+
     Node currentNode = nodes.get(id);
 
-    // Update the setSet for this new node
-    if (isSet) {
-      currentNode.setSetSet(tempSetSet, manual);
-      tempSetSet = new HashSet<NameValuePair>(); 
-      isSet = false;
-      manual = false;
-    }
+    // Update the edge based on the current transition
+    updateTheEdge(currentNode, transition);
+
+    // Reset the temporary variables and flags
+    tempSetSet = new ArrayList<NameValuePair>();
+    manual = false;
+
+    // Check for the conflict in this transition
+    conflictFound = checkForConflict(parentNode, currentNode, transition);
 
     if (search.isNewState()) {
       detail = "new";
@@ -356,23 +473,27 @@ public class ConflictTracker extends ListenerAdapter {
     // Updating the predecessors for this node
     // Check if parent node is already in successors of the current node or not
     if (!(currentNode.getPredecessors().contains(parentNode)))
-	currentNode.addPredecessor(parentNode);
+	currentNode.getPredecessors().add(parentNode);
 
     // Update the successors for this node
     // Check if current node is already in successors of the parent node or not
     if (!(parentNode.getSuccessors().contains(currentNode)))
-        parentNode.addSuccessor(currentNode);
-
-    // Update the sets, check if the outSet is changed or not
-    boolean isChanged = updateSets(currentNode);
-   
-    // Check for a conflict
-    conflictFound = checkForConflict(currentNode);
+        parentNode.getSuccessors().add(currentNode);
 
+    // Update the outset of the current node and check if it is changed or not to propagate the change
+    boolean isChanged = updateTheOutSet(parentNode, currentNode);
+    
     // Check if the outSet of this state has changed, update all of its successors' sets if any
-    if (isChanged)
+    if (isChanged) {
+	for (Node node : currentNode.getSuccessors()) {
+		HashMap<Transition, ArrayList<NameValuePair>> setSets = currentNode.getOutgoingEdges().get(node).getSetSetMap();
+		for (Map.Entry mapElement : setSets.entrySet()) {
+			Transition currentTransition = (Transition)mapElement.getKey();
+			conflictFound = conflictFound || checkForConflict(currentNode, node, currentTransition);
+		}
+	}
 	conflictFound = conflictFound || propagateTheChange(currentNode);
-
+    }
     // Update the parent node
     if (nodes.containsKey(id)) {
 	  parentNode = nodes.get(id);
@@ -539,17 +660,15 @@ public class ConflictTracker extends ListenerAdapter {
 
   private void writeWriterAndValue(String writer, String value, String var) {
     // Update the temporary Set set.
-    if (writer.equals("App1"))
-      tempSetSet.add(new NameValuePair(1, value, var, manual));
-    else if (writer.equals("App2"))
-      tempSetSet.add(new NameValuePair(2, value, var, manual));
-    // Set isSet to true
-    isSet = true;
+    NameValuePair temp = new NameValuePair(1, value, var, manual);
+    if (writer.equals("App2"))
+    	temp = new NameValuePair(2, value, var, manual);
+    
+    tempSetSet.add(temp);
   }
 
   @Override
   public void instructionExecuted(VM vm, ThreadInfo ti, Instruction nextInsn, Instruction executedInsn) {
-    // Instantiate timeoutTimer
     if (timeout > 0) {
       if (System.currentTimeMillis() - startTime > timeout) {
         StringBuilder sbTimeOut = new StringBuilder();
@@ -583,6 +702,7 @@ public class ConflictTracker extends ListenerAdapter {
       } else {
         if (executedInsn instanceof WriteInstruction) {
           String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName();
+
           for (String var : conflictSet) {
             if (varId.contains(var)) {
               // Get variable info