From c0667b74acfa088e95ae9ef01eaf7e5d965c096c Mon Sep 17 00:00:00 2001 From: amiraj Date: Tue, 3 Dec 2019 14:31:21 -0800 Subject: [PATCH 1/1] Change in the Conflict Tracker analysis --- .../nasa/jpf/listener/ConflictTracker.java | 274 ++++++++++++------ 1 file changed, 183 insertions(+), 91 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index a0ecc4b..193d2f0 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -37,7 +37,6 @@ import java.util.*; **/ public class ConflictTracker extends ListenerAdapter { - private final PrintWriter out; private final HashSet conflictSet = new HashSet(); // Variables we want to track private final HashSet appSet = new HashSet(); // Apps we want to find their conflicts @@ -90,22 +89,56 @@ public class ConflictTracker extends ListenerAdapter { boolean propagateTheChange(Node currentNode) { HashSet changed = new HashSet(currentNode.getSuccessors()); + HashMap> parentQueueMap = new HashMap>(); + HashSet parents = new HashSet(); + 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> 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(); + 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); + } } } @@ -115,110 +148,142 @@ public class ConflictTracker extends ListenerAdapter { String createErrorMessage(NameValuePair pair, HashMap valueMap, HashMap 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 setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap().get(currentTransition); HashMap valueMap = new HashMap(); // HashMap from varName to value - HashMap writerMap = new HashMap(); // 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 writerMap = new HashMap(); // 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 setSet = currentNode.getSetSetMap().get(parentNode); + boolean updateTheOutSet(Node parentNode, Node currentNode) { + HashMap> setSet = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap(); HashSet updatedVarNames = new HashSet(); - HashMap writerLastValue = new HashMap(); - + Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); + HashMap lastWriter = currentEdge.getLastWriter(); + HashMap 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 value = (ArrayList)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 value = (ArrayList)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 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 predecessors = new HashSet(); HashSet successors = new HashSet(); HashSet outSet = new HashSet(); - ArrayList setSet = new ArrayList(); - HashMap> setSetMap = new HashMap>(); + HashMap outgoingEdges = new HashMap(); Node(Integer id) { this.id = id; } - void addPredecessor(Node node) { - predecessors.add(node); - } - - void addSuccessor(Node node) { - successors.add(node); - } - Integer getId() { return id; } @@ -235,13 +300,41 @@ public class ConflictTracker extends ListenerAdapter { return outSet; } - ArrayList getSetSet() { - return setSet; - } + HashMap getOutgoingEdges() { + return outgoingEdges; + } + } + + static class Edge { + Node source, destination; + HashMap lastWriter = new HashMap(); + HashMap lastValue = new HashMap(); + HashMap> setSetMap = new HashMap>(); + + Edge(Node source, Node destination) { + this.source = source; + this.destination = destination; + } + + Node getSource() { + return source; + } - HashMap> getSetSetMap() { + Node getDestination() { + return destination; + } + + HashMap> getSetSetMap() { return setSetMap; } + + HashMap getLastWriter() { + return lastWriter; + } + + HashMap getLastValue() { + return lastValue; + } } static class NameValuePair { @@ -331,6 +424,7 @@ 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"; @@ -341,17 +435,15 @@ public class ConflictTracker extends ListenerAdapter { Node currentNode = nodes.get(id); - if ((currentNode.getSetSetMap().get(parentNode) == null) || manual) - currentNode.getSetSetMap().put(parentNode, new ArrayList()); + // 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(); 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"; @@ -369,15 +461,15 @@ 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); + 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) -- 2.34.1