X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=schedule.cc;h=f68cb528a16b846a2f2653ecd3336b6ca496fee8;hb=a2176c7545c29b28598bb252718cf080a3463665;hp=4f5f3de7d70ddf881e15ac6bd39cb27c795c728e;hpb=f19fd46f4e67fd2d4a4041a4eecaa6789f97aba1;p=model-checker.git diff --git a/schedule.cc b/schedule.cc index 4f5f3de..f68cb52 100644 --- a/schedule.cc +++ b/schedule.cc @@ -1,74 +1,190 @@ +#include #include -#include "libthreads.h" +#include "threads-model.h" #include "schedule.h" #include "common.h" #include "model.h" +#include "nodestack.h" -struct thread_list_node { - struct thread *t; - struct thread_list_node *next; - int live; -}; - -#define NUM_LIST_NODES 32 +/** Constructor */ +Scheduler::Scheduler() : + enabled(NULL), + enabled_len(0), + curr_thread_index(0), + current(NULL) +{ +} -struct thread_list_node *head, *tail; -struct thread_list_node nodes[NUM_LIST_NODES]; -struct thread *current; +void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) { + int threadid=id_to_int(t->get_id()); + if (threadid>=enabled_len) { + enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1)); + memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(enabled_type_t)); + if (enabled != NULL) { + memcpy(new_enabled, enabled, enabled_len*sizeof(enabled_type_t)); + snapshot_free(enabled); + } + enabled=new_enabled; + enabled_len=threadid+1; + } + enabled[threadid]=enabled_status; +} -static void enqueue_thread(struct thread *t) +/** + * @brief Check if a Thread is currently enabled + * @param t The Thread to check + * @return True if the Thread is currently enabled + */ +bool Scheduler::is_enabled(Thread *t) const { - int i; - struct thread_list_node *node; + int id = id_to_int(t->get_id()); + return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED); +} - for (node = nodes, i = 0; node->live && i < NUM_LIST_NODES; i++, node++); - if (i >= NUM_LIST_NODES) { - printf("ran out of nodes\n"); - exit(1); - } - node->t = t; - node->next = NULL; - node->live = 1; +enabled_type_t Scheduler::get_enabled(Thread *t) { + return enabled[id_to_int(t->get_id())]; +} - if (tail) - tail->next = node; - else - head = node; - tail = node; +void Scheduler::update_sleep_set(Node *n) { + enabled_type_t *enabled_array=n->get_enabled_array(); + for(int i=0;iget_id())); + set_enabled(t, THREAD_SLEEP_SET); +} - if (!head) - return NULL; +/** + * Remove a Thread from the sleep set. + * @param t The Thread to remove + */ +void Scheduler::remove_sleep(Thread *t) +{ + DEBUG("thread %d\n", id_to_int(t->get_id())); + set_enabled(t, THREAD_ENABLED); +} - pop = head->t; - head->live = 0; - if (head == tail) - tail = NULL; - head = head->next; +/** + * Add a Thread to the scheduler's ready list. + * @param t The Thread to add + */ +void Scheduler::add_thread(Thread *t) +{ + DEBUG("thread %d\n", id_to_int(t->get_id())); + ASSERT(!t->is_model_thread()); + set_enabled(t, THREAD_ENABLED); +} - /* Set new current thread */ - current = pop; +/** + * Remove a given Thread from the scheduler. + * @param t The Thread to remove + */ +void Scheduler::remove_thread(Thread *t) +{ + if (current == t) + current = NULL; + set_enabled(t, THREAD_DISABLED); +} - return pop; +/** + * Prevent a Thread from being scheduled. The sleeping Thread should be + * re-awoken via Scheduler::wake. + * @param thread The Thread that should sleep + */ +void Scheduler::sleep(Thread *t) +{ + set_enabled(t, THREAD_DISABLED); + t->set_state(THREAD_BLOCKED); } -void DefaultScheduler::add_thread(struct thread *t) +/** + * Wake a Thread up that was previously waiting (see Scheduler::wait) + * @param t The Thread to wake up + */ +void Scheduler::wake(Thread *t) { - DEBUG("thread %d\n", t->id); - enqueue_thread(t); + ASSERT(!t->is_model_thread()); + set_enabled(t, THREAD_ENABLED); + t->set_state(THREAD_READY); } -struct thread *DefaultScheduler::next_thread(void) +/** + * Select a Thread. This implementation defaults to round-robin, if a + * thread is not already provided. + * + * @param t Thread to run, if chosen by an external entity (e.g., + * ModelChecker). May be NULL to indicate no external choice. + * @return The next Thread to run + */ +Thread * Scheduler::next_thread(Thread *t) { - return dequeue_thread(); + if ( t == NULL ) { + int old_curr_thread = curr_thread_index; + bool have_enabled_thread_with_priority=false; + Node *n=model->get_curr_node(); + + for(int i=0;ihas_priority(tid)) { + //Have a thread with priority + if (enabled[i]!=THREAD_DISABLED) + have_enabled_thread_with_priority=true; + } + } + + while(true) { + curr_thread_index = (curr_thread_index+1) % enabled_len; + thread_id_t curr_tid=int_to_id(curr_thread_index); + if (enabled[curr_thread_index]==THREAD_ENABLED&& + (!have_enabled_thread_with_priority||n->has_priority(curr_tid))) { + t = model->get_thread(int_to_id(curr_tid)); + break; + } + if (curr_thread_index == old_curr_thread) { + print(); + return NULL; + } + } + } else if (t->is_model_thread()) { + /* model-checker threads never run */ + t = NULL; + } else { + curr_thread_index = id_to_int(t->get_id()); + } + + current = t; + print(); + return t; } -struct thread *DefaultScheduler::get_current_thread(void) +/** + * @return The currently-running Thread + */ +Thread * Scheduler::get_current_thread() const { + ASSERT(!current || !current->is_model_thread()); return current; } + +/** + * Print debugging information about the current state of the scheduler. Only + * prints something if debugging is enabled. + */ +void Scheduler::print() const +{ + if (current) + DEBUG("Current thread: %d\n", id_to_int(current->get_id())); + else + DEBUG("No current thread\n"); +}