Use simple_action_list for conditionvariable waiters

diff --combined classlist.h
index ccbbbb1418a9ca785394e41df2480f24f22a923d,71f545128b9257156940fe4427380c78f84ea764..e74ebcf64bdbb5aace60103095d47dcf09bfd395
--- 1/classlist.h
--- 2/classlist.h
+++ b/classlist.h
@@@ -22,11 -22,14 +22,15 @@@ class FuncInst
  class Predicate;
  class ConcretePredicate;
  class WaitObj;
+ class actionlist;
+ 
+ #include "actionlist.h"
  
  struct model_snapshot_members;
  struct bug_message;
  
- typedef SnapList<ModelAction *> action_list_t;
++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 --combined execution.cc
index 48c73cfbeca2db10dd19148062bded4bfd9858e7,c37de41a1f14fb032c0ab85fe28064426cb943a1..9c3b4afa2986fac9ecce604e9de9394ebca6f3eb
--- 1/execution.cc
--- 2/execution.cc
+++ b/execution.cc
@@@ -118,6 -118,6 +118,16 @@@ static SnapVector<action_list_t> * get_
        return tmp;
  }
  
++static simple_action_list_t * get_safe_ptr_action(HashTable<const void *, simple_action_list_t *, uintptr_t, 2> * hash, void * ptr)
++{
++      simple_action_list_t *tmp = hash->get(ptr);
++      if (tmp == NULL) {
++              tmp = new simple_action_list_t();
++              hash->put(ptr, tmp);
++      }
++      return tmp;
++}
++
  /** @return a thread ID for a new Thread */
  thread_id_t ModelExecution::get_next_id()
  {
@@@ -329,6 -329,10 +339,10 @@@ bool ModelExecution::process_read(Model
                        read_from(curr, rf);
                        get_thread(curr)->set_return_value(curr->get_return_value());
                        delete priorset;
+                       //Update acquire fence clock vector
+                       ClockVector * hbcv = get_hb_from_write(curr->get_reads_from());
+                       if (hbcv != NULL)
+                               get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
                        return canprune && (curr->get_type() == ATOMIC_READ);
                }
                priorset->clear();
@@@ -376,8 -380,6 +390,8 @@@ bool ModelExecution::process_mutex(Mode
                //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
@@@ -401,17 -403,8 +415,17 @@@
                        /* 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 */
-                       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());
 +                      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));
                }
  
@@@ -428,7 -421,6 +442,7 @@@
                //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));
@@@ -442,7 -434,7 +456,7 @@@
                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()));
@@@ -451,7 -443,7 +465,7 @@@
                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);
