fix edge case

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 5decd2bea613c3058abcfd53dcc0d371fd3f5336..2f744eee754e43126b071638f8f81568b834ed53 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -351,9 +351,9 @@ void ModelChecker::continueExecution(Thread *old)
                checkfree += params.checkthreshold;
                execution->collectActions();
        }
-       curr_thread_num = 0;
-       thread_id_t tid = int_to_id(0);
-       Thread *thr = get_thread(tid);
+       thread_chosen = false;
+       curr_thread_num = 1;
+       Thread *thr = getNextThread();
        scheduler->set_current_thread(thr);
        if (Thread::swap(old, thr) < 0) {
                perror("swap threads");
@@ -361,6 +361,20 @@ void ModelChecker::continueExecution(Thread *old)
        }
 }
 
+Thread* ModelChecker::getNextThread()
+{
+       Thread *thr = NULL;
+       for (unsigned int i = curr_thread_num; i < get_num_threads(); i++) {
+               thread_id_t tid = int_to_id(i);
+               thr = get_thread(tid);
+               if (!thr->is_complete() && !thr->get_pending()) {
+                       curr_thread_num = i;
+                       break;
+               }
+       }
+       return thr;
+}
+
 void ModelChecker::finishExecution(Thread *old) 
 {
        scheduler->set_current_thread(NULL);
@@ -399,50 +413,43 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
 
        old->set_pending(act);
 
-       Thread *next = NULL;
        curr_thread_num++;
-       while (curr_thread_num < get_num_threads()) {
-               thread_id_t tid = int_to_id(curr_thread_num);
-               next = get_thread(tid);
-               if (!next->is_model_thread() && !next->is_complete() && !next->get_pending())
-                       break;
-               curr_thread_num++;
-       }
-       if (curr_thread_num < get_num_threads()) {
-               scheduler->set_current_thread(next);
-               if (old->is_waiting_on(old))
-                       assert_bug("Deadlock detected (thread %u)", curr_thread_num);
+       Thread* next = getNextThread();
 
-               ModelAction *act = old->get_pending();
+       if (old->is_waiting_on(old))
+               assert_bug("Deadlock detected (thread %u)", curr_thread_num-1);
+
+       ModelAction *act2 = old->get_pending();
                
-               if (act && execution->is_enabled(old) && !execution->check_action_enabled(act)) {
-                       scheduler->sleep(old);
-               }
-               if (!thread_chosen && act && execution->is_enabled(old) && (old->get_state() != THREAD_BLOCKED) ) {
-                       if (act->is_write()) {
-                               std::memory_order order = act->get_mo();
-                               if (order == std::memory_order_relaxed || \
-                                               order == std::memory_order_release) {
-                                       chosen_thread = old;
-                                       thread_chosen = true;
-                               }
-                       } else if (act->get_type() == THREAD_CREATE || \
-                                                               act->get_type() == PTHREAD_CREATE || \
-                                                               act->get_type() == THREAD_START || \
-                                                               act->get_type() == THREAD_FINISH) {
+       if (act2 && execution->is_enabled(old) && !execution->check_action_enabled(act2)) {
+               scheduler->sleep(old);
+       }
+       if (!thread_chosen && act2 && execution->is_enabled(old) && (old->get_state() != THREAD_BLOCKED) ) {
+               if (act2->is_write()) {
+                       std::memory_order order = act2->get_mo();
+                       if (order == std::memory_order_relaxed || \
+                                       order == std::memory_order_release) {
                                chosen_thread = old;
                                thread_chosen = true;
                        }
+               } else if (act2->get_type() == THREAD_CREATE || \
+                                                       act2->get_type() == PTHREAD_CREATE || \
+                                                       act2->get_type() == THREAD_START || \
+                                                       act2->get_type() == THREAD_FINISH) {
+                       chosen_thread = old;
+                       thread_chosen = true;
                }
+       }
+
+       if (curr_thread_num < get_num_threads()) {
+               scheduler->set_current_thread(next);    
 
                if (Thread::swap(old, next) < 0) {
                        perror("swap threads");
                        exit(EXIT_FAILURE);
                }               
        } else {
-               if (old->is_waiting_on(old))
-                       assert_bug("Deadlock detected (thread %u)", curr_thread_num);
-
+               
                if (execution->has_asserted())
                        finishExecution(old);
                if (!chosen_thread)
@@ -504,8 +511,8 @@ void ModelChecker::run()
        for(int exec = 0;exec < params.maxexecutions;exec++) {
                chosen_thread = init_thread;
                thread_chosen = false;
-               curr_thread_num = 0;
-               thread_id_t tid = int_to_id(0);
+               curr_thread_num = 1;
+               thread_id_t tid = int_to_id(1);
                Thread *thr = get_thread(tid);
                switch_from_master(thr);
                finish_execution((exec+1) < params.maxexecutions);