Reimplement hash table remove method

diff --git a/action.cc b/action.cc
index d90a94ee48211ddb17e9a3f26cafcb4e56ca9e55..9905ab2bf11bbd50e601f6157b04ee69480d99c6 100644 (file)
--- a/action.cc
+++ b/action.cc
@@ -38,6 +38,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -69,6 +70,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, uint64_t value,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -99,6 +101,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -133,6 +136,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),
@@ -168,6 +172,7 @@ ModelAction::ModelAction(action_type_t type, const char * position, memory_order
        last_fence_release(NULL),
        cv(NULL),
        rf_cv(NULL),
+       action_ref(NULL),
        value(value),
        type(type),
        order(order),

diff --git a/action.h b/action.h
index c5ba6d7dda9f9593a315a26c3d1da336a50b5a0f..fbf566fb7a8f61497284c6ab1e826dd39b0f44e0 100644 (file)
--- a/action.h
+++ b/action.h
@@ -193,6 +193,9 @@ public:
        Thread * thread_operand;
        void set_thread_operand(Thread *th) { thread_operand = th; }
 
+       void setActionRef(sllnode<ModelAction *> *ref) { action_ref = ref; }
+       sllnode<ModelAction *> * getActionRef() { return action_ref; }
+
        SNAPSHOTALLOC
 private:
        const char * get_type_str() const;
@@ -227,6 +230,7 @@ private:
         */
        ClockVector *cv;
        ClockVector *rf_cv;
+       sllnode<ModelAction *> * action_ref;
 
        /** @brief The value written (for write or RMW; undefined for read) */
        uint64_t value;

diff --git a/classlist.h b/classlist.h
index 71f545128b9257156940fe4427380c78f84ea764..e74ebcf64bdbb5aace60103095d47dcf09bfd395 100644 (file)
--- a/classlist.h
+++ b/classlist.h
@@ -29,6 +29,7 @@ class actionlist;
 struct model_snapshot_members;
 struct bug_message;
 
+typedef SnapList<ModelAction *> simple_action_list_t;
 typedef actionlist action_list_t;
 typedef SnapList<uint32_t> func_id_list_t;
 typedef SnapList<FuncInst *> func_inst_list_t;

diff --git a/execution.cc b/execution.cc
index 7f7d31c110b2e6ce9d30c844a16c63703c31f2e6..04314d194c17058713d1107911b7377b692c5a25 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -98,21 +98,31 @@ int ModelExecution::get_execution_number() const
        return model->get_execution_number();
 }
 
-static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
+static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
 {
-       action_list_t *tmp = hash->get(ptr);
+       SnapVector<action_list_t> *tmp = hash->get(ptr);
        if (tmp == NULL) {
-               tmp = new action_list_t();
+               tmp = new SnapVector<action_list_t>();
                hash->put(ptr, tmp);
        }
        return tmp;
 }
 
-static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
+static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)
 {
-       SnapVector<action_list_t> *tmp = hash->get(ptr);
+       simple_action_list_t *tmp = hash->get(ptr);
        if (tmp == NULL) {
-               tmp = new SnapVector<action_list_t>();
+               tmp = new simple_action_list_t();
+               hash->put(ptr, tmp);
+       }
+       return tmp;
+}
+
+static SnapVector<simple_action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<simple_action_list_t> *, uintptr_t, 2> * hash, void * ptr)
+{
+       SnapVector<simple_action_list_t> *tmp = hash->get(ptr);
+       if (tmp == NULL) {
+               tmp = new SnapVector<simple_action_list_t>();
                hash->put(ptr, tmp);
        }
        return tmp;
@@ -394,6 +404,8 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
                //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
                //      assert_bug("Lock access before initialization");
+
+               // TODO: lock count for recursive mutexes
                state->locked = get_thread(curr);
                ModelAction *unlock = get_last_unlock(curr);
                //synchronize with the previous unlock statement
@@ -417,8 +429,17 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                        /* unlock the lock - after checking who was waiting on it */
                        state->locked = NULL;
 
-                       /* disable this thread */
-                       get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr);
+                       /* remove old wait action and disable this thread */
+                       simple_action_list_t * waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+                       for (sllnode<ModelAction *> * it = waiters->begin(); it != NULL; it = it->getNext()) {
+                               ModelAction * wait = it->getVal();
+                               if (wait->get_tid() == curr->get_tid()) {
+                                       waiters->erase(it);
+                                       break;
+                               }
+                       }
+
+                       waiters->push_back(curr);
                        scheduler->sleep(get_thread(curr));
                }
 