@@@ -481,7 -473,7 +495,7 @@@ void ModelExecution::process_write(Mode
   * @param curr The ModelAction to process
   * @return True if synchronization was updated
   */
- bool ModelExecution::process_fence(ModelAction *curr)
+ void ModelExecution::process_fence(ModelAction *curr)
  {
        /*
         * fence-relaxed: no-op
@@@ -491,36 -483,9 +505,9 @@@
         *   sequences
         * fence-seq-cst: MO constraints formed in {r,w}_modification_order
         */
-       bool updated = false;
        if (curr->is_acquire()) {
-               action_list_t *list = &action_trace;
-               sllnode<ModelAction *> * rit;
-               /* Find X : is_read(X) && X --sb-> curr */
-               for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
-                       ModelAction *act = rit->getVal();
-                       if (act == curr)
-                               continue;
-                       if (act->get_tid() != curr->get_tid())
-                               continue;
-                       /* Stop at the beginning of the thread */
-                       if (act->is_thread_start())
-                               break;
-                       /* Stop once we reach a prior fence-acquire */
-                       if (act->is_fence() && act->is_acquire())
-                               break;
-                       if (!act->is_read())
-                               continue;
-                       /* read-acquire will find its own release sequences */
-                       if (act->is_acquire())
-                               continue;
- 
-                       /* Establish hypothetical release sequences */
-                       ClockVector *cv = get_hb_from_write(act->get_reads_from());
-                       if (cv != NULL && curr->get_cv()->merge(cv))
-                               updated = true;
-               }
+               curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
        }
-       return updated;
  }
  
  /**
@@@ -703,15 -668,8 +690,15 @@@ bool ModelExecution::check_action_enabl
        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()) {
@@@ -1148,11 -1106,11 +1135,11 @@@ void ModelExecution::add_action_to_list
        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());
-               act->setActionRef(list->add_back(act));
+               list->addAction(act);
        }
  
        // Update action trace, a total order of all actions
-       act->setTraceRef(action_trace.add_back(act));
+       action_trace.addAction(act);
  
  
        // Update obj_thrd_map, a per location, per thread, order of actions
@@@ -1164,7 -1122,7 +1151,7 @@@
                        new (&(*vec)[i]) action_list_t();
        }
        if (!canprune && (act->is_read() || act->is_write()))
-               act->setThrdMapRef((*vec)[tid].add_back(act));
+               (*vec)[tid].addAction(act);
  
        // Update thrd_last_action, the last action taken by each thread
        if ((int)thrd_last_action.size() <= tid)
@@@ -1180,43 -1138,17 +1167,17 @@@
  
        if (act->is_wait()) {
                void *mutex_loc = (void *) act->get_value();
-               act->setActionRef(get_safe_ptr_action(&obj_map, mutex_loc)->add_back(act));
+               get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
        }
  }
  
- sllnode<ModelAction *>* insertIntoActionList(action_list_t *list, ModelAction *act) {
-       sllnode<ModelAction*> * rit = list->end();
-       modelclock_t next_seq = act->get_seq_number();
-       if (rit == NULL || (rit->getVal()->get_seq_number() <= next_seq))
-               return list->add_back(act);
-       else {
-               for(;rit != NULL;rit=rit->getPrev()) {
-                       if (rit->getVal()->get_seq_number() <= next_seq) {
-                               return list->insertAfter(rit, act);
-                       }
-               }
-               return list->add_front(act);
-       }
+ void insertIntoActionList(action_list_t *list, ModelAction *act) {
+       list->addAction(act);
  }
  
- sllnode<ModelAction *>* insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
-       sllnode<ModelAction*> * rit = list->end();
-       modelclock_t next_seq = act->get_seq_number();
-       if (rit == NULL) {
-               act->create_cv(NULL);
-               return list->add_back(act);
-       } else if (rit->getVal()->get_seq_number() <= next_seq) {
-               act->create_cv(rit->getVal());
-               return list->add_back(act);
-       } else {
-               for(;rit != NULL;rit=rit->getPrev()) {
-                       if (rit->getVal()->get_seq_number() <= next_seq) {
-                               act->create_cv(rit->getVal());
-                               return list->insertAfter(rit, act);
-                       }
-               }
-               return list->add_front(act);
-       }
+ void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
+       act->create_cv(NULL);
+       list->addAction(act);
  }
  
  /**
@@@ -1230,7 -1162,7 +1191,7 @@@
  void ModelExecution::add_normal_write_to_lists(ModelAction *act)
  {
        int tid = id_to_int(act->get_tid());
-       act->setTraceRef(insertIntoActionListAndSetCV(&action_trace, act));
+       insertIntoActionListAndSetCV(&action_trace, act);
  
        // Update obj_thrd_map, a per location, per thread, order of actions
        SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
@@@ -1240,7 -1172,7 +1201,7 @@@
                for(uint i=oldsize;i<priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       act->setThrdMapRef(insertIntoActionList(&(*vec)[tid],act));
+       insertIntoActionList(&(*vec)[tid],act);
  
        ModelAction * lastact = thrd_last_action[tid];
        // Update thrd_last_action, the last action taken by each thrad
@@@ -1258,7 -1190,7 +1219,7 @@@ void ModelExecution::add_write_to_lists
                for(uint i=oldsize;i<priv->next_thread_id;i++)
                        new (&(*vec)[i]) action_list_t();
        }
-       write->setActionRef((*vec)[tid].add_back(write));
+       (*vec)[tid].addAction(write);
  }
  
  /**
@@@ -1561,7 -1493,7 +1522,7 @@@ void ModelExecution::print_tail(
        int length = 25;
        int counter = 0;
        SnapList<ModelAction *> list;
-       for (it = action_trace.end(); it != NULL; it = it->getPrev()) {
+       for (it = action_trace.end();it != NULL;it = it->getPrev()) {
                if (counter > length)
                        break;
  
@@@ -1716,36 -1648,22 +1677,22 @@@ Thread * ModelExecution::take_step(Mode
  
  void ModelExecution::removeAction(ModelAction *act) {
        {
-               sllnode<ModelAction *> * listref = act->getTraceRef();
-               if (listref != NULL) {
-                       action_trace.erase(listref);
-               }
+               action_trace.removeAction(act);
        }
        {
-               sllnode<ModelAction *> * listref = act->getThrdMapRef();
-               if (listref != NULL) {
-                       SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
-                       (*vec)[act->get_tid()].erase(listref);
-               }
+               SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
+               (*vec)[act->get_tid()].removeAction(act);
        }
        if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
-               sllnode<ModelAction *> * listref = act->getActionRef();
-               if (listref != NULL) {
-                       action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
-                       list->erase(listref);
-               }
+               action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
+               list->removeAction(act);
        } else if (act->is_wait()) {
-               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);
-               }
+               void *mutex_loc = (void *) act->get_value();
+               get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
        } else if (act->is_free()) {
-               sllnode<ModelAction *> * listref = act->getActionRef();
-               if (listref != NULL) {
-                       SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
-                       (*vec)[act->get_tid()].erase(listref);
-               }
+               SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
+               (*vec)[act->get_tid()].removeAction(act);
+ 
                //Clear it from last_sc_map
                if (obj_last_sc_map.get(act->get_location()) == act) {
                        obj_last_sc_map.remove(act->get_location());

diff --combined execution.h
index 722b864723a40f8d902c5ed2920575d43b837b01,7ca610cad3fa7d488f29d682795f7886ff0f5943..0c401b19b59084609a2fe12b1cbb565a736cfbac
--- 1/execution.h
--- 2/execution.h
+++ b/execution.h
@@@ -19,8 -19,6 +19,6 @@@
  #include <condition_variable>
  #include "classlist.h"
  
- typedef SnapList<ModelAction *> action_list_t;
- 
  struct PendingFutureValue {
        PendingFutureValue(ModelAction *writer, ModelAction *reader) :
                writer(writer), reader(reader)
@@@ -105,7 -103,7 +103,7 @@@ private
        bool initialize_curr_action(ModelAction **curr);
        bool process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set);
        void process_write(ModelAction *curr);
-       bool process_fence(ModelAction *curr);
+       void process_fence(ModelAction *curr);
        bool process_mutex(ModelAction *curr);
        void process_thread_action(ModelAction *curr);
        void read_from(ModelAction *act, ModelAction *rf);
@@@ -152,7 -150,7 +150,7 @@@
  
        /** 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;

diff --combined fuzzer.cc
index 371838dcb1977c912a346a7a995e4e9cc3083425,c41af4a0466b173615a7cd2d9bb48a45c569424c..e102d9c34431a13dea089d9437857640e2691cfd
--- 1/fuzzer.cc
--- 2/fuzzer.cc
+++ b/fuzzer.cc
@@@ -16,14 -16,14 +16,14 @@@ Thread * Fuzzer::selectThread(int * thr
        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 +41,5 @@@ bool Fuzzer::shouldWake(const ModelActi
  
  bool Fuzzer::shouldWait(const ModelAction * act)
  {
--      return random() & 1;
++      return true;
  }

diff --combined fuzzer.h
index 14dff6e023ddbbf174f1a129378bee7a55b72f55,14dff6e023ddbbf174f1a129378bee7a55b72f55..0fcfb51f67e66ff9ee439f9b48c1bd860838cbfa
--- 1/fuzzer.h
--- 2/fuzzer.h
+++ b/fuzzer.h
@@@ -12,7 -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 --combined newfuzzer.h
index 45a7e8bbe91f44f867e22958502491ffb64b4fa6,45a7e8bbe91f44f867e22958502491ffb64b4fa6..26fab3f6c2fff4e0ed995e4d68a8dd7733ecb5f5
--- 1/newfuzzer.h
--- 2/newfuzzer.h
+++ b/newfuzzer.h
@@@ -29,7 -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 --combined threads.cc
index ee0df19ca338bd20e2a3dc0e4bd85b00ab059354,a2d2ed166ba3350400e6e5c13cb9b897fdad628a..a576697f561087fe2c09c607e44ef02bb0c6fa8c
--- 1/threads.cc
--- 2/threads.cc
+++ b/threads.cc
@@@ -14,6 -14,7 +14,7 @@@
  #include "model.h"
  #include "execution.h"
  #include "schedule.h"
+ #include "clockvector.h"
  
  #ifdef TLS
  #include <dlfcn.h>
@@@ -359,6 -360,7 +360,7 @@@ void Thread::complete(
   */
  Thread::Thread(thread_id_t tid) :
        parent(NULL),
+       acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
        start_routine(NULL),
@@@ -384,6 -386,7 +386,7 @@@
   */
  Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread *parent) :
        parent(parent),
+       acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
        start_routine(func),
@@@ -416,6 -419,7 +419,7 @@@
   */
  Thread::Thread(thread_id_t tid, thrd_t *t, void *(*func)(void *), void *a, Thread *parent) :
        parent(parent),
+       acq_fence_cv(new ClockVector()),
        creation(NULL),
        pending(NULL),
        start_routine(NULL),
@@@ -444,6 -448,8 +448,8 @@@ Thread::~Thread(
  {
        if (!is_complete())
                complete();
+ 
+       delete acq_fence_cv;
  }
  
  /** @return The thread_id_t corresponding to this Thread object. */
@@@ -490,14 -496,6 +496,14 @@@ Thread * Thread::waiting_on() cons
  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;