X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=775b796f167d68ee8394a0e828b0791e122a4937;hb=730038c9f0475c6c4355c8b2a15cab702207e5c3;hp=52eab24c6790fdc472bdfc30937fa356aa319fed;hpb=b133a2b2e11e6b95dfa805b9b90a4e53dce3d81d;p=model-checker.git diff --git a/model.cc b/model.cc index 52eab24..775b796 100644 --- a/model.cc +++ b/model.cc @@ -235,7 +235,7 @@ void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { Thread *thr=get_thread(tid); if ( scheduler->get_enabled(thr) == THREAD_SLEEP_SET ) { ModelAction *pending_act=thr->get_pending(); - if (pending_act->could_synchronize_with(curr)) { + if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) { //Remove this thread from sleep set scheduler->remove_sleep(thr); } @@ -856,7 +856,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) ModelAction *newcurr = initialize_curr_action(curr); - wake_up_sleeping_actions(curr); + wake_up_sleeping_actions(newcurr); /* Add the action to lists before any other model-checking tasks */ if (!second_part_of_rmw)