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=3ec1eea1b9b9d466a0d9db55e5d001e97dbb3de4;hp=b28d65bf52a2dd377088091b1bda937f91ec7773;hb=4dc7b430e4ec5e2cdba1c837b1c4960a5875cd6a;hpb=6a0130156602669e2f61bc2ebe4dd6918b2f21b3 diff --git a/src/main/gov/nasa/jpf/listener/ConflictTracker.java b/src/main/gov/nasa/jpf/listener/ConflictTracker.java index b28d65b..3ec1eea 100644 --- a/src/main/gov/nasa/jpf/listener/ConflictTracker.java +++ b/src/main/gov/nasa/jpf/listener/ConflictTracker.java @@ -42,21 +42,20 @@ public class ConflictTracker extends ListenerAdapter { private final HashSet appSet = new HashSet(); // Apps we want to find their conflicts private final HashSet manualSet = new HashSet(); // Writer classes with manual inputs to detect direct-direct(No Conflict) interactions private final HashMap nodes = new HashMap(); // Nodes of a graph - private ArrayList tempSetSet = new ArrayList(); + private HashSet transitions = new HashSet(); + private ArrayList currUpdates = new ArrayList(); private long timeout; private long startTime; private Node parentNode = new Node(-2); private String operation; private String detail; - private String errorMessage; private int depth; private int id; - private boolean conflictFound = false; private boolean manual = 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); @@ -87,329 +86,243 @@ public class ConflictTracker extends ListenerAdapter { startTime = System.currentTimeMillis(); } - 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 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> 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(); - 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); - } - } - } + void propagateChange(Edge newEdge) { + HashSet changed = new HashSet(); - return false; - } + // Add the current node to the changed set + changed.add(newEdge); - 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!"; - System.out.println(message); - return message; - } + while(!changed.isEmpty()) { + // Get the first element of the changed set and remove it + Edge edgeToProcess = changed.iterator().next(); + changed.remove(edgeToProcess); - 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 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); - } - } - - // 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; + //If propagating change on edge causes change, enqueue all the target node's out edges + if (propagateEdge(edgeToProcess)) { + Node dst = edgeToProcess.getDst(); + for (Edge e : dst.getOutEdges()) { + changed.add(e); + } + } + } } - boolean updateTheOutSet(Node parentNode, Node currentNode) { - HashMap> setSets = parentNode.getOutgoingEdges().get(currentNode).getSetSetMap(); - HashSet updatedVarNames = new HashSet(); - Edge currentEdge = parentNode.getOutgoingEdges().get(currentNode); - HashMap lastWriter = currentEdge.getLastWriter(); - HashMap lastValue = currentEdge.getLastValue(); - HashMap outSetVarMap = new HashMap(); - boolean isChanged = false; - - for (Map.Entry mapElement : setSets.entrySet()) { - ArrayList setSet = (ArrayList)mapElement.getValue(); - - for (int i = 0;i < setSet.size();i++) { - updatedVarNames.add(setSet.get(i).getVarName()); - } - } + boolean propagateEdge(Edge e) { + HashMap> srcUpdates = e.getSrc().getLastUpdates(); + HashMap> dstUpdates = e.getDst().getLastUpdates(); + ArrayList edgeUpdates = e.getUpdates(); + HashMap lastupdate = new HashMap(); + boolean changed = false; + + //Go through each update on the current transition + for(int i=0; i confupdates = null; + + //See if we have already updated this device attribute + if (lastupdate.containsKey(io)) { + confupdates = new HashSet(); + confupdates.add(lastupdate.get(io)); + } else if (srcUpdates.containsKey(io)){ + confupdates = srcUpdates.get(io); + } + //Check for conflict with the appropriate update set if we are not a manual transition + if (confupdates != null && !u.isManual()) { + for(Update u2: confupdates) { + if (conflicts(u, u2)) { + throw new RuntimeException(createErrorMessage(u, u2)); + } + } + } + lastupdate.put(io, u); + } + for(IndexObject io: srcUpdates.keySet()) { + //Only propagate src changes if the transition doesn't update the device attribute + if (!lastupdate.containsKey(io)) { + //Make sure destination has hashset in map + if (!dstUpdates.containsKey(io)) + dstUpdates.put(io, new HashSet()); + + changed |= dstUpdates.get(io).addAll(srcUpdates.get(io)); + } + } + for(IndexObject io: lastupdate.keySet()) { + //Make sure destination has hashset in map + if (!dstUpdates.containsKey(io)) + dstUpdates.put(io, new HashSet()); + + changed |= dstUpdates.get(io).add(lastupdate.get(io)); + } + return changed; + } - for (NameValuePair i : parentNode.getOutSet()) { - outSetVarMap.put(i.getVarName(), i.getAppNum()); - if (!updatedVarNames.contains(i.getVarName())) - isChanged |= currentNode.getOutSet().add(i); - } + //Method to check for conflicts between two updates + //Have conflict if same device, same attribute, different app, different vaalue + boolean conflicts(Update u, Update u2) { + return (!u.getApp().equals(u2.getApp())) && + u.getDeviceId().equals(u2.getDeviceId()) && + u.getAttribute().equals(u2.getAttribute()) && + (!u.getValue().equals(u2.getValue())); + } + + String createErrorMessage(Update u, Update u2) { + String message = "Conflict found between the two apps. App"+u.getApp()+ + " has written the value: "+u.getValue()+ + " to the attribute: "+u.getAttribute()+" while App" + +u2.getApp()+" is writing the value: " + +u2.getValue()+" to the same variable!"; + System.out.println(message); + return message; + } + Edge createEdge(Node parent, Node current, Transition transition) { + //Check if this transition is explored. If so, just skip everything + if (transitions.contains(transition)) + return null; - for (Map.Entry mapElement : setSets.entrySet()) { - ArrayList setSet = (ArrayList)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)); - } - } - } + //Create edge + Edge e = new Edge(parent, current, transition, currUpdates); + parent.addOutEdge(e); - return isChanged; + //Mark transition as explored + transitions.add(transition); + return e; } - 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); - } + static class Node { + Integer id; + Vector outEdges = new Vector(); + HashMap> lastUpdates = new HashMap>(); + + Node(Integer id) { + this.id = id; + } - // 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()); - } - } + Integer getId() { + return id; + } - + Vector getOutEdges() { + return outEdges; + } - static class Node { - Integer id; - HashSet predecessors = new HashSet(); - HashSet successors = new HashSet(); - HashSet outSet = new HashSet(); - HashMap outgoingEdges = new HashMap(); - - Node(Integer id) { - this.id = id; - } - - Integer getId() { - return id; - } - - HashSet getPredecessors() { - return predecessors; - } - - HashSet getSuccessors() { - return successors; - } - - HashSet getOutSet() { - return outSet; - } - - HashMap getOutgoingEdges() { - return outgoingEdges; - } + void addOutEdge(Edge e) { + outEdges.add(e); + } + + HashMap> getLastUpdates() { + return lastUpdates; + } } + //Each Edge corresponds to a transition 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; - } - - Node getDestination() { - return destination; - } - - HashMap> getSetSetMap() { - return setSetMap; - } - - HashMap getLastWriter() { - return lastWriter; - } - - HashMap getLastValue() { - return lastValue; - } + Node source, destination; + Transition transition; + ArrayList updates = new ArrayList(); + + Edge(Node src, Node dst, Transition t, ArrayList _updates) { + this.source = src; + this.destination = dst; + this.transition = t; + this.updates.addAll(_updates); + } + + Node getSrc() { + return source; + } + + Node getDst() { + return destination; + } + + Transition getTransition() { + return transition; + } + + ArrayList getUpdates() { + return updates; + } } - static class NameValuePair { - Integer appNum; - String value; - String varName; - boolean isManual; - - NameValuePair(Integer appNum, String value, String varName, boolean isManual) { - this.appNum = appNum; - this.value = value; - this.varName = varName; - this.isManual = isManual; - } - - void setAppNum(Integer appNum) { - this.appNum = appNum; - } - - void setValue(String value) { - this.value = value; - } - - void setVarName(String varName) { - this.varName = varName; - } - - void setIsManual(String varName) { - this.isManual = isManual; - } - - Integer getAppNum() { - return appNum; - } - - String getValue() { - return value; - } - - String getVarName() { - return varName; - } - - boolean getIsManual() { - return isManual; - } - - @Override - public boolean equals(Object o) { - if (o instanceof NameValuePair) { - NameValuePair other = (NameValuePair) o; - if (varName.equals(other.getVarName())) - return appNum.equals(other.getAppNum()); - } - return false; - } + static class Update { + String appName; + String deviceId; + String attribute; + String value; + boolean ismanual; + + Update(String _appName, String _deviceId, String _attribute, String _value, boolean _ismanual) { + this.appName = _appName; + this.deviceId = _deviceId; + this.attribute = _attribute; + this.value = _value; + this.ismanual = _ismanual; + } + + boolean isManual() { + return ismanual; + } + + String getApp() { + return appName; + } + + String getDeviceId() { + return deviceId; + } + + String getAttribute() { + return attribute; + } + + String getValue() { + return value; + } + + //Gets an index object for indexing updates by just device and attribute + IndexObject getIndex() { + return new IndexObject(this); + } + + public boolean equals(Object o) { + if (!(o instanceof Update)) + return false; + Update u=(Update)o; + return (getDeviceId().equals(u.getDeviceId()) && + getAttribute().equals(u.getAttribute()) && + getApp().equals(u.getApp()) && + getValue().equals(u.getValue())); + } - @Override - public int hashCode() { - return appNum.hashCode() * 31 + varName.hashCode(); - } + public int hashCode() { + return (getDeviceId().hashCode() << 3) ^ + (getAttribute().hashCode() << 2) ^ + (getApp().hashCode() << 1) ^ + getValue().hashCode(); + } } + static class IndexObject { + Update u; + IndexObject(Update _u) { + this.u = _u; + } + + public boolean equals(Object o) { + if (!(o instanceof IndexObject)) + return false; + IndexObject io=(IndexObject)o; + return (u.getDeviceId().equals(io.u.getDeviceId()) && + u.getAttribute().equals(io.u.getAttribute())); + } + public int hashCode() { + return (u.getDeviceId().hashCode() << 1) ^ u.getAttribute().hashCode(); + } + } + @Override public void stateRestored(Search search) { id = search.getStateId(); @@ -420,18 +333,19 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is restored to state with id: "+id+", depth: "+depth); // Update the parent node - if (nodes.containsKey(id)) { - parentNode = nodes.get(id); - } else { - parentNode = new Node(id); - } + parentNode = getNode(id); } @Override public void searchStarted(Search search) { out.println("----------------------------------- search started"); } - + + private Node getNode(Integer id) { + if (!nodes.containsKey(id)) + nodes.put(id, new Node(id)); + return nodes.get(id); + } @Override public void stateAdvanced(Search search) { @@ -442,20 +356,18 @@ public class ConflictTracker extends ListenerAdapter { operation = "forward"; // Add the node to the list of nodes - if (nodes.get(id) == null) - nodes.put(id, new Node(id)); + Node currentNode = getNode(id); - Node currentNode = nodes.get(id); - - // Update the edge based on the current transition - updateTheEdge(currentNode, transition); + // Create an edge based on the current transition + Edge newEdge = createEdge(parentNode, currentNode, transition); // Reset the temporary variables and flags - tempSetSet = new ArrayList(); + currUpdates.clear(); manual = false; - // Check for the conflict in this transition - conflictFound = checkForConflict(parentNode, currentNode, transition); + // If we have a new Edge, check for conflicts + if (newEdge != null) + propagateChange(newEdge); if (search.isNewState()) { detail = "new"; @@ -470,36 +382,8 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is forwarded to state with id: "+id+", depth: "+depth+" which is "+detail+" state: "+"% "+theEnd); - // 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.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.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) { - for (Node node : currentNode.getSuccessors()) { - HashMap> 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); - } else { - parentNode = new Node(id); - } + parentNode = currentNode; } @Override @@ -512,11 +396,7 @@ public class ConflictTracker extends ListenerAdapter { out.println("The state is backtracked to state with id: "+id+", depth: "+depth); // Update the parent node - if (nodes.containsKey(id)) { - parentNode = nodes.get(id); - } else { - parentNode = new Node(id); - } + parentNode = getNode(id); } @Override @@ -658,13 +538,9 @@ public class ConflictTracker extends ListenerAdapter { return null; } - private void writeWriterAndValue(String writer, String value, String var) { - // Update the temporary Set set. - NameValuePair temp = new NameValuePair(1, value, var, manual); - if (writer.equals("App2")) - temp = new NameValuePair(2, value, var, manual); - - tempSetSet.add(temp); + private void writeWriterAndValue(String writer, String attribute, String value) { + Update u = new Update(writer, "DEVICE", attribute, value, manual); + currUpdates.add(u); } @Override @@ -678,47 +554,40 @@ public class ConflictTracker extends ListenerAdapter { } } - if (conflictFound) { - StringBuilder sb = new StringBuilder(); - sb.append(errorMessage); - Instruction nextIns = ti.createAndThrowException("java.lang.RuntimeException", sb.toString()); - ti.setNextPC(nextIns); + if (conflictSet.contains(LOCATION_VAR)) { + MethodInfo mi = executedInsn.getMethodInfo(); + // Find the last load before return and get the value here + if (mi.getName().equals(SET_LOCATION_METHOD) && + executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) { + byte type = getType(ti, executedInsn); + String value = getValue(ti, executedInsn, type); + + // Extract the writer app name + ClassInfo ci = mi.getClassInfo(); + String writer = ci.getName(); + + // Update the temporary Set set. + writeWriterAndValue(writer, LOCATION_VAR, value); + } } else { - if (conflictSet.contains(LOCATION_VAR)) { - MethodInfo mi = executedInsn.getMethodInfo(); - // Find the last load before return and get the value here - if (mi.getName().equals(SET_LOCATION_METHOD) && - executedInsn instanceof ALOAD && nextInsn instanceof ARETURN) { - byte type = getType(ti, executedInsn); - String value = getValue(ti, executedInsn, type); - - // Extract the writer app name - ClassInfo ci = mi.getClassInfo(); - String writer = ci.getName(); - - // Update the temporary Set set. - writeWriterAndValue(writer, value, LOCATION_VAR); - } - } else { - if (executedInsn instanceof WriteInstruction) { - String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName(); - - for (String var : conflictSet) { - if (varId.contains(var)) { - // Get variable info - byte type = getType(ti, executedInsn); - String value = getValue(ti, executedInsn, type); - String writer = getWriter(ti.getStack(), appSet); - // Just return if the writer is not one of the listed apps in the .jpf file - if (writer == null) - return; - - if (getWriter(ti.getStack(), manualSet) != null) - manual = true; - - // Update the temporary Set set. - writeWriterAndValue(writer, value, var); - } + if (executedInsn instanceof WriteInstruction) { + String varId = ((WriteInstruction) executedInsn).getFieldInfo().getFullName(); + + for (String var : conflictSet) { + if (varId.contains(var)) { + // Get variable info + byte type = getType(ti, executedInsn); + String value = getValue(ti, executedInsn, type); + String writer = getWriter(ti.getStack(), appSet); + // Just return if the writer is not one of the listed apps in the .jpf file + if (writer == null) + return; + + if (getWriter(ti.getStack(), manualSet) != null) + manual = true; + + // Update the current updates + writeWriterAndValue(writer, var, value); } } }