small changes (things still work) towards support RMW

Reserve value field only for writes. Using it for reads will only make thinks
weird for RMW operations.

[Amended by Brian Norris]

diff --git a/action.cc b/action.cc
index b5c72c0226aa8e562cf80cedd6444e2088bb19ba..c617f0d70b15ab8b22f957e7103b8cd4aa78a4d9 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -28,12 +28,12 @@ ModelAction::~ModelAction()
 
 bool ModelAction::is_read() const
 {
-       return type == ATOMIC_READ;
+       return type == ATOMIC_READ || type == ATOMIC_RMW;
 }
 
 bool ModelAction::is_write() const
 {
-       return type == ATOMIC_WRITE || type == ATOMIC_INIT;
+       return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT;
 }
 
 bool ModelAction::is_rmw() const
@@ -85,6 +85,15 @@ 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
+       this->type=act->type;
+       this->order=act->order;
+       this->value=act->value;
+}
+
 /** The is_synchronizing method should only explore interleavings if:
  *  (1) the operations are seq_cst and don't commute or
  *  (2) the reordering may establish or break a synchronization relation.
@@ -136,7 +145,6 @@ void ModelAction::read_from(const ModelAction *act)
        if (act->is_release() && this->is_acquire())
                cv->merge(act->cv);
        reads_from = act;
-       value = act->value;
 }
 
 /**
@@ -182,8 +190,10 @@ void ModelAction::print(void) const
                type_str = "unknown type";
        }
 
+       uint64_t valuetoprint=type==ATOMIC_READ?reads_from->value:value;
+
        printf("(%3d) Thread: %-2d    Action: %-13s    MO: %d    Loc: %14p    Value: %-12" PRIu64,
-                       seq_number, id_to_int(tid), type_str, order, location, value);
+                       seq_number, id_to_int(tid), type_str, order, location, valuetoprint);
        if (reads_from)
                printf(" Rf: %d", reads_from->get_seq_number());
        if (cv) {

diff --git a/action.h b/action.h
index 36c72079b165a6a7462d5a32698e61dbdef12dbd..fff6bc8226990010bae9270a021d606f0cd5fa05 100644 (file)
--- a/action.h
+++ b/action.h
@@ -80,6 +80,8 @@ public:
                return get_seq_number() > act.get_seq_number();
        }
 
+       void upgrade_rmw(ModelAction * act);
+
        MEMALLOC
 private:
 
@@ -95,8 +97,7 @@ private:
        /** The thread id that performed this action. */
        thread_id_t tid;
 
-       /** The value read or written (if RMW, then the value written). This
-        * should probably be something longer. */
+       /** The value written (for write or RMW; undefined for read) */
        uint64_t value;
 
        /** The action that this action reads from. Only valid for reads */

diff --git a/model.cc b/model.cc
index cf845ecd215a68a83c3ca1a449c7f06cf557a808..1b379000d75f4832795190acc8e583f933ee7675 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -252,6 +252,15 @@ void ModelChecker::check_current_action(void)
                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 */
@@ -274,6 +283,10 @@ 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();
@@ -310,6 +323,15 @@ bool ModelChecker::isfeasible() {
        return !cyclegraph->checkForCycles();
 }
 
+/** 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();
+       lastread->upgrade_rmw(act);
+}
+
 void ModelChecker::r_modification_order(ModelAction * curr, const ModelAction *rf) {
        std::vector<action_list_t> *thrd_lists = &(*obj_thrd_map)[curr->get_location()];
        unsigned int i;

diff --git a/model.h b/model.h
index 4c0af0af1f3e33ba3aaa0e3bc5a74f67f6cd9c10..a4751099cfdf6f7eda943e3b832e705acaaa68d8 100644 (file)
--- a/model.h
+++ b/model.h
@@ -83,6 +83,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);
        void r_modification_order(ModelAction * curr, const ModelAction *rf);
        void w_modification_order(ModelAction * curr);