From: Brian Demsky Date: Thu, 20 Sep 2012 08:20:34 +0000 (-0700) Subject: bug fixes for lock support...think it works now... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=70525635cea4c0622d30571c7028c1c293950bb5 bug fixes for lock support...think it works now... --- diff --git a/action.cc b/action.cc index e5c9afe4..3fda30de 100644 --- a/action.cc +++ b/action.cc @@ -27,6 +27,10 @@ ModelAction::~ModelAction() delete cv; } +void ModelAction::copy_from_new(ModelAction *newaction) { + seq_number=newaction->seq_number; +} + bool ModelAction::is_mutex_op() const { return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK; } @@ -180,6 +184,23 @@ bool ModelAction::is_synchronizing(const ModelAction *act) const return false; } +bool ModelAction::is_conflicting_lock(const ModelAction *act) const +{ + //Must be different threads to reorder + if (same_thread(act)) + return false; + + //Try to reorder a lock past a successful lock + if (act->is_success_lock()) + return true; + + //Try to push a successful trylock past an unlock + if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS) + return true; + + return false; +} + void ModelAction::create_cv(const ModelAction *parent) { if (cv) @@ -278,6 +299,15 @@ void ModelAction::print(void) const case ATOMIC_INIT: type_str = "init atomic"; break; + case ATOMIC_LOCK: + type_str = "lock"; + break; + case ATOMIC_UNLOCK: + type_str = "unlock"; + break; + case ATOMIC_TRYLOCK: + type_str = "trylock"; + break; default: type_str = "unknown type"; } diff --git a/action.h b/action.h index c5179bcf..f83aec95 100644 --- a/action.h +++ b/action.h @@ -72,6 +72,7 @@ public: Node * get_node() const { return node; } void set_node(Node *n) { node = n; } + void copy_from_new(ModelAction *newaction); void set_try_lock(bool obtainedlock); bool is_mutex_op() const; bool is_lock() const; @@ -91,6 +92,7 @@ public: bool is_seqcst() const; bool same_var(const ModelAction *act) const; bool same_thread(const ModelAction *act) const; + bool is_conflicting_lock(const ModelAction *act) const; bool is_synchronizing(const ModelAction *act) const; void create_cv(const ModelAction *parent = NULL); diff --git a/model.cc b/model.cc index 4f2d9e0f..02518eef 100644 --- a/model.cc +++ b/model.cc @@ -217,7 +217,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; - if (prev->is_success_lock()) + if (act->is_conflicting_lock(prev)) return prev; } } else if (type==ATOMIC_UNLOCK) { @@ -226,7 +226,7 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) action_list_t::reverse_iterator rit; for (rit = list->rbegin(); rit != list->rend(); rit++) { ModelAction *prev = *rit; - if (prev->is_failed_trylock()) + if (!act->same_thread(prev)&&prev->is_failed_trylock()) return prev; } } @@ -235,35 +235,44 @@ ModelAction * ModelChecker::get_last_conflict(ModelAction *act) void ModelChecker::set_backtracking(ModelAction *act) { - ModelAction *prev; - Node *node; Thread *t = get_thread(act); - - prev = get_last_conflict(act); + ModelAction * prev = get_last_conflict(act); if (prev == NULL) return; - node = prev->get_node()->get_parent(); - - while (!node->is_enabled(t)) - t = t->get_parent(); - - /* Check if this has been explored already */ - if (node->has_been_explored(t->get_id())) - return; + Node * node = prev->get_node()->get_parent(); - /* Cache the latest backtracking point */ - if (!priv->next_backtrack || *prev > *priv->next_backtrack) - priv->next_backtrack = prev; + int low_tid, high_tid; + if (node->is_enabled(t)) { + low_tid=id_to_int(act->get_tid()); + high_tid=low_tid+1; + } else { + low_tid=0; + high_tid=get_num_threads(); + } + + for(int i=low_tid;iis_enabled(tid)) + continue; - /* If this is a new backtracking point, mark the tree */ - if (!node->set_backtrack(t->get_id())) - return; - DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n", - prev->get_tid(), t->get_id()); - if (DBG_ENABLED()) { - prev->print(); - act->print(); + /* Check if this has been explored already */ + if (node->has_been_explored(tid)) + continue; + + /* Cache the latest backtracking point */ + if (!priv->next_backtrack || *prev > *priv->next_backtrack) + priv->next_backtrack = prev; + + /* If this is a new backtracking point, mark the tree */ + if (!node->set_backtrack(tid)) + continue; + DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n", + prev->get_tid(), t->get_id()); + if (DBG_ENABLED()) { + prev->print(); + act->print(); + } } } @@ -423,6 +432,7 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) newcurr->copy_typeandorder(curr); ASSERT(curr->get_location()==newcurr->get_location()); + newcurr->copy_from_new(curr); /* Discard duplicate ModelAction; use action from NodeStack */ delete curr; diff --git a/nodestack.cc b/nodestack.cc index b79863e2..715dbb23 100644 --- a/nodestack.cc +++ b/nodestack.cc @@ -224,6 +224,12 @@ bool Node::is_enabled(Thread *t) return thread_id < num_threads && enabled_array[thread_id]; } +bool Node::is_enabled(thread_id_t tid) +{ + int thread_id=id_to_int(tid); + return thread_id < num_threads && enabled_array[thread_id]; +} + /** * Add an action to the may_read_from set. * @param act is the action to add diff --git a/nodestack.h b/nodestack.h index 3262a569..a06bef40 100644 --- a/nodestack.h +++ b/nodestack.h @@ -56,6 +56,7 @@ public: bool set_backtrack(thread_id_t id); thread_id_t get_next_backtrack(); bool is_enabled(Thread *t); + bool is_enabled(thread_id_t tid); ModelAction * get_action() { return action; } /** @return the parent Node to this Node; that is, the action that