projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
d7e2671
)
cyclegraph: template-ize addRMWEdge()
author
Brian Norris
<banorris@uci.edu>
Wed, 6 Feb 2013 01:13:28 +0000
(17:13 -0800)
committer
Brian Norris
<banorris@uci.edu>
Wed, 6 Feb 2013 21:45:23 +0000
(13:45 -0800)
cyclegraph.cc
patch
|
blob
|
history
cyclegraph.h
patch
|
blob
|
history
diff --git
a/cyclegraph.cc
b/cyclegraph.cc
index e834cb672b5a360077c9cb877ea164a986880acb..1ff9d70b792ad685749f8fa3c038bc7de91fdb86 100644
(file)
--- a/
cyclegraph.cc
+++ b/
cyclegraph.cc
@@
-118,12
+118,18
@@
bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node,
{
ASSERT(!w_node->is_promise());
ASSERT(p_node->is_promise());
{
ASSERT(!w_node->is_promise());
ASSERT(p_node->is_promise());
+
const Promise *promise = p_node->getPromise();
if (!promise->is_compatible(w_node->getAction())) {
hasCycles = true;
return false;
}
const Promise *promise = p_node->getPromise();
if (!promise->is_compatible(w_node->getAction())) {
hasCycles = true;
return false;
}
+ /* Transfer the RMW */
+ CycleNode *promise_rmw = p_node->getRMW();
+ if (promise_rmw && promise_rmw != w_node->getRMW() && w_node->setRMW(promise_rmw))
+ hasCycles = true;
+
/* Transfer back edges to w_node */
while (p_node->getNumBackEdges() > 0) {
CycleNode *back = p_node->removeBackEdge();
/* Transfer back edges to w_node */
while (p_node->getNumBackEdges() > 0) {
CycleNode *back = p_node->removeBackEdge();
@@
-201,15
+207,16
@@
bool CycleGraph::addNodeEdge(CycleNode *fromnode, CycleNode *tonode)
* @brief Add an edge between a write and the RMW which reads from it
*
* Handles special case of a RMW action, where the ModelAction rmw reads from
* @brief Add an edge between a write and the RMW which reads from it
*
* Handles special case of a RMW action, where the ModelAction rmw reads from
- * the ModelAction from. The key differences are:
+ * the ModelAction
/Promise
from. The key differences are:
* (1) no write can occur in between the rmw and the from action.
* (2) Only one RMW action can read from a given write.
*
* (1) no write can occur in between the rmw and the from action.
* (2) Only one RMW action can read from a given write.
*
- * @param from The edge comes from this ModelAction
+ * @param from The edge comes from this ModelAction
/Promise
* @param rmw The edge points to this ModelAction; this action must read from
* @param rmw The edge points to this ModelAction; this action must read from
- *
ModelAction
from
+ *
the ModelAction/Promise
from
*/
*/
-void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
+template <typename T>
+void CycleGraph::addRMWEdge(const T *from, const ModelAction *rmw)
{
ASSERT(from);
ASSERT(rmw);
{
ASSERT(from);
ASSERT(rmw);
@@
-240,6
+247,9
@@
void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw)
addNodeEdge(fromnode, rmwnode);
}
addNodeEdge(fromnode, rmwnode);
}
+/* Instantiate two forms of CycleGraph::addRMWEdge */
+template void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw);
+template void CycleGraph::addRMWEdge(const Promise *from, const ModelAction *rmw);
#if SUPPORT_MOD_ORDER_DUMP
void CycleGraph::dumpNodes(FILE *file) const
#if SUPPORT_MOD_ORDER_DUMP
void CycleGraph::dumpNodes(FILE *file) const
diff --git
a/cyclegraph.h
b/cyclegraph.h
index fcb1d30960843413814b07796c015866100cabf7..a9e46120f1f3efac17efacb9a608abca451868d4 100644
(file)
--- a/
cyclegraph.h
+++ b/
cyclegraph.h
@@
-30,8
+30,10
@@
class CycleGraph {
template <typename T, typename U>
bool addEdge(const T from, const U to);
template <typename T, typename U>
bool addEdge(const T from, const U to);
+ template <typename T>
+ void addRMWEdge(const T *from, const ModelAction *rmw);
+
bool checkForCycles() const;
bool checkForCycles() const;
- void addRMWEdge(const ModelAction *from, const ModelAction *rmw);
bool checkPromise(const ModelAction *from, Promise *p) const;
template <typename T>
bool checkPromise(const ModelAction *from, Promise *p) const;
template <typename T>