Add RMW support to core.
authorBrian Demsky <bdemsky@uci.edu>
Thu, 19 Jul 2012 21:15:27 +0000 (14:15 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 2 Aug 2012 17:12:37 +0000 (10:12 -0700)
Eliminate annoying warning.

cyclegraph.cc
cyclegraph.h
model.cc
snapshot-interface.cc

index c526af0..6676f2f 100644 (file)
@@ -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;
+}
index a98e68c..6901700 100644 (file)
@@ -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
index 3262f5e..9fc15cd 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);
 }
 
 /**
index 84749f1..84d9dbc 100644 (file)
@@ -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;