fix thread switch

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 2aacaa2de441e3d3ff391b8009a241431fa0f9d7..53bb7b0d04b5f0ba6a34d1a9ed24218acdfbdbe3 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -351,8 +351,8 @@ void ModelChecker::continueExecution(Thread *old)
                checkfree += params.checkthreshold;
                execution->collectActions();
        }
-       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);
        scheduler->set_current_thread(thr);
        if (Thread::swap(old, thr) < 0) {
@@ -404,42 +404,45 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
        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())
+               if (!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);
 
-               ModelAction *act = old->get_pending();
+       if (old->is_waiting_on(old))
+               assert_bug("Deadlock detected (thread %u)", curr_thread_num);
+
+       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 (execution->has_asserted())
                        finishExecution(old);
                if (!chosen_thread)
@@ -450,7 +453,11 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
                        chosen_thread->set_wakeup_state(false);
                        chosen_thread->set_pending(NULL);
                        chosen_thread = NULL;
-                       continueExecution(old); // Allow this thread to stash the next pending action
+                       // Allow this thread to stash the next pending action
+                       if (should_terminate_execution())
+                               finishExecution(old);
+                       else
+                               continueExecution(old); 
                } else {
                        /* Consume the next action for a Thread */
                        consumeAction();
@@ -497,8 +504,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);