Do not report deadlock on relocking a recursive mutex; lock count not implemented yet
[c11tester.git] / execution.cc
index a98567edb9ba7b723c474405cbb5d3d75433687a..d455b5161e988fa3fe9ef00da1402a9782b6409b 100644 (file)
@@ -53,7 +53,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
        scheduler(scheduler),
        thread_map(2),  /* We'll always need at least 2 threads */
        pthread_map(0),
-       pthread_counter(1),
+       pthread_counter(2),
        action_trace(),
        obj_map(),
        condvar_waiters_map(),
@@ -376,6 +376,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,6 +419,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));
@@ -691,8 +694,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()) {
@@ -1527,6 +1537,40 @@ void ModelExecution::print_summary()
 
 }
 
+void ModelExecution::print_tail()
+{
+       model_print("Execution trace %d:\n", get_execution_number());
+
+       sllnode<ModelAction*> *it;
+
+       model_print("------------------------------------------------------------------------------------\n");
+       model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
+       model_print("------------------------------------------------------------------------------------\n");
+
+       unsigned int hash = 0;
+
+       int length = 25;
+       int counter = 0;
+       SnapList<ModelAction *> list;
+       for (it = action_trace.end(); it != NULL; it = it->getPrev()) {
+               if (counter > length)
+                       break;
+
+               ModelAction * act = it->getVal();
+               list.push_front(act);
+               counter++;
+       }
+
+       for (it = list.begin();it != NULL;it=it->getNext()) {
+               const ModelAction *act = it->getVal();
+               if (act->get_seq_number() > 0)
+                       act->print();
+               hash = hash^(hash<<3)^(it->getVal()->hash());
+       }
+       model_print("HASH %u\n", hash);
+       model_print("------------------------------------------------------------------------------------\n");
+}
+
 /**
  * Add a Thread to the system for the first time. Should only be called once
  * per thread.
@@ -1571,14 +1615,21 @@ Thread * ModelExecution::get_thread(const ModelAction *act) const
  * @return A Thread reference
  */
 Thread * ModelExecution::get_pthread(pthread_t pid) {
+       // pid 1 is reserved for the main thread, pthread ids should start from 2
+       if (pid == 1)
+               return get_thread(pid);
+
        union {
                pthread_t p;
                uint32_t v;
        } x;
        x.p = pid;
        uint32_t thread_id = x.v;
-       if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
-       else return NULL;
+
+       if (thread_id < pthread_counter + 1)
+               return pthread_map[thread_id];
+       else
+               return NULL;
 }
 
 /**