X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;ds=sidebyside;f=model.cc;h=83c79c97ffc654818df100c04ebbf5efa8c244a6;hb=dcf7f575967bec560d500cc4f52e35c21671525c;hp=715a2584f36a1538528489d60f987142ad0f2a77;hpb=9bdbedb24f7c16c4941ec6b711fc8065e0cee9d3;p=model-checker.git diff --git a/model.cc b/model.cc index 715a258..83c79c9 100644 --- a/model.cc +++ b/model.cc @@ -286,8 +286,7 @@ void ModelChecker::execute_sleep_set() { for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET && - thr->get_pending() == NULL ) { + if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) { thr->set_state(THREAD_RUNNING); scheduler->next_thread(thr); Thread::swap(&system_context, thr); @@ -298,16 +297,15 @@ void ModelChecker::execute_sleep_set() { priv->current_action = NULL; } -void ModelChecker::wake_up_sleeping_actions(ModelAction * curr) { - for(unsigned int i=0;iget_enabled(thr) == THREAD_SLEEP_SET ) { - ModelAction *pending_act=thr->get_pending(); - if ((!curr->is_rmwr())&&pending_act->could_synchronize_with(curr)) { +void ModelChecker::wake_up_sleeping_actions(ModelAction *curr) +{ + for (unsigned int i = 0; i < get_num_threads(); i++) { + Thread *thr = get_thread(int_to_id(i)); + if (scheduler->is_sleep_set(thr)) { + ModelAction *pending_act = thr->get_pending(); + if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr)) //Remove this thread from sleep set scheduler->remove_sleep(thr); - } } } }