**/
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
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
+ // Get the first element of the changed set and remove it
Node nodeToProcess = changed.iterator().next();
changed.remove(nodeToProcess);
- // Update the edge
- boolean isChanged = updateEdge(currentNode, 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;
+ }
+ }
+ }
- // Check for a conflict in this transition(currentNode -> nodeToProcess)
- if (checkForConflict(nodeToProcess))
- 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) {
- propagateTheChange(nodeToProcess);
+ 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);
+ }
}
}
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: "
+ " 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;
}
- boolean checkForConflict(Node nodeToProcess) {
+ 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
- for (int i = 0;i < nodeToProcess.getSetSet().size();i++) {
- NameValuePair nameValuePair = nodeToProcess.getSetSet().get(i);
-
- if (valueMap.containsKey(nameValuePair.getVarName())) {
- // Check if we have a same writer
- if (!writerMap.get(nameValuePair.getVarName()).equals(nameValuePair.getAppNum())) {
- // Check if we have a conflict or not
- if (!valueMap.get(nameValuePair.getVarName()).equals(nameValuePair.getValue())) {
- errorMessage = createErrorMessage(nameValuePair, valueMap, writerMap);
- return true;
- } else { // We have two writers writing the same value
- writerMap.put(nameValuePair.getVarName(), 3); // 3 represents both apps
- }
- } else {
- // Check if we have more than one value with the same writer
- if (!valueMap.get(nameValuePair.getVarName()).equals(nameValuePair.getValue())) {
- valueMap.put(nameValuePair.getVarName(), "twoValue"); // We have one writer writing more than one value in a same event
- }
- }
+ 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 {
- valueMap.put(nameValuePair.getVarName(), nameValuePair.getValue());
- writerMap.put(nameValuePair.getVarName(), nameValuePair.getAppNum());
- }
- }
-
- // Comparing the outSet to setSet
- for (NameValuePair i : nodeToProcess.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
- errorMessage = createErrorMessage(i, valueMap, writerMap);
- return true;
- }
+ // 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);
+ }
}
- return false;
+ // 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 updateEdge(Node parentNode, Node currentNode) {
- ArrayList<NameValuePair> setSet = currentNode.getSetSetMap().get(parentNode);
+ boolean updateTheOutSet(Node parentNode, Node currentNode) {
+ HashMap<Transition, ArrayList<NameValuePair>> setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap();
HashSet<String> updatedVarNames = new HashSet<String>();
- HashMap<Integer, String> writerLastValue = new HashMap<Integer, String>();
-
+ Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode);
+ HashMap<String, Integer> lastWriter = currentEdge.getLastWriter();
+ HashMap<String, String> lastValue = currentEdge.getLastValue();
boolean isChanged = false;
-
- if (setSet != null) {
- for (int i = 0;i < setSet.size();i++) {
- updatedVarNames.add(setSet.get(i).getVarName());
- writerLastValue.put(setSet.get(i).getAppNum(), setSet.get(i).getValue());
- }
- }
+
+ for (Map.Entry mapElement : setSet.entrySet()) {
+ ArrayList<NameValuePair> value = (ArrayList<NameValuePair>)mapElement.getValue();
+
+ for (int i = 0;i < value.size();i++) {
+ updatedVarNames.add(value.get(i).getVarName());
+ }
+ }
+
for (NameValuePair i : parentNode.getOutSet()) {
if (!updatedVarNames.contains(i.getVarName()))
isChanged |= currentNode.getOutSet().add(i);
}
- if (setSet != null) {
- for (int i = 0;i < setSet.size();i++) {
- if (setSet.get(i).getValue().equals(writerLastValue.get(setSet.get(i).getAppNum()))) {
- isChanged |= currentNode.getOutSet().add(setSet.get(i));
+
+ for (Map.Entry mapElement : setSet.entrySet()) {
+ ArrayList<NameValuePair> value = (ArrayList<NameValuePair>)mapElement.getValue();
+
+ for (int i = 0;i < value.size();i++) {
+ if (value.get(i).getAppNum().equals(lastWriter.get(value.get(i).getVarName()))
+ && value.get(i).getValue().equals(lastValue.get(value.get(i).getVarName()))) {
+ isChanged |= currentNode.getOutSet().add(value.get(i));
}
- }
- }
+ }
+ }
return isChanged;
}
+ 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);
+ }
+
+ // 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;
HashSet<Node> predecessors = new HashSet<Node>();
HashSet<Node> successors = new HashSet<Node>();
HashSet<NameValuePair> outSet = new HashSet<NameValuePair>();
- ArrayList<NameValuePair> setSet = new ArrayList<NameValuePair>();
- HashMap<Node, ArrayList<NameValuePair>> setSetMap = new HashMap<Node, ArrayList<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);
- }
-
Integer getId() {
return id;
}
return outSet;
}
- ArrayList<NameValuePair> getSetSet() {
- return setSet;
- }
+ HashMap<Node, Edge> getOutgoingEdges() {
+ return outgoingEdges;
+ }
+ }
+
+ 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;
+ }
- HashMap<Node, ArrayList<NameValuePair>> getSetSetMap() {
+ Node getDestination() {
+ return destination;
+ }
+
+ HashMap<Transition, ArrayList<NameValuePair>> getSetSetMap() {
return setSetMap;
}
+
+ HashMap<String, Integer> getLastWriter() {
+ return lastWriter;
+ }
+
+ HashMap<String, String> getLastValue() {
+ return lastValue;
+ }
}
static class NameValuePair {
@Override
public void stateAdvanced(Search search) {
String theEnd = null;
+ Transition transition = search.getTransition();
id = search.getStateId();
depth = search.getDepth();
operation = "forward";
Node currentNode = nodes.get(id);
- if ((currentNode.getSetSetMap().get(parentNode) == null) || manual)
- currentNode.getSetSetMap().put(parentNode, new ArrayList<NameValuePair>());
+ // Update the edge based on the current transition
+ updateTheEdge(currentNode, transition);
- // Update the setSet for the edge
- currentNode.getSetSetMap().get(parentNode).addAll(tempSetSet);
- parentNode.getSetSet().addAll(tempSetSet);
+ // Reset the temporary variables and flags
tempSetSet = new ArrayList<NameValuePair>();
manual = false;
- // Check for the conflict in this edge
- conflictFound = checkForConflict(parentNode);
+ // Check for the conflict in this transition
+ conflictFound = checkForConflict(parentNode, currentNode, transition);
if (search.isNewState()) {
detail = "new";
// 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);
+ parentNode.getSuccessors().add(currentNode);
- // Update the edge and check if the outset of the current node is changed or not to propagate the change
- boolean isChanged = updateEdge(parentNode, 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)
projects / jpf-core.git / commitdiff