cyclegraph: change Promise nodes map
authorBrian Norris <banorris@uci.edu>
Tue, 26 Feb 2013 23:59:00 +0000 (15:59 -0800)
committerBrian Norris <banorris@uci.edu>
Wed, 27 Feb 2013 00:08:26 +0000 (16:08 -0800)
Map from Promises to Nodes, not ModelAction (readers) to Nodes. This
will make it cleaner when more than one reader maps to the same promise
Node.

cyclegraph.cc
cyclegraph.h
model.cc

index 44f5a28..eeec665 100644 (file)
@@ -38,8 +38,7 @@ void CycleGraph::putNode(const ModelAction *act, CycleNode *node)
  */
 void CycleGraph::putNode(const Promise *promise, CycleNode *node)
 {
-       const ModelAction *reader = promise->get_action();
-       readerToPromiseNode.put(reader, node);
+       promiseToNode.put(promise, node);
 #if SUPPORT_MOD_ORDER_DUMP
        nodeList.push_back(node);
 #endif
@@ -51,8 +50,7 @@ void CycleGraph::putNode(const Promise *promise, CycleNode *node)
  */
 void CycleGraph::erasePromiseNode(const Promise *promise)
 {
-       const ModelAction *reader = promise->get_action();
-       readerToPromiseNode.put(reader, NULL);
+       promiseToNode.put(promise, NULL);
 #if SUPPORT_MOD_ORDER_DUMP
        /* Remove the promise node from nodeList */
        CycleNode *node = getNode_noCreate(promise);
@@ -73,7 +71,7 @@ CycleNode * CycleGraph::getNode_noCreate(const ModelAction *act) const
 /** @return The corresponding CycleNode, if exists; otherwise NULL */
 CycleNode * CycleGraph::getNode_noCreate(const Promise *promise) const
 {
-       return readerToPromiseNode.get(promise->get_action());
+       return promiseToNode.get(promise);
 }
 
 /**
@@ -116,10 +114,10 @@ CycleNode * CycleGraph::getNode(const Promise *promise)
 /**
  * @return false if the resolution results in a cycle; true otherwise
  */
-bool CycleGraph::resolvePromise(ModelAction *reader, ModelAction *writer,
+bool CycleGraph::resolvePromise(const Promise *promise, ModelAction *writer,
                promise_list_t *mustResolve)
 {
-       CycleNode *promise_node = readerToPromiseNode.get(reader);
+       CycleNode *promise_node = promiseToNode.get(promise);
        CycleNode *w_node = actionToNode.get(writer);
        ASSERT(promise_node);
 
index bb2ab2d..1af54c7 100644 (file)
@@ -47,7 +47,7 @@ class CycleGraph {
        void dumpGraphToFile(const char *filename) const;
 #endif
 
-       bool resolvePromise(ModelAction *reader, ModelAction *writer,
+       bool resolvePromise(const Promise *promise, ModelAction *writer,
                        promise_list_t *mustResolve);
 
        SNAPSHOTALLOC
@@ -67,9 +67,8 @@ class CycleGraph {
 
        /** @brief A table for mapping ModelActions to CycleNodes */
        HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> actionToNode;
-       /** @brief A table for mapping reader ModelActions to Promise
-        *  CycleNodes */
-       HashTable<const ModelAction *, CycleNode *, uintptr_t, 4> readerToPromiseNode;
+       /** @brief A table for mapping Promises to CycleNodes */
+       HashTable<const Promise *, CycleNode *, uintptr_t, 4> promiseToNode;
 
 #if SUPPORT_MOD_ORDER_DUMP
        std::vector<CycleNode *> nodeList;
index 94bc58b..4461379 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2447,7 +2447,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
                        read_from(read, write);
                        //Make sure the promise's value matches the write's value
                        ASSERT(promise->is_compatible(write));
-                       mo_graph->resolvePromise(read, write, &mustResolve);
+                       mo_graph->resolvePromise(promise, write, &mustResolve);
 
                        resolved.push_back(promise);
                        promises->erase(promises->begin() + promise_index);