Add RMW support to core.

Eliminate annoying warning.

diff --git a/cyclegraph.cc b/cyclegraph.cc
index c526af0f590266a825f698be60fb92c4354d1a9c..6676f2f0a7ea4a000f2555810cbc4f31f0112263 100644 (file)
--- 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 a98e68c972e77cf6b615cff94521bd872df4e26a..690170022b3746c878c253d46eb58cc102f5c50c 100644 (file)
--- 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 3262f5e55caf992397d9134f24f2bba325cc4e87..9fc15cd894fc48062c74ac131884fbebc530a5e2 100644 (file)
--- 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 84749f1f4b0d3a3fa2cca047dee826696eba84c9..84d9dbc015f0d6d593f4e72da807042c8bc3e373 100644 (file)
--- 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;