From: Brian Demsky Date: Tue, 18 Sep 2012 22:46:29 +0000 (-0700) Subject: changes X-Git-Tag: pldi2013~186 X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=7f6d1166c41b6b00405eb8cd00d3adda5440f386 changes --- diff --git a/model.cc b/model.cc index 0074922..72919c6 100644 --- a/model.cc +++ b/model.cc @@ -33,7 +33,6 @@ ModelChecker::ModelChecker(struct model_params params) : lazy_sync_with_release(new HashTable, uintptr_t, 4>()), thrd_last_action(new std::vector(1)), node_stack(new NodeStack()), - is_enabled(NULL), mo_graph(new CycleGraph()), failed_promise(false), too_many_reads(false), @@ -53,8 +52,6 @@ ModelChecker::~ModelChecker() for (int i = 0; i < get_num_threads(); i++) delete thread_map->get(i); delete thread_map; - if (is_enabled) - free(is_enabled); delete obj_thrd_map; delete obj_map; @@ -89,13 +86,7 @@ void ModelChecker::reset_to_initial_state() /** @returns a thread ID for a new Thread */ thread_id_t ModelChecker::get_next_id() { - thread_id_t newid=priv->next_thread_id++; - bool * tmp=(bool *) malloc((newid+1)*sizeof(bool)); - memcpy(tmp, is_enabled, newid*sizeof(bool)); - tmp[newid]=true; - free(is_enabled); - is_enabled=tmp; - return newid; + return priv->next_thread_id++; } /** @returns the number of user threads created during this execution */ @@ -379,17 +370,17 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) curr = tmp; compute_promises(curr); } else { - ModelAction *tmp = node_stack->explore_action(curr, NULL); + ModelAction *tmp = node_stack->explore_action(curr, scheduler->get_enabled()); 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); - + /* If we have diverged, we need to reset the clock vector. */ if (diverge == NULL) tmp->create_cv(get_parent_action(tmp->get_tid())); - + delete curr; curr = tmp; } else { @@ -1342,25 +1333,23 @@ int ModelChecker::switch_to_master(ModelAction *act) * @return Returns true (success) if a step was taken and false otherwise. */ bool ModelChecker::take_step() { - Thread *curr, *next; - if (has_asserted()) return false; - curr = thread_current(); + Thread * curr = thread_current(); if (curr) { if (curr->get_state() == THREAD_READY) { ASSERT(priv->current_action); priv->nextThread = check_current_action(priv->current_action); priv->current_action = NULL; - if (!curr->is_blocked() && !curr->is_complete()) - scheduler->add_thread(curr); + if (curr->is_blocked() || curr->is_complete()) + scheduler->remove_thread(curr); } else { ASSERT(false); } } - next = scheduler->next_thread(priv->nextThread); + Thread * next = scheduler->next_thread(priv->nextThread); /* Infeasible -> don't take any more steps */ if (!isfeasible()) diff --git a/model.h b/model.h index 54f3026..4fc32c6 100644 --- a/model.h +++ b/model.h @@ -177,8 +177,6 @@ private: * together for efficiency and maintainability. */ struct model_snapshot_members *priv; - bool * is_enabled; - /** * @brief The modification order graph * diff --git a/nodestack.cc b/nodestack.cc index 69f0b5f..2e170b9 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -332,7 +332,7 @@ void NodeStack::print() printf("............................................\n"); } -ModelAction * NodeStack::explore_action(ModelAction *act, bool * enabled) +ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled) { DBG(); @@ -347,7 +347,7 @@ ModelAction * NodeStack::explore_action(ModelAction *act, bool * enabled) /* Record action */ get_head()->explore_child(act); - node_list.push_back(new Node(act, get_head(), model->get_num_threads(), enabled)); + node_list.push_back(new Node(act, get_head(), model->get_num_threads())); total_nodes++; iter++; return NULL; diff --git a/nodestack.h b/nodestack.h index 6cd8cfd..3262a56 100644 --- a/nodestack.h +++ b/nodestack.h @@ -120,7 +120,7 @@ class NodeStack { public: NodeStack(); ~NodeStack(); - ModelAction * explore_action(ModelAction *act, bool * enabled); + ModelAction * explore_action(ModelAction *act, bool * is_enabled); Node * get_head(); Node * get_next(); void reset_execution(); diff --git a/schedule.cc b/schedule.cc index cbb4957..b19a5d3 100644 --- a/schedule.cc +++ b/schedule.cc @@ -5,10 +5,26 @@ /** Constructor */ Scheduler::Scheduler() : + is_enabled(NULL), + enabled_len(0), + curr_thread_index(0), current(NULL) { } +void Scheduler::set_enabled(Thread *t, bool enabled_status) { + int threadid=id_to_int(t->get_id()); + if (threadid>=enabled_len) { + bool * new_enabled=(bool *)malloc(sizeof(bool)*(threadid+1)); + memcpy(new_enabled, is_enabled, enabled_len*sizeof(bool)); + memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(bool)); + free(is_enabled); + is_enabled=new_enabled; + enabled_len=threadid+1; + } + is_enabled[threadid]=enabled_status; +} + /** * Add a Thread to the scheduler's ready list. * @param t The Thread to add @@ -16,7 +32,7 @@ Scheduler::Scheduler() : void Scheduler::add_thread(Thread *t) { DEBUG("thread %d\n", t->get_id()); - readyList.push_back(t); + set_enabled(t, true); } /** @@ -27,8 +43,7 @@ void Scheduler::remove_thread(Thread *t) { if (current == t) current = NULL; - else - readyList.remove(t); + set_enabled(t, false); } /** @@ -38,7 +53,7 @@ void Scheduler::remove_thread(Thread *t) */ void Scheduler::sleep(Thread *t) { - remove_thread(t); + set_enabled(t, false); t->set_state(THREAD_BLOCKED); } @@ -48,7 +63,7 @@ void Scheduler::sleep(Thread *t) */ void Scheduler::wake(Thread *t) { - add_thread(t); + set_enabled(t, true); t->set_state(THREAD_READY); } @@ -62,19 +77,22 @@ void Scheduler::wake(Thread *t) */ Thread * Scheduler::next_thread(Thread *t) { - if (t != NULL) { - current = t; - readyList.remove(t); - } else if (readyList.empty()) { - t = NULL; - } else { - t = readyList.front(); - current = t; - readyList.pop_front(); + if ( t == NULL ) { + int old_curr_thread = curr_thread_index; + while(true) { + curr_thread_index = (curr_thread_index+1) % enabled_len; + if (is_enabled[curr_thread_index]) { + t = model->get_thread(int_to_id(curr_thread_index)); + break; + } + if (curr_thread_index == old_curr_thread) { + print(); + return NULL; + } + } } - + current = t; print(); - return t; } @@ -96,9 +114,4 @@ void Scheduler::print() const DEBUG("Current thread: %d\n", current->get_id()); else DEBUG("No current thread\n"); - DEBUG("Num. threads in ready list: %zu\n", readyList.size()); - - std::list >::const_iterator it; - for (it = readyList.begin(); it != readyList.end(); it++) - DEBUG("In ready list: thread %d\n", (*it)->get_id()); } diff --git a/schedule.h b/schedule.h index a7483e0..fb4d082 100644 --- a/schedule.h +++ b/schedule.h @@ -23,11 +23,15 @@ public: Thread * next_thread(Thread *t); Thread * get_current_thread() const; void print() const; + bool * get_enabled() { return is_enabled; }; SNAPSHOTALLOC private: /** The list of available Threads that are not currently running */ - std::list readyList; + bool * is_enabled; + int enabled_len; + int curr_thread_index; + void set_enabled(Thread *t, bool enabled_status); /** The currently-running Thread */ Thread *current;