From ffc110b3aaa80564dbf85f3c6a9049efd40571f1 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Thu, 11 Oct 2012 22:51:45 -0700
Subject: [PATCH] commit untested condvar code
---
action.cc | 18 +++++++++++-
action.h | 3 ++
model.cc | 77 +++++++++++++++++++++++++++++++++++++++++++++++++++-
model.h | 4 +++
nodestack.cc | 22 ++++++++++++++-
nodestack.h | 8 ++++++
6 files changed, 129 insertions(+), 3 deletions(-)
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<int, Thread *, int>()),
obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
lock_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
+ condvar_waiters_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
@@ -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<const void *, action_list_t, uintptr_t, 4> *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<const void *, action_list_t, uintptr_t, 4> *condvar_waiters_map;
+
HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 > *obj_thrd_map;
std::vector< Promise *, SnapshotAlloc<Promise *> > *promises;
std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> > *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)&&((++misc_index)<misc_max);
+}
+
+bool Node::misc_empty() {
+ return (misc_index+1)>=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<const ModelAction *> > relseq_break_writes;
int relseq_break_index;
+
+ int misc_index;
+ int misc_max;
};
typedef std::vector< Node *, ModelAlloc< Node * > > node_list_t;
--
2.34.1