cyclegraph: change Promise nodes map

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.

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 44f5a28bc15b69cc3289a4906b298341845ae324..eeec66520c34d19d1f3d63539ce0c01a7109814b 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -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);
 

diff --git a/cyclegraph.h b/cyclegraph.h
index bb2ab2d87b4370065ff64fa9dfcac45e86f2ce39..1af54c77818bde954d784eb925cc56adc2013fd4 100644 (file)
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -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;

diff --git a/model.cc b/model.cc
index 94bc58b6c5a010254ac34a509afe1a135fa1247d..446137922bbce9b56aa37c092db174a0dc3df71f 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);