From: Brian Demsky Date: Fri, 12 Oct 2012 05:51:45 +0000 (-0700) Subject: commit untested condvar code X-Git-Url: http://plrg.eecs.uci.edu/git/?p=cdsspec-compiler.git;a=commitdiff_plain;h=ffc110b3aaa80564dbf85f3c6a9049efd40571f1 commit untested condvar code --- diff --git a/action.cc b/action.cc index 44a6d9a..5705892 100644 --- a/action.cc +++ b/action.cc @@ -76,7 +76,7 @@ bool ModelAction::is_relseq_fixup() const bool ModelAction::is_mutex_op() const { - return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK; + return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL; } bool ModelAction::is_lock() const @@ -84,6 +84,18 @@ bool ModelAction::is_lock() const return type == ATOMIC_LOCK; } +bool ModelAction::is_wait() const { + return type == ATOMIC_WAIT; +} + +bool ModelAction::is_notify() const { + return type==ATOMIC_NOTIFY_ONE || type==ATOMIC_NOTIFY_ALL; +} + +bool ModelAction::is_notify_one() const { + return type==ATOMIC_NOTIFY_ONE; +} + bool ModelAction::is_unlock() const { return type == ATOMIC_UNLOCK; @@ -250,6 +262,10 @@ bool ModelAction::is_conflicting_lock(const ModelAction *act) const if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS) return true; + //Try to push a successful trylock past a wait + if (act->is_wait() && is_trylock() && value == VALUE_TRYSUCCESS) + return true; + return false; } diff --git a/action.h b/action.h index 21fed0c..f7e7e5e 100644 --- a/action.h +++ b/action.h @@ -93,6 +93,9 @@ public: bool is_lock() const; bool is_trylock() const; bool is_unlock() const; + bool is_wait() const; + bool is_notify() const; + bool is_notify_one() const; bool is_success_lock() const; bool is_failed_trylock() const; bool is_read() const; diff --git a/model.cc b/model.cc index b3b517c..101a5f0 100644 --- a/model.cc +++ b/model.cc @@ -31,6 +31,7 @@ ModelChecker::ModelChecker(struct model_params params) : thread_map(new HashTable()), obj_map(new HashTable()), lock_waiters_map(new HashTable()), + condvar_waiters_map(new HashTable()), obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector< Promise *, SnapshotAlloc >()), futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc >()), @@ -63,6 +64,7 @@ ModelChecker::~ModelChecker() delete obj_thrd_map; delete obj_map; delete lock_waiters_map; + delete condvar_waiters_map; delete action_trace; for (unsigned int i = 0; i < promises->size(); i++) @@ -162,7 +164,11 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) scheduler->update_sleep_set(prevnode); /* Reached divergence point */ - if (nextnode->increment_promise()) { + if (nextnode->increment_misc()) { + /* The next node will try to satisfy a different misc_index values. */ + tid = next->get_tid(); + node_stack->pop_restofstack(2); + } else if (nextnode->increment_promise()) { /* The next node will try to satisfy a different set of promises. */ tid = next->get_tid(); node_stack->pop_restofstack(2); @@ -319,6 +325,32 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) } break; } + case ATOMIC_WAIT: { + /* linear search: from most recent to oldest */ + action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *prev = *rit; + if (!act->same_thread(prev)&&prev->is_failed_trylock()) + return prev; + if (!act->same_thread(prev)&&prev->is_notify()) + return prev; + } + break; + } + + case ATOMIC_NOTIFY_ALL: + case ATOMIC_NOTIFY_ONE: { + /* linear search: from most recent to oldest */ + action_list_t *list = obj_map->get_safe_ptr(act->get_location()); + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) { + ModelAction *prev = *rit; + if (!act->same_thread(prev)&&prev->is_wait()) + return prev; + } + break; + } default: break; } @@ -505,6 +537,43 @@ bool ModelChecker::process_mutex(ModelAction *curr) { waiters->clear(); break; } + case ATOMIC_WAIT: { + //unlock the lock + state->islocked = false; + //wake up the other threads + action_list_t *waiters = lock_waiters_map->get_safe_ptr((void *) curr->get_value()); + //activate all the waiting threads + for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { + scheduler->wake(get_thread(*rit)); + } + waiters->clear(); + //check whether we should go to sleep or not...simulate spurious failures + if (curr->get_node()->get_misc()==0) { + condvar_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + //disable us + scheduler->sleep(get_current_thread()); + } + break; + } + case ATOMIC_NOTIFY_ALL: { + action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location()); + //activate all the waiting threads + for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) { + scheduler->wake(get_thread(*rit)); + } + waiters->clear(); + break; + } + case ATOMIC_NOTIFY_ONE: { + action_list_t *waiters = condvar_waiters_map->get_safe_ptr(curr->get_location()); + int wakeupthread=curr->get_node()->get_misc(); + action_list_t::iterator it = waiters->begin(); + advance(it, wakeupthread); + scheduler->wake(get_thread(*it)); + waiters->erase(it); + break; + } + default: ASSERT(0); } @@ -712,6 +781,11 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) compute_promises(newcurr); else if (newcurr->is_relseq_fixup()) compute_relseq_breakwrites(newcurr); + else if (newcurr->is_wait()) + newcurr->get_node()->set_misc_max(2); + else if (newcurr->is_notify_one()) { + newcurr->get_node()->set_misc_max(condvar_waiters_map->get_safe_ptr(newcurr->get_location())->size()); + } } return newcurr; } @@ -856,6 +930,7 @@ void ModelChecker::check_curr_backtracking(ModelAction * curr) { Node *parnode = currnode->get_parent(); if ((!parnode->backtrack_empty() || + !currnode->misc_empty() || !currnode->read_from_empty() || !currnode->future_value_empty() || !currnode->promise_empty() || diff --git a/model.h b/model.h index d6c0337..d0043a1 100644 --- a/model.h +++ b/model.h @@ -187,6 +187,10 @@ private: * to a trace of all actions performed on the object. */ HashTable *lock_waiters_map; + /** Per-object list of actions. Maps an object (i.e., memory location) + * to a trace of all actions performed on the object. */ + HashTable *condvar_waiters_map; + HashTable, uintptr_t, 4 > *obj_thrd_map; std::vector< Promise *, SnapshotAlloc > *promises; std::vector< struct PendingFutureValue, SnapshotAlloc > *futurevalues; diff --git a/nodestack.cc b/nodestack.cc index a850478..ec7ce16 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -34,7 +34,9 @@ Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness) future_values(), future_index(-1), relseq_break_writes(), - relseq_break_index(0) + relseq_break_index(0), + misc_index(0), + misc_max(0) { if (act) { act->set_node(this); @@ -151,6 +153,24 @@ bool Node::promise_empty() { return true; } + +void Node::set_misc_max(int i) { + misc_max=i; +} + +int Node::get_misc() { + return misc_index; +} + +bool Node::increment_misc() { + return (misc_index=misc_max; +} + + /** * Adds a value from a weakly ordered future write to backtrack to. * @param value is the value to backtrack to. diff --git a/nodestack.h b/nodestack.h index 803d2b8..1dfccfc 100644 --- a/nodestack.h +++ b/nodestack.h @@ -92,6 +92,11 @@ public: bool promise_empty(); enabled_type_t *get_enabled_array() {return enabled_array;} + void set_misc_max(int i); + int get_misc(); + bool increment_misc(); + bool misc_empty(); + void add_relseq_break(const ModelAction *write); const ModelAction * get_relseq_break(); bool increment_relseq_break(); @@ -125,6 +130,9 @@ private: std::vector< const ModelAction *, ModelAlloc > relseq_break_writes; int relseq_break_index; + + int misc_index; + int misc_max; }; typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;