From 37c87f91496ff3e713003c21692c63b8e87d81fb Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 19 Jul 2012 14:15:27 -0700
Subject: [PATCH] Add RMW support to core.
Eliminate annoying warning.
---
cyclegraph.cc | 29 +++++++++++++++++++++++++++++
cyclegraph.h | 3 +++
model.cc | 5 ++---
snapshot-interface.cc | 2 +-
4 files changed, 35 insertions(+), 4 deletions(-)
diff --git a/cyclegraph.cc b/cyclegraph.cc
index c526af0..6676f2f 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -30,6 +30,29 @@ void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
fromnode->addEdge(tonode);
}
+void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
+ CycleNode *fromnode=getNode(from);
+ CycleNode *rmwnode=getNode(rmw);
+
+ /* Two RMW actions cannot read from the same write. */
+ if (fromnode->setRMW())
+ hasCycles=true;
+
+ /* Transfer all outgoing edges from the from node to the rmw node */
+ /* This process cannot add a cycle because rmw should not have any
+ incoming edges yet.*/
+ std::vector<CycleNode *> * edges=fromnode->getEdges();
+ for(unsigned int i=0;edges->size();i++) {
+ CycleNode * tonode=(*edges)[i];
+ rmwnode->addEdge(tonode);
+ }
+ if (!hasCycles) {
+ hasCycles=checkReachable(rmwnode, fromnode);
+ }
+ fromnode->addEdge(rmwnode);
+}
+
+
/** Checks whether the first CycleNode can reach the second one. */
bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) {
std::vector<CycleNode *> queue;
@@ -73,3 +96,9 @@ std::vector<CycleNode *> * CycleNode::getEdges() {
void CycleNode::addEdge(CycleNode * node) {
edges.push_back(node);
}
+
+bool CycleNode::setRMW() {
+ bool oldhasRMW=hasRMW;
+ hasRMW=true;
+ return oldhasRMW;
+}
diff --git a/cyclegraph.h b/cyclegraph.h
index a98e68c..6901700 100644
--- a/cyclegraph.h
+++ b/cyclegraph.h
@@ -15,6 +15,7 @@ class CycleGraph {
~CycleGraph();
void addEdge(const ModelAction *from, const ModelAction *to);
bool checkForCycles();
+ void addRMWEdge(const ModelAction *from, const ModelAction *to);
private:
CycleNode * getNode(const ModelAction *);
@@ -28,10 +29,12 @@ class CycleNode {
CycleNode(const ModelAction *action);
void addEdge(CycleNode * node);
std::vector<CycleNode *> * getEdges();
+ bool setRMW();
private:
const ModelAction *action;
std::vector<CycleNode *> edges;
+ bool hasRMW;
};
#endif
diff --git a/model.cc b/model.cc
index 3262f5e..9fc15cd 100644
--- a/model.cc
+++ b/model.cc
@@ -332,10 +332,9 @@ bool ModelChecker::isfeasible() {
/** Process a RMW by converting previous read into a RMW. */
void ModelChecker::process_rmw(ModelAction * act) {
int tid = id_to_int(act->get_tid());
- std::vector<action_list_t> *vec = &(*obj_thrd_map)[act->get_location()];
- ASSERT(tid < (int) vec->size());
- ModelAction *lastread=(*vec)[tid].back();
+ ModelAction *lastread=get_last_action(tid);
lastread->upgrade_rmw(act);
+ cyclegraph->addRMWEdge(lastread->get_reads_from(),lastread);
}
/**
diff --git a/snapshot-interface.cc b/snapshot-interface.cc
index 84749f1..84d9dbc 100644
--- a/snapshot-interface.cc
+++ b/snapshot-interface.cc
@@ -57,7 +57,7 @@ static void SnapshotGlobalSegments(){
if (buf[0]=='\n')
break;
- sscanf(buf, "%22s %p-%p [%5dK] %c%c%c/%c%c%c SM=%3s %200s\n", &type, &begin, &end, &size, &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
+ sscanf(buf, "%22s %p-%p [%5dK] %c%c%c/%c%c%c SM=%3s %200s\n", type, &begin, &end, &size, &r, &w, &x, &mr, &mw, &mx, smstr, regionname);
if (w == 'w' && (strstr(regionname, MYBINARYNAME) || strstr(regionname, MYLIBRARYNAME))) {
size_t len = ((uintptr_t)end - (uintptr_t)begin) / PAGESIZE;
--
2.34.1