towards making rmw work...
authorBrian Demsky <bdemsky@uci.edu>
Fri, 20 Jul 2012 19:32:42 +0000 (12:32 -0700)
committerBrian Norris <banorris@uci.edu>
Thu, 2 Aug 2012 17:12:46 +0000 (10:12 -0700)
[Split by Brian Norris]

action.cc
action.h
cmodelint.cc
cmodelint.h
cyclegraph.cc
cyclegraph.h
impatomic.cc
include/impatomic.h
model.cc
model.h

index 74ba5aa..1fb3b76 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -95,13 +95,19 @@ bool ModelAction::same_thread(const ModelAction *act) const
        return tid == act->tid;
 }
 
-void ModelAction::upgrade_rmw(ModelAction * act) {
-       ASSERT(is_read());
-       ASSERT(act->is_rmw());
-       //Upgrade our type to the act's type
+void ModelAction::copy_typeandorder(ModelAction * act) {
        this->type=act->type;
        this->order=act->order;
-       this->value=act->value;
+}
+
+void ModelAction::process_rmw(ModelAction * act) {
+       this->order=act->order;
+       if (act->is_rmwc())
+               this->type=ATOMIC_READ;
+       else if (act->is_rmw()) {
+               this->type=ATOMIC_RMW;
+               this->value=act->value;
+       }
 }
 
 /** The is_synchronizing method should only explore interleavings if:
@@ -206,7 +212,7 @@ void ModelAction::print(void) const
                type_str = "unknown type";
        }
 
-       uint64_t valuetoprint=type==ATOMIC_READ?reads_from->value:value;
+       uint64_t valuetoprint=type==ATOMIC_READ?(reads_from!=NULL?reads_from->value:VALUE_NONE):value;
 
        printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %-12" PRIu64,
                        seq_number, id_to_int(tid), type_str, order, location, valuetoprint);
index 5ab36b3..8d06aa4 100644 (file)
--- a/action.h
+++ b/action.h
@@ -91,7 +91,8 @@ public:
                return get_seq_number() > act.get_seq_number();
        }
 
-       void upgrade_rmw(ModelAction * act);
+       void process_rmw(ModelAction * act);
+       void copy_typeandorder(ModelAction * act);
 
        MEMALLOC
 private:
index 20f257c..4754a82 100644 (file)
@@ -14,6 +14,15 @@ void model_init_action(void * obj, uint64_t val) {
        model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
 }
 
+uint64_t model_rmwr_action(void *obj, memory_order ord) {
+       model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
+       return thread_current()->get_return_value();
+}
+
 void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
        model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
 }
+
+void model_rmwc_action(void *obj, memory_order ord) {
+       model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
+}
index 0f65327..5e762f8 100644 (file)
@@ -9,8 +9,11 @@ extern "C" {
 
 uint64_t model_read_action(void * obj, memory_order ord);
 void model_write_action(void * obj, memory_order ord, uint64_t val);
-void model_rmw_action(void *obj, memory_order ord, uint64_t val);
 void model_init_action(void * obj, uint64_t val);
+uint64_t model_rmwr_action(void *obj, memory_order ord);
+void model_rmw_action(void *obj, memory_order ord, uint64_t val);
+void model_rmwc_action(void *obj, memory_order ord);
+
 
 #if __cplusplus
 }
index 6676f2f..c0e8e2a 100644 (file)
@@ -20,35 +20,53 @@ CycleNode * CycleGraph::getNode(const ModelAction * action) {
 }
 
 /** Adds an edge between two ModelActions. */
-void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
+
+//the event to happens after the event from
+
+void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
        CycleNode *fromnode=getNode(from);
        CycleNode *tonode=getNode(to);
+
        if (!hasCycles) {
                // Check for Cycles
                hasCycles=checkReachable(tonode, fromnode);
        }
        fromnode->addEdge(tonode);
+
+       CycleNode * rmwnode=fromnode->getRMW();
+
+       //If the fromnode has a rmwnode that is not the tonode, we
+       //should add an edge between its rmwnode and the tonode
+
+       if (rmwnode!=NULL&&rmwnode!=tonode) {
+               if (!hasCycles) {
+                       // Check for Cycles
+                       hasCycles=checkReachable(tonode, rmwnode);
+               }
+               rmwnode->addEdge(tonode);
+       }
 }
 
