From 9ba28a8ef15225525c30c5303c859f64602820a3 Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 19 Sep 2012 16:09:19 -0700 Subject: [PATCH] support for locks... untested, but doesn't break quick run of a sample of test cases --- action.cc | 23 +++++++++++++ action.h | 5 +++ model.cc | 99 ++++++++++++++++++++++++++++++++++++++++++++++++++---- model.h | 7 ++++ mutex.cc | 6 ++-- mutex.h | 9 +++-- threads.cc | 1 + threads.h | 3 ++ 8 files changed, 141 insertions(+), 12 deletions(-) diff --git a/action.cc b/action.cc index bf55d00..f7ca249 100644 --- a/action.cc +++ b/action.cc @@ -27,6 +27,22 @@ ModelAction::~ModelAction() delete cv; } +bool ModelAction::is_mutex_op() const { + return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK; +} + +bool ModelAction::is_lock() const { + return type == ATOMIC_LOCK; +} + +bool ModelAction::is_unlock() const { + return type == ATOMIC_UNLOCK; +} + +bool ModelAction::is_trylock() const { + return type == ATOMIC_TRYLOCK; +} + bool ModelAction::is_success_lock() const { return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS); } @@ -175,6 +191,13 @@ void ModelAction::create_cv(const ModelAction *parent) cv = new ClockVector(NULL, this); } +void ModelAction::set_try_lock(bool obtainedlock) { + if (obtainedlock) + value=VALUE_TRYSUCCESS; + else + value=VALUE_TRYFAILED; +} + /** Update the model action's read_from action */ void ModelAction::read_from(const ModelAction *act) { diff --git a/action.h b/action.h index 7538609..c5179bc 100644 --- a/action.h +++ b/action.h @@ -72,6 +72,11 @@ public: Node * get_node() const { return node; } void set_node(Node *n) { node = n; } + void set_try_lock(bool obtainedlock); + bool is_mutex_op() const; + bool is_lock() const; + bool is_trylock() const; + bool is_unlock() const; bool is_success_lock() const; bool is_failed_trylock() const; bool is_read() const; diff --git a/model.cc b/model.cc index c57ddee..651d32d 100644 --- a/model.cc +++ b/model.cc @@ -11,6 +11,7 @@ #include "cyclegraph.h" #include "promise.h" #include "datarace.h" +#include "mutex.h" #define INITIAL_THREAD_ID 0 @@ -27,6 +28,7 @@ ModelChecker::ModelChecker(struct model_params params) : action_trace(new action_list_t()), thread_map(new HashTable()), obj_map(new HashTable()), + lock_waiters_map(new HashTable()), obj_thrd_map(new HashTable, uintptr_t, 4 >()), promises(new std::vector()), futurevalues(new std::vector()), @@ -55,6 +57,7 @@ ModelChecker::~ModelChecker() delete obj_thrd_map; delete obj_map; + delete lock_waiters_map; delete action_trace; for (unsigned int i = 0; i < promises->size(); i++) @@ -118,12 +121,14 @@ Thread * ModelChecker::get_next_thread(ModelAction *curr) { thread_id_t tid; - /* Do not split atomic actions. */ - if (curr->is_rmwr()) - return thread_current(); - /* The THREAD_CREATE action points to the created Thread */ - else if (curr->get_type() == THREAD_CREATE) - return (Thread *)curr->get_location(); + if (curr!=NULL) { + /* Do not split atomic actions. */ + if (curr->is_rmwr()) + return thread_current(); + /* The THREAD_CREATE action points to the created Thread */ + else if (curr->get_type() == THREAD_CREATE) + return (Thread *)curr->get_location(); + } /* Have we completed exploring the preselected path? */ if (diverge == NULL) @@ -320,6 +325,42 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) } } +void ModelChecker::process_mutex(ModelAction *curr) { + std::mutex * mutex=(std::mutex *) curr->get_location(); + struct std::mutex_state * state=mutex->get_state(); + switch(curr->get_type()) { + case ATOMIC_TRYLOCK: { + bool success=!state->islocked; + curr->set_try_lock(success); + if (!success) + break; + } + //otherwise fall into the lock case + case ATOMIC_LOCK: { + state->islocked=true; + ModelAction *unlock=get_last_unlock(curr); + //synchronize with the previous unlock statement + curr->synchronize_with(unlock); + break; + } + case ATOMIC_UNLOCK: { + //unlock the lock + state->islocked=false; + //wake up the other threads + action_list_t * waiters = lock_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++) { + add_thread(get_thread((*rit)->get_tid())); + } + waiters->clear(); + break; + } + default: + ASSERT(0); + } +} + + /** * Process a write ModelAction * @param curr The ModelAction to process @@ -393,6 +434,20 @@ ModelAction * ModelChecker::initialize_curr_action(ModelAction *curr) return newcurr; } +bool ModelChecker::check_action_enabled(ModelAction *curr) { + if (curr->is_lock()) { + std::mutex * lock=(std::mutex *) curr->get_location(); + struct std::mutex_state * state = lock->get_state(); + if (state->islocked) { + //Stick the action in the appropriate waiting queue + lock_waiters_map->get_safe_ptr(curr->get_location())->push_back(curr); + return false; + } + } + + return true; +} + /** * This is the heart of the model checker routine. It performs model-checking * actions corresponding to a given "current action." Among other processes, it @@ -411,6 +466,14 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw(); + if (!check_action_enabled(curr)) { + //we'll make the execution look like we chose to run this action + //much later...when a lock is actually available to relese + remove_thread(get_current_thread()); + get_current_thread()->set_pending(curr); + return get_next_thread(NULL); + } + ModelAction *newcurr = initialize_curr_action(curr); /* Add the action to lists before any other model-checking tasks */ @@ -476,6 +539,9 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_write() && process_write(act)) updated = true; + if (act->is_mutex_op()) + process_mutex(act); + if (updated) work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); break; @@ -1181,6 +1247,18 @@ ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) return NULL; } +ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) +{ + void *location = curr->get_location(); + action_list_t *list = obj_map->get_safe_ptr(location); + /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */ + action_list_t::reverse_iterator rit; + for (rit = list->rbegin(); rit != list->rend(); rit++) + if ((*rit)->is_unlock()) + return *rit; + return NULL; +} + ModelAction * ModelChecker::get_parent_action(thread_id_t tid) { ModelAction *parent = get_last_action(tid); @@ -1443,6 +1521,15 @@ bool ModelChecker::take_step() { /* next == NULL -> don't take any more steps */ if (!next) return false; + + if ( next->get_pending() != NULL ) { + //restart a pending action + set_current_action(next->get_pending()); + next->set_pending(NULL); + next->set_state(THREAD_READY); + return true; + } + /* Return false only if swap fails with an error */ return (Thread::swap(&system_context, next) == 0); } diff --git a/model.h b/model.h index fd6e6c2..8d10d51 100644 --- a/model.h +++ b/model.h @@ -117,6 +117,8 @@ private: ModelAction * initialize_curr_action(ModelAction *curr); bool process_read(ModelAction *curr, bool second_part_of_rmw); bool process_write(ModelAction *curr); + void process_mutex(ModelAction *curr); + bool check_action_enabled(ModelAction *curr); bool take_step(); @@ -133,6 +135,7 @@ private: void add_action_to_lists(ModelAction *act); ModelAction * get_last_action(thread_id_t tid); ModelAction * get_last_seq_cst(ModelAction *curr); + ModelAction * get_last_unlock(ModelAction *curr); void build_reads_from_past(ModelAction *curr); ModelAction * process_rmw(ModelAction *curr); void post_r_modification_order(ModelAction *curr, const ModelAction *rf); @@ -152,6 +155,10 @@ private: * to a trace of all actions performed on the object. */ HashTable *obj_map; + /** Per-object list of actions. Maps an object (i.e., memory location) + * to a trace of all actions performed on the object. */ + HashTable *lock_waiters_map; + HashTable, uintptr_t, 4 > *obj_thrd_map; std::vector *promises; std::vector *futurevalues; diff --git a/mutex.cc b/mutex.cc index b31b20a..2cf6828 100644 --- a/mutex.cc +++ b/mutex.cc @@ -3,10 +3,8 @@ namespace std { -mutex::mutex() : - owner(0), islocked(false) -{ - +mutex::mutex() { + state.islocked=false; } void mutex::lock() { diff --git a/mutex.h b/mutex.h index 1c6c3f3..a65250b 100644 --- a/mutex.h +++ b/mutex.h @@ -3,6 +3,10 @@ #include "threads.h" namespace std { + struct mutex_state { + bool islocked; + }; + class mutex { public: mutex(); @@ -10,9 +14,10 @@ namespace std { void lock(); bool try_lock(); void unlock(); + struct mutex_state * get_state() {return &state;} + private: - thread_id_t owner; - bool islocked; + struct mutex_state state; }; } #endif diff --git a/threads.cc b/threads.cc index 7fa4507..39f0495 100644 --- a/threads.cc +++ b/threads.cc @@ -119,6 +119,7 @@ void Thread::complete() * @param a The parameter to pass to this function. */ Thread::Thread(thrd_t *t, void (*func)(void *), void *a) : + pending(NULL), start_routine(func), arg(a), user_thread(t), diff --git a/threads.h b/threads.h index 87a21ef..9456a22 100644 --- a/threads.h +++ b/threads.h @@ -84,6 +84,8 @@ public: */ void push_wait_list(ModelAction *act) { wait_list.push_back(act); } + ModelAction * get_pending() { return pending; } + void set_pending(ModelAction *act) { pending = act; } /** * Remove one ModelAction from the waiting list * @return The ModelAction that was removed from the waiting list @@ -102,6 +104,7 @@ private: Thread *parent; ModelAction *creation; + ModelAction *pending; void (*start_routine)(void *); void *arg; ucontext_t context; -- 2.34.1