support for locks... untested, but doesn't break quick run of a sample of test cases

diff --git a/action.cc b/action.cc
index bf55d0091a2fdb368f5a2caf9727c3f2aab61d6f..f7ca249f965e6b351cd9763f382f9c792d586182 100644 (file)
--- 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 753860984a2f2df79869deb11bb0053fdb05d7a5..c5179bcfa81a77de58b79b5c57077a28d32cfb24 100644 (file)
--- 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 c57ddeea13a28ce1ff1a1bad5a72a6ef9353830d..651d32d5b9c7bf74a63bbfda817419009a1e6049 100644 (file)
--- 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<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>()),
        obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
        promises(new std::vector<Promise *>()),
        futurevalues(new std::vector<struct PendingFutureValue>()),
@@ -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 fd6e6c234f1c4d55e9a9a17ac652484f28be53b2..8d10d51e7e2138904ae415cf8fa11c06c959765e 100644 (file)
--- 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<const void *, action_list_t, uintptr_t, 4> *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<const void *, action_list_t, uintptr_t, 4> *lock_waiters_map;
+
        HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 > *obj_thrd_map;
        std::vector<Promise *> *promises;
        std::vector<struct PendingFutureValue> *futurevalues;

diff --git a/mutex.cc b/mutex.cc
index b31b20a8ed2f02446fd1c4fbea5965c65b2b6979..2cf6828af0ac679811d0fe7cac42d57502fe60d9 100644 (file)
--- 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 1c6c3f3624fc1f9f31b4fa8331a756ea1eebee34..a65250b542fafd68a28ab089131d0a4937694784 100644 (file)
--- 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 7fa4507ee94397e7e092730567901de94cf07a46..39f049541d69184cc012bcd042f2400208863a3a 100644 (file)
--- 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 87a21ef2633f46f14de70240f052bc50af2adcce..9456a22f2fe4942b1004a87794fa3474eaeab26b 100644 (file)
--- 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;