From c35157d6103e1302e7edaed71ecf0c52450faf46 Mon Sep 17 00:00:00 2001 From: amiraj Date: Thu, 24 Oct 2019 16:16:47 -0700 Subject: [PATCH] Modifying conflict tracker --- .../nasa/jpf/listener/ConflictTracker.java | 193 +++++++++--------- 1 file changed, 102 insertions(+), 91 deletions(-) diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index 1343467..1aa50b9 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -93,104 +93,109 @@ public class ConflictTracker extends ListenerAdapter { HashSet changed = new HashSet(currentNode.getSuccessors()); 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 HashSet and remove it from the changed set + Node nodeToProcess = changed.iterator().next(); + changed.remove(nodeToProcess); + + // Update the edge + boolean isChanged = updateEdge(currentNode, nodeToProcess); + + // Check for a conflict in this transition(currentNode -> nodeToProcess) + if (checkForConflict(currentNode)) + 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); + } + } } - } - - return false; - } - - boolean setOutSet(Node currentNode) { - Integer prevSize = currentNode.getOutSet().size(); - - // Update based on setSet - for (NameValuePair i : currentNode.getSetSet()) { - if (currentNode.getOutSet().contains(i)) - currentNode.getOutSet().remove(i); - currentNode.getOutSet().add(i); - } - // 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; + return false; } - void setInSet(Node currentNode) { - for (Node i : currentNode.getPredecessors()) { - currentNode.getInSet().addAll(i.getOutSet()); - } + 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: " + +valueMap.get(pair.getVarName())+" to the same variable!"; + return message; } - boolean checkForConflict(Node currentNode) { + boolean checkForConflict(Node nodeToProcess) { HashMap valueMap = new HashMap(); // HashMap from varName to value HashMap writerMap = new HashMap(); // HashMap from varName to appNum - 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()); + // Update the valueMap and check if we have conflict in the setSet + for (NameValuePair i : nodeToProcess.getSetSet()) { + if (i.getIsManual()) // Manual input: we have no conflict + continue; // If this manual write is the last write, this is actually a break + + if (valueMap.containsKey(i.getVarName())) { + if (!valueMap.get(i.getVarName()).equals(i.getValue())) { // Check if their value is different we have a conflict + errorMessage = createErrorMessage(i, valueMap, writerMap); + return true; + } + else // We have two writers writing the same value + writerMap.put(i.getVarName(), i.getAppNum()+writerMap.get(i.getVarName())); + } else { + valueMap.put(i.getVarName(), i.getValue()); + writerMap.put(i.getVarName(), i.getAppNum()); + } } - // 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; - } - } - } + // 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; + } + } + } } return false; } - boolean updateSets(Node currentNode) { - // Set input set according to output set of pred states of current state - setInSet(currentNode); + boolean updateEdge(Node parentNode, Node currentNode) { + HashSet setSet = currentNode.getSetSetMap().get(parentNode); + HashSet updatedVarNames = new HashSet(); + HashMap lastWriter = new HashMap(); // Store the last writer of each variable + boolean isChanged = false; - // Set outSet according to inSet, and setSet of current node, check if there is a change - return setOutSet(currentNode); + for (NameValuePair i : setSet) { + updatedVarNames.add(i.getVarName()); + lastWriter.put(i.getVarName(), i.getAppNum()); + } + + for (NameValuePair i : parentNode.getOutSet()) { + if (!updatedVarNames.contains(i.getVarName())) + isChanged |= currentNode.getOutSet().add(i); + } + + for (NameValuePair i : setSet) { + if (i.getAppNum().equals(lastWriter.get(i.getVarName()))) // Add the last writer of each variable to outSet + isChanged |= currentNode.getOutSet().add(i); + } + + return isChanged; } static class Node { Integer id; HashSet predecessors = new HashSet(); HashSet successors = new HashSet(); - HashSet inSet = new HashSet(); HashSet setSet = new HashSet(); HashSet outSet = new HashSet(); + HashMap> setSetMap = new HashMap>(); + Node(Integer id) { this.id = id; @@ -205,11 +210,11 @@ public class ConflictTracker extends ListenerAdapter { } void setSetSet(HashSet setSet, boolean isManual) { - if (isManual) - this.setSet = new HashSet(); - for (NameValuePair i : setSet) { - this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual())); - } + if (isManual) + this.setSet = new HashSet(); + for (NameValuePair i : setSet) { + this.setSet.add(new NameValuePair(i.getAppNum(), i.getValue(), i.getVarName(), i.getIsManual())); + } } Integer getId() { @@ -224,10 +229,6 @@ public class ConflictTracker extends ListenerAdapter { return successors; } - HashSet getInSet() { - return inSet; - } - HashSet getSetSet() { return setSet; } @@ -235,6 +236,10 @@ public class ConflictTracker extends ListenerAdapter { HashSet getOutSet() { return outSet; } + + HashMap> getSetSetMap() { + return setSetMap; + } } static class NameValuePair { @@ -244,10 +249,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) { @@ -328,6 +333,9 @@ public class ConflictTracker extends ListenerAdapter { depth = search.getDepth(); operation = "forward"; + // Check for the conflict in this new transition + conflictFound = checkForConflict(parentNode); + // Add the node to the list of nodes nodes.put(id, new Node(id)); Node currentNode = nodes.get(id); @@ -363,11 +371,14 @@ public class ConflictTracker extends ListenerAdapter { 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); + + // Update the setSetMap of the current node + for (Node i : currentNode.getPredecessors()) { + currentNode.getSetSetMap().put(i, i.getSetSet()); + } + + // 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); // Check if the outSet of this state has changed, update all of its successors' sets if any if (isChanged) -- 2.34.1