From: Brian Norris <banorris@uci.edu>
Date: Tue, 26 Feb 2013 23:59:00 +0000 (-0800)
Subject: cyclegraph: change Promise nodes map
X-Git-Tag: oopsla2013~217
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=3510b440b186949cbc0760d369da6787f0def7ac;p=model-checker.git

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 44f5a28..eeec665 100644
--- 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 bb2ab2d..1af54c7 100644
--- 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 94bc58b..4461379 100644
--- 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);