@@ -435,6 +456,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                //FAILS AND IN THE CASE IT DOESN'T...  TIMED WAITS
                //MUST EVENMTUALLY RELEASE...
 
+               // TODO: lock count for recursive mutexes
                /* wake up the other threads */
                for (unsigned int i = 0;i < get_num_threads();i++) {
                        Thread *t = get_thread(int_to_id(i));
@@ -448,7 +470,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                break;
        }
        case ATOMIC_NOTIFY_ALL: {
-               action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+               simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                //activate all the waiting threads
                for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
                        scheduler->wake(get_thread(rit->getVal()));
@@ -457,7 +479,7 @@ bool ModelExecution::process_mutex(ModelAction *curr)
                break;
        }
        case ATOMIC_NOTIFY_ONE: {
-               action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
+               simple_action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
                if (waiters->size() != 0) {
                        Thread * thread = fuzzer->selectNotify(waiters);
                        scheduler->wake(thread);
@@ -682,8 +704,15 @@ bool ModelExecution::check_action_enabled(ModelAction *curr) {
        if (curr->is_lock()) {
                cdsc::mutex *lock = curr->get_mutex();
                struct cdsc::mutex_state *state = lock->get_state();
-               if (state->locked)
+               if (state->locked) {
+                       Thread *lock_owner = (Thread *)state->locked;
+                       Thread *curr_thread = get_thread(curr);
+                       if (lock_owner == curr_thread && state->type == PTHREAD_MUTEX_RECURSIVE) {
+                               return true;
+                       }
+
                        return false;
+               }
        } else if (curr->is_thread_join()) {
                Thread *blocking = curr->get_thread_operand();
                if (!blocking->is_complete()) {
@@ -1121,8 +1150,8 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
 {
        int tid = id_to_int(act->get_tid());
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
-               action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-               list->addAction(act);
+               simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+               act->setActionRef(list->add_back(act));
        }
 
        // Update action trace, a total order of all actions
@@ -1156,7 +1185,7 @@ void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
 
        if (act->is_wait()) {
                void *mutex_loc = (void *) act->get_value();
-               get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
+               act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
        }
 }
 
@@ -1202,17 +1231,15 @@ void ModelExecution::add_normal_write_to_lists(ModelAction *act)
 
 
 void ModelExecution::add_write_to_lists(ModelAction *write) {
-       SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
+       SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
        int tid = id_to_int(write->get_tid());
        if (tid >= (int)vec->size()) {
                uint oldsize =vec->size();
                vec->resize(priv->next_thread_id);
                for(uint i=oldsize;i<priv->next_thread_id;i++)
-                       new (&(*vec)[i]) action_list_t();
-
-               fixup_action_list(vec);
+                       new (&(*vec)[i]) simple_action_list_t();
        }
-       (*vec)[tid].addAction(write);
+       write->setActionRef((*vec)[tid].add_back(write));
 }
 
 /**
@@ -1268,7 +1295,7 @@ ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
 {
        /* All fences should have location FENCE_LOCATION */
-       action_list_t *list = obj_map.get(FENCE_LOCATION);
+       simple_action_list_t *list = obj_map.get(FENCE_LOCATION);
 
        if (!list)
                return NULL;
@@ -1304,7 +1331,7 @@ ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
 {
        void *location = curr->get_location();
 
-       action_list_t *list = obj_map.get(location);
+       simple_action_list_t *list = obj_map.get(location);
        if (list == NULL)
                return NULL;
 
@@ -1360,7 +1387,7 @@ bool valequals(uint64_t val1, uint64_t val2, int size) {
  */
 SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
 {
-       SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
+       SnapVector<simple_action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
        unsigned int i;
        ASSERT(curr->is_read());
 
@@ -1375,7 +1402,7 @@ SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *cu
        if (thrd_lists != NULL)
                for (i = 0;i < thrd_lists->size();i++) {
                        /* Iterate over actions in thread, starting from most recent */
-                       action_list_t *list = &(*thrd_lists)[i];
+                       simple_action_list_t *list = &(*thrd_lists)[i];
                        sllnode<ModelAction *> * rit;
                        for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
                                ModelAction *act = rit->getVal();
@@ -1677,14 +1704,23 @@ void ModelExecution::removeAction(ModelAction *act) {
                (*vec)[act->get_tid()].removeAction(act);
        }
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
-               action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-               list->removeAction(act);
+               sllnode<ModelAction *> * listref = act->getActionRef();
+               if (listref != NULL) {
+                       simple_action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+                       list->erase(listref);
+               }
        } else if (act->is_wait()) {
-               void *mutex_loc = (void *) act->get_value();
-               get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
+               sllnode<ModelAction *> * listref = act->getActionRef();
+               if (listref != NULL) {
+                       void *mutex_loc = (void *) act->get_value();
+                       get_safe_ptr_action(&obj_map, mutex_loc)->erase(listref);
+               }
        } else if (act->is_free()) {
-               SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
-               (*vec)[act->get_tid()].removeAction(act);
+               sllnode<ModelAction *> * listref = act->getActionRef();
+               if (listref != NULL) {
+                       SnapVector<simple_action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+                       (*vec)[act->get_tid()].erase(listref);
+               }
 
                //Clear it from last_sc_map
                if (obj_last_sc_map.get(act->get_location()) == act) {

diff --git a/execution.h b/execution.h
index 7ca610cad3fa7d488f29d682795f7886ff0f5943..5cd54469c6d3c920b1fda9ab7cecc54ca2de4f29 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -146,17 +146,17 @@ private:
         * to a trace of all actions performed on the object.
         * Used only for SC fences, unlocks, & wait.
         */
-       HashTable<const void *, action_list_t *, uintptr_t, 2> obj_map;
+       HashTable<const void *, simple_action_list_t *, uintptr_t, 2> 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, 2> condvar_waiters_map;
+       HashTable<const void *, simple_action_list_t *, uintptr_t, 2> condvar_waiters_map;
 
        /** Per-object list of actions that each thread performed. */
        HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> obj_thrd_map;
 
        /** Per-object list of writes that each thread performed. */
-       HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> obj_wr_thrd_map;
+       HashTable<const void *, SnapVector<simple_action_list_t> *, uintptr_t, 2> obj_wr_thrd_map;
 
        HashTable<const void *, ModelAction *, uintptr_t, 4> obj_last_sc_map;
 

diff --git a/fuzzer.cc b/fuzzer.cc
index c41af4a0466b173615a7cd2d9bb48a45c569424c..e102d9c34431a13dea089d9437857640e2691cfd 100644 (file)
--- a/fuzzer.cc
+++ b/fuzzer.cc
@@ -16,14 +16,14 @@ Thread * Fuzzer::selectThread(int * threadlist, int numthreads) {
        return model->get_thread(curr_tid);
 }
 
-Thread * Fuzzer::selectNotify(action_list_t * waiters) {
+Thread * Fuzzer::selectNotify(simple_action_list_t * waiters) {
        int numwaiters = waiters->size();
        int random_index = random() % numwaiters;
        sllnode<ModelAction*> * it = waiters->begin();
        while(random_index--)
                it=it->getNext();
        Thread *thread = model->get_thread(it->getVal());
-       waiters->removeAction(it->getVal());
+       waiters->erase(it);
        return thread;
 }
 
@@ -41,5 +41,5 @@ bool Fuzzer::shouldWake(const ModelAction *sleep) {
 
 bool Fuzzer::shouldWait(const ModelAction * act)
 {
-       return random() & 1;
+       return true;
 }

diff --git a/fuzzer.h b/fuzzer.h
index 14dff6e023ddbbf174f1a129378bee7a55b72f55..0fcfb51f67e66ff9ee439f9b48c1bd860838cbfa 100644 (file)
--- a/fuzzer.h
+++ b/fuzzer.h
@@ -12,7 +12,7 @@ public:
        virtual bool has_paused_threads() { return false; }
        virtual Thread * selectThread(int * threadlist, int numthreads);
 
-       Thread * selectNotify(action_list_t * waiters);
+       Thread * selectNotify(simple_action_list_t * waiters);
        bool shouldSleep(const ModelAction *sleep);
        bool shouldWake(const ModelAction *sleep);
        virtual bool shouldWait(const ModelAction *wait);

diff --git a/hashtable.h b/hashtable.h
index 81772a8f039addae09c726c0f7bf3e37ab626ef1..b7cac67410c287004e9861d14db91c4afc0367dd 100644 (file)
--- a/hashtable.h
+++ b/hashtable.h
@@ -258,6 +258,7 @@ public:
         */
        _Val remove(_Key key) {
                struct hashlistnode<_Key, _Val> *search;
+               struct hashlistnode<_Key, _Val> *replace;
 
                /* HashTable cannot handle 0 as a key */
                if (!key) {
@@ -280,14 +281,40 @@ public:
                        if (!search->key) {
                                if (!search->val)
                                        break;
-                       } else
-                       if (equals(search->key, key)) {
-                               _Val v=search->val;
-                               //empty out this bin
-                               search->val=(_Val) 1;
-                               search->key=0;
-                               size--;
-                               return v;
+                       } else {
+                               // The case where an item is found
+                               if (equals(search->key, key)) {
+                                       unsigned int j = index;
+                                       _Val v = search->val;
+                                       size--;
+
+                                       // Idea: keep bins contiguous
+                                       while (true) {
+                                               search->val = 0;
+                                               search->key = 0;
+
+                                               while (true) {
+                                                       j = (j + 1) & capacitymask;
+                                                       replace = &table[j];
+
+                                                       if (!replace->key && !replace->val) {
+                                                               return v;
+                                                       }
+
+                                                       unsigned int hash = hash_function(replace->key) & capacitymask;
+                                                       if (index <= j && index < hash && hash <= j)
+                                                               continue;
+                                                       else if (index > j && (index < hash || hash <= j) )
+                                                               continue;
+                                                       else
+                                                               break;
+                                               }
+
+                                               table[index] = table[j];
+                                               index = j;
+                                               search = &table[index];
+                                       }
+                               }
                        }
                        index++;
                } while (true);

diff --git a/include/mutex.h b/include/mutex.h
index f5894952282be7024867a8880793383f82b8e5f7..1f573bd1e51dd128e0b5b8982aa113f5f70a212c 100644 (file)
--- a/include/mutex.h
+++ b/include/mutex.h
@@ -8,17 +8,20 @@
 
 #include "modeltypes.h"
 #include "mymemory.h"
+#include "mypthread.h"
 
 namespace cdsc {
 struct mutex_state {
        void *locked;   /* Thread holding the lock */
        thread_id_t alloc_tid;
        modelclock_t alloc_clock;
+       int type;
+       int lock_count;
 };
 
 class mutex {
 public:
-       mutex();
+       mutex(int type = PTHREAD_MUTEX_DEFAULT);
        ~mutex() {}
        void lock();
        bool try_lock();
@@ -31,7 +34,7 @@ private:
 
 class snapmutex : public mutex {
 public:
-       snapmutex() : mutex()
+       snapmutex(int type = 0) : mutex(type)
        { }
        SNAPSHOTALLOC
 };

diff --git a/include/mypthread.h b/include/mypthread.h
index 4b2b615f61f9b1c0bcd0f64311e1edacd05824e1..660a8197e5084ca920cf46c99762915dafd62f15 100644 (file)
--- a/include/mypthread.h
+++ b/include/mypthread.h
@@ -9,6 +9,15 @@
 #include <sched.h>
 #include <pthread.h>
 
+/* pthread mutex types
+enum
+{
+  PTHREAD_MUTEX_NORMAL
+  PTHREAD_MUTEX_RECURSIVE
+  PTHREAD_MUTEX_ERRORCHECK
+  PTHREAD_MUTEX_DEFAULT
+};*/
+
 typedef void *(*pthread_start_t)(void *);
 
 struct pthread_params {

diff --git a/mutex.cc b/mutex.cc
index 0776db8eef5857b34c47bdbf3493194c9672097a..10fb5e3248b0550dd8b18afea34164380306ff23 100644 (file)
--- a/mutex.cc
+++ b/mutex.cc
@@ -8,13 +8,17 @@
 
 namespace cdsc {
 
-mutex::mutex()
+mutex::mutex(int type)
 {
        state.locked = NULL;
        thread_id_t tid = thread_current()->get_id();
        state.alloc_tid = tid;
        ClockVector *cv = model->get_execution()->get_cv(tid);
        state.alloc_clock = cv  == NULL ? 0 : cv->getClock(tid);
+
+       // For recursive mutex
+       state.type = type;
+       state.lock_count = 0;
 }
 
 void mutex::lock()

diff --git a/newfuzzer.h b/newfuzzer.h
index 45a7e8bbe91f44f867e22958502491ffb64b4fa6..26fab3f6c2fff4e0ed995e4d68a8dd7733ecb5f5 100644 (file)
--- a/newfuzzer.h
+++ b/newfuzzer.h
@@ -29,7 +29,7 @@ public:
        void notify_paused_thread(Thread * thread);
 
        Thread * selectThread(int * threadlist, int numthreads);
-       Thread * selectNotify(action_list_t * waiters);
+       Thread * selectNotify(simple_action_list_t * waiters);
        bool shouldSleep(const ModelAction * sleep);
        bool shouldWake(const ModelAction * sleep);
        bool shouldWait(const ModelAction * wait);

diff --git a/pthread.cc b/pthread.cc
index 706f1b75602ef6ae33e2876be5064dcd10ab18a3..50214c34b31d6d578e4d732c11865eab9b3a3a89 100644 (file)
--- a/pthread.cc
+++ b/pthread.cc
@@ -66,13 +66,18 @@ void pthread_exit(void *value_ptr) {
        real_pthread_exit(NULL);
 }
 
-int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t *) {
+int pthread_mutex_init(pthread_mutex_t *p_mutex, const pthread_mutexattr_t * attr) {
        if (!model) {
                snapshot_system_init(10000, 1024, 1024, 40000);
                model = new ModelChecker();
                model->startChecker();
        }
-       cdsc::snapmutex *m = new cdsc::snapmutex();
+
+       int mutex_type = PTHREAD_MUTEX_DEFAULT;
+       if (attr != NULL)
+               pthread_mutexattr_gettype(attr, &mutex_type);
+
+       cdsc::snapmutex *m = new cdsc::snapmutex(mutex_type);
 
        ModelExecution *execution = model->get_execution();
        execution->getMutexMap()->put(p_mutex, m);

diff --git a/threads.cc b/threads.cc
index a2d2ed166ba3350400e6e5c13cb9b897fdad628a..a576697f561087fe2c09c607e44ef02bb0c6fa8c 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -496,6 +496,14 @@ Thread * Thread::waiting_on() const
 bool Thread::is_waiting_on(const Thread *t) const
 {
        Thread *wait;
+
+       // One thread relocks a recursive mutex
+       if (waiting_on() == t && pending->is_lock()) {
+               int mutex_type = pending->get_mutex()->get_state()->type;
+               if (mutex_type == PTHREAD_MUTEX_RECURSIVE)
+                       return false;
+       }
+
        for (wait = waiting_on();wait != NULL;wait = wait->waiting_on())
                if (wait == t)
                        return true;