X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=c022e9e3baab9c716498992bc09e525fca61ce69;hb=bf698c32ac174a4dcfce69ad78cccf2a65e3bf92;hp=5292b24745a3eaa2c9ddd99c904dfd05718bc1b6;hpb=193c917736aedbc4b34e6cae3e6eb35eb5e98502;p=c11tester.git diff --git a/model.cc b/model.cc index 5292b247..c022e9e3 100644 --- a/model.cc +++ b/model.cc @@ -366,12 +366,31 @@ Thread* ModelChecker::getNextThread(Thread *old) thr->freeResources(); } - /* Don't schedule threads which should be disabled */ ModelAction *act = thr->get_pending(); - if (act && execution->is_enabled(thr) && !execution->check_action_enabled(act)) { - scheduler->sleep(thr); + if (act && execution->is_enabled(tid)){ + /* Don't schedule threads which should be disabled */ + if (!execution->check_action_enabled(act)) { + scheduler->sleep(thr); + } + + /* Allow pending relaxed/release stores or thread actions to perform first */ + else if (!thread_chosen) { + if (act->is_write()) { + std::memory_order order = act->get_mo(); + if (order == std::memory_order_relaxed || \ + order == std::memory_order_release) { + chosen_thread = thr; + thread_chosen = true; + } + } else if (act->get_type() == THREAD_CREATE || \ + act->get_type() == PTHREAD_CREATE || \ + act->get_type() == THREAD_START || \ + act->get_type() == THREAD_FINISH) { + chosen_thread = thr; + thread_chosen = true; + } + } } - chooseThread(act, thr); } return nextThread; } @@ -405,27 +424,6 @@ void ModelChecker::finishRunExecution(Thread *old) _Exit(0); } -/* Allow pending relaxed/release stores or thread actions to perform first */ -void ModelChecker::chooseThread(ModelAction *act, Thread *thr) -{ - if (!thread_chosen && act && execution->is_enabled(thr) && (thr->get_state() != THREAD_BLOCKED) ) { - if (act->is_write()) { - std::memory_order order = act->get_mo(); - if (order == std::memory_order_relaxed || \ - order == std::memory_order_release) { - chosen_thread = thr; - thread_chosen = true; - } - } else if (act->get_type() == THREAD_CREATE || \ - act->get_type() == PTHREAD_CREATE || \ - act->get_type() == THREAD_START || \ - act->get_type() == THREAD_FINISH) { - chosen_thread = thr; - thread_chosen = true; - } - } -} - uint64_t ModelChecker::switch_thread(ModelAction *act) { if (modellock) {