rmw example works

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 3262f5e55caf992397d9134f24f2bba325cc4e87..e18fda15248399cda859339296447ca2b35bd9f5 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -118,7 +118,6 @@ Thread * ModelChecker::schedule_next_thread()
  */
 thread_id_t ModelChecker::get_next_replay_thread()
 {
-       ModelAction *next;
        thread_id_t tid;
 
        /* Have we completed exploring the preselected path? */
@@ -126,7 +125,7 @@ thread_id_t ModelChecker::get_next_replay_thread()
                return THREAD_ID_T_NONE;
 
        /* Else, we are trying to replay an execution */
-       next = node_stack->get_next()->get_action();
+       ModelAction * next = node_stack->get_next()->get_action();
 
        if (next == diverge) {
                Node *nextnode = next->get_node();
@@ -250,36 +249,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,24 +288,7 @@ 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 */
-       /* TODO: perform release/acquire synchronization here; include
-        * reads_from as ModelAction member? */
        Thread *th = get_thread(curr->get_tid());
        uint64_t value = VALUE_NONE;
        if (curr->is_read()) {
@@ -320,8 +303,29 @@ 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);
+
+       /* Is there a better interface for setting the next thread rather
+                than this field/convoluted approach?  Perhaps like just returning
+                it or something? */
+
+       /* Do not split atomic actions. */
+       if (curr->is_rmwr()) {
+               nextThread = thread_current()->get_id();
+       } else {
+               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. */
@@ -329,13 +333,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());
-       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);
+       ModelAction *lastread=get_last_action(tid);
+       lastread->process_rmw(act);
+       if (act->is_rmw())
+               cyclegraph->addRMWEdge(lastread, lastread->get_reads_from());
+       return lastread;
 }
 
 /**
@@ -534,7 +539,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                /* TODO: need a more informative way of reporting errors */
                printf("ERROR: may read from uninitialized atomic\n");
        }
-       
+
        if (DBG_ENABLED() || !initialized) {
                printf("Reached read action:\n");
                curr->print();
@@ -542,7 +547,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                curr->get_node()->print_may_read_from();
                printf("End printing may_read_from\n");
        }
-       
+
        ASSERT(initialized);
 }
 
@@ -598,10 +603,8 @@ void ModelChecker::remove_thread(Thread *t)
  */
 int ModelChecker::switch_to_master(ModelAction *act)
 {
-       Thread *old;
-
        DBG();
-       old = thread_current();
+       Thread * old = thread_current();
        set_current_action(act);
        old->set_state(THREAD_READY);
        return Thread::swap(old, get_system_context());