-void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
+//event rmw that reads from the node from
+
+void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction * from) {
        CycleNode *fromnode=getNode(from);
        CycleNode *rmwnode=getNode(rmw);
 
        /* Two RMW actions cannot read from the same write. */
-       if (fromnode->setRMW())
+       if (fromnode->setRMW(rmwnode)) {
                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++) {
+       for(unsigned int i=0;i<edges->size();i++) {
                CycleNode * tonode=(*edges)[i];
                rmwnode->addEdge(tonode);
        }
-       if (!hasCycles) {
-               hasCycles=checkReachable(rmwnode, fromnode);
-       }
+
        fromnode->addEdge(rmwnode);
 }
 
@@ -85,6 +103,7 @@ bool CycleGraph::checkForCycles() {
 /** Constructor for a CycleNode. */
 CycleNode::CycleNode(const ModelAction *modelaction) {
        action=modelaction;
+       hasRMW=NULL;
 }
 
 /** Returns a vector of the edges from a CycleNode. */
@@ -97,8 +116,12 @@ void CycleNode::addEdge(CycleNode * node) {
        edges.push_back(node);
 }
 
-bool CycleNode::setRMW() {
-       bool oldhasRMW=hasRMW;
-       hasRMW=true;
-       return oldhasRMW;
+CycleNode* CycleNode::getRMW() {
+       return hasRMW;
+}
+
+bool CycleNode::setRMW(CycleNode * node) {
+       CycleNode * oldhasRMW=hasRMW;
+       hasRMW=node;
+       return (oldhasRMW!=NULL);
 }
index 6901700..3ed4e4a 100644 (file)
@@ -29,12 +29,13 @@ class CycleNode {
        CycleNode(const ModelAction *action);
        void addEdge(CycleNode * node);
        std::vector<CycleNode *> * getEdges();
-       bool setRMW();
+       bool setRMW(CycleNode *);
+       CycleNode* getRMW();
 
  private:
        const ModelAction *action;
        std::vector<CycleNode *> edges;
-       bool hasRMW;
+       CycleNode * hasRMW;
 };
 
 #endif
index 8642bee..df11202 100644 (file)
@@ -6,7 +6,7 @@ namespace std {
 
 bool atomic_flag_test_and_set_explicit ( volatile atomic_flag * __a__, memory_order __x__ ) {
        volatile bool * __p__ = &((__a__)->__f__);
-       model->switch_to_master(new ModelAction(ATOMIC_READ, __x__, (void *) __p__));
+       model->switch_to_master(new ModelAction(ATOMIC_RMWR, __x__, (void *) __p__));
        bool result = (bool) thread_current()->get_return_value();
        model->switch_to_master(new ModelAction(ATOMIC_RMW, __x__, (void *) __p__, true));
        return result;
index 4d842d6..808dc12 100644 (file)
@@ -92,7 +92,7 @@ inline void atomic_flag::fence( memory_order __x__ ) const volatile
 
 #define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ )                                                                          \
        ({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__);                     \
-       __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_read_action((void *)__p__, __x__); \
+       __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
        __typeof__(__m__) __v__ = (__m__);                                                                                                                                              \
        __typeof__((__a__)->__f__) __copy__= __old__;                                                                                                   \
        __copy__ __o__ __v__;                                                                                                                                                                                                   \
@@ -104,10 +104,10 @@ inline void atomic_flag::fence( memory_order __x__ ) const volatile
                __typeof__(__e__) __q__ = (__e__);                                                                                                                                      \
                __typeof__(__m__) __v__ = (__m__);                                                                                                                                      \
                bool __r__;                                                                                                                                                                                                                                     \
-               __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_read_action((void *)__p__, __x__);\
+               __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__);\
                if (__t__ == * __q__ ) {                                                                                                                                                                                \
                        model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
-               else {  *__q__ = __t__;  __r__ = false;}                                                                                                                \
+               else {  model_rmwc_action((void *)__p__, __x__); *__q__ = __t__;  __r__ = false;} \
                __r__; })
 
 //TODO
@@ -2121,7 +2121,7 @@ inline void* atomic_fetch_add_explicit
 ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
 {
        void* volatile* __p__ = &((__a__)->__f__);
-       void* __r__ = (void *) model_read_action((void *)__p__, __x__);
+       void* __r__ = (void *) model_rmwr_action((void *)__p__, __x__);
        model_rmw_action((void *)__p__, __x__, (uint64_t) ((char*)(*__p__) + __m__));
   return __r__; }
 
@@ -2134,7 +2134,7 @@ inline void* atomic_fetch_sub_explicit
 ( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
 {
        void* volatile* __p__ = &((__a__)->__f__);
-       void* __r__ = (void *) model_read_action((void *)__p__, __x__);
+       void* __r__ = (void *) model_rmwr_action((void *)__p__, __x__);
        model_rmw_action((void *)__p__, __x__, (uint64_t)((char*)(*__p__) - __m__));
   return __r__; }
 
index 726901b..59f148e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -250,36 +250,37 @@ ModelAction * ModelChecker::get_next_backtrack()
 void ModelChecker::check_current_action(void)
 {
        ModelAction *curr = this->current_action;
-       ModelAction *tmp;
-       current_action = NULL;
+       bool already_added = false;
+       this->current_action = NULL;
        if (!curr) {
                DEBUG("trying to push NULL action...\n");
                return;
        }
 
-       if (curr->is_rmw()) {
-               //We have a RMW action
-               process_rmw(curr);
-               //Force the current thread to continue since the RMW should be atomic
-               nextThread = thread_current()->get_id();
-               delete curr;
-               return;
-       }
-
-       tmp = node_stack->explore_action(curr);
-       if (tmp) {
-               /* Discard duplicate ModelAction; use action from NodeStack */
+       if (curr->is_rmwc()||curr->is_rmw()) {
+               ModelAction *tmp=process_rmw(curr);
+               already_added = true;
                delete curr;
-               curr = tmp;
+               curr=tmp;
        } else {
-               /*
-                * Perform one-time actions when pushing new ModelAction onto
-                * NodeStack
-                */
-               curr->create_cv(get_parent_action(curr->get_tid()));
-               /* Build may_read_from set */
-               if (curr->is_read())
-                       build_reads_from_past(curr);
+               ModelAction * tmp = node_stack->explore_action(curr);
+               if (tmp) {
+                       /* Discard duplicate ModelAction; use action from NodeStack */
+                       /* First restore type and order in case of RMW operation */
+                       if (curr->is_rmwr())
+                               tmp->copy_typeandorder(curr);
+                       delete curr;
+                       curr = tmp;
+               } else {
+                       /*
+                        * Perform one-time actions when pushing new ModelAction onto
+                        * NodeStack
+                        */
+                       curr->create_cv(get_parent_action(curr->get_tid()));
+                       /* Build may_read_from set */
+                       if (curr->is_read())
+                               build_reads_from_past(curr);
+               }
        }
 
        /* Assign 'creation' parent */
@@ -288,21 +289,6 @@ void ModelChecker::check_current_action(void)
                th->set_creation(curr);
        }
 
-       /* Is there a better interface for setting the next thread rather
-                than this field/convoluted approach?  Perhaps like just returning
-                it or something? */
-
-       nextThread = get_next_replay_thread();
-
-       Node *currnode = curr->get_node();
-       Node *parnode = currnode->get_parent();
-
-       if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
-               if (!next_backtrack || *curr > *next_backtrack)
-                       next_backtrack = curr;
-
-       set_backtracking(curr);
-
        /* Assign reads_from values */
        Thread *th = get_thread(curr->get_tid());
        uint64_t value = VALUE_NONE;
@@ -318,8 +304,30 @@ void ModelChecker::check_current_action(void)
 
        th->set_return_value(value);
 
-       /* Add action to list last.  */
-       add_action_to_lists(curr);
+       /* Add action to list.  */
+       if (!already_added)
+               add_action_to_lists(curr);
+
+       /* Do not split atomic actions. */
+       if (curr->is_rmwr()) {
+               nextThread = thread_current()->get_id();
+               return;
+       }
+
+       /* Is there a better interface for setting the next thread rather
+                than this field/convoluted approach?  Perhaps like just returning
+                it or something? */
+
+       nextThread = get_next_replay_thread();
+
+       Node *currnode = curr->get_node();
+       Node *parnode = currnode->get_parent();
+
+       if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
+               if (!next_backtrack || *curr > *next_backtrack)
+                       next_backtrack = curr;
+
+       set_backtracking(curr);
 }
 
 /** @returns whether the current trace is feasible. */
@@ -327,12 +335,14 @@ bool ModelChecker::isfeasible() {
        return !cyclegraph->checkForCycles();
 }
 
-/** Process a RMW by converting previous read into a RMW. */
-void ModelChecker::process_rmw(ModelAction * act) {
+/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
+ModelAction * ModelChecker::process_rmw(ModelAction * act) {
        int tid = id_to_int(act->get_tid());
        ModelAction *lastread=get_last_action(tid);
-       lastread->upgrade_rmw(act);
-       cyclegraph->addRMWEdge(lastread->get_reads_from(),lastread);
+       lastread->process_rmw(act);
+       if (act->is_rmw())
+               cyclegraph->addRMWEdge(lastread, lastread->get_reads_from());
+       return lastread;
 }
 
 /**
diff --git a/model.h b/model.h
index 76ded6c..8593b98 100644 (file)
--- a/model.h
+++ b/model.h
@@ -82,7 +82,7 @@ private:
        ModelAction * get_parent_action(thread_id_t tid);
        ModelAction * get_last_seq_cst(const void *location);
        void build_reads_from_past(ModelAction *curr);
-       void process_rmw(ModelAction * curr);
+       ModelAction * process_rmw(ModelAction * curr);
        void r_modification_order(ModelAction * curr, const ModelAction *rf);
        void w_modification_order(ModelAction * curr);