add switch thread function

diff --git a/model.cc b/model.cc
index d1e94e5efa4f70c08486abf646b0ef46a3fae324..03f4648ea2da536360de815f4ac53c4bbf01b8d8 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -344,6 +344,62 @@ uint64_t ModelChecker::switch_to_master(ModelAction *act)
        return old->get_return_value();
 }
 
+uint64_t ModelChecker::switch_thread(ModelAction *act)
+{
+       if (modellock) {
+               static bool fork_message_printed = false;
+
+               if (!fork_message_printed) {
+                       model_print("Fork handler or dead thread trying to call into model checker...\n");
+                       fork_message_printed = true;
+               }
+               delete act;
+               return 0;
+       }
+       DBG();
+       Thread *old = thread_current();
+       ASSERT(!old->get_pending());
+
+       if (inspect_plugin != NULL) {
+               inspect_plugin->inspectModelAction(act);
+       }
+
+       old->set_pending(act);
+       //Thread *next;
+       /*do {
+               curr_thread_num++;
+               thread_id_t tid = int_to_id(curr_thread_num);
+               next = get_thread(tid);
+
+       } while (next->is_model_thread() || next->is_complete() || next->get_pending() && curr_thread_num < get_num_threads()); 
+       */
+       Thread *next;
+       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 (Thread::swap(old, next) < 0) {
+                       perror("swap threads");
+                       exit(EXIT_FAILURE);
+               }
+               if (next->is_waiting_on(next))
+                       assert_bug("Deadlock detected (thread %u)", curr_thread_num);
+       } else {
+               scheduler->set_current_thread(NULL);
+               if (Thread::swap(old, &system_context) < 0) {
+                       perror("swap threads");
+                       exit(EXIT_FAILURE);
+               }
+       }
+       return old->get_return_value();
+}
+
 static void runChecker() {
        model->run();
        delete model;
@@ -391,6 +447,11 @@ void ModelChecker::run()
                         * thread which just took a step--plus the first step
                         * for any newly-created thread
                         */
+                       curr_thread_num = 0;
+                       thread_id_t tid = int_to_id(0);
+                       Thread *thr = get_thread(tid);
+                       switch_from_master(tid);
+                       /*
                        for (unsigned int i = 0;i < get_num_threads();i++) {
                                thread_id_t tid = int_to_id(i);
                                Thread *thr = get_thread(tid);
@@ -400,7 +461,7 @@ void ModelChecker::run()
                                                assert_bug("Deadlock detected (thread %u)", i);
                                }
                        }
-
+                       */
                        /* Don't schedule threads which should be disabled */
                        for (unsigned int i = 0;i < get_num_threads();i++) {
                                Thread *th = get_thread(int_to_id(i));

diff --git a/model.h b/model.h
index 62b227e4bcdce915125e9c8b7f9a877c94ee9529..a1a04d138cb31d4fe5936d648303073871a7d400 100644 (file)
--- a/model.h
+++ b/model.h
@@ -53,6 +53,7 @@ public:
 
        void switch_from_master(Thread *thread);
        uint64_t switch_to_master(ModelAction *act);
+       uint64_t switch_thread(ModelAction *act);
 
        void assert_bug(const char *msg, ...);
 
@@ -77,6 +78,8 @@ private:
 
        int execution_number;
 
+       int curr_thread_num;
+
        unsigned int get_num_threads() const;
 
        void finish_execution(bool moreexecutions);

diff --git a/threads-model.h b/threads-model.h
index c6078200f5911f5bf3dd78f80125b881683e1a0e..5756c1029688fb6fd9d29616291d496129592f7a 100644 (file)
--- a/threads-model.h
+++ b/threads-model.h
@@ -49,6 +49,7 @@ public:
 
        static int swap(ucontext_t *ctxt, Thread *t);
        static int swap(Thread *t, ucontext_t *ctxt);
+       static int swap(Thread *t, Thread *t2);
 
        thread_state get_state() const { return state; }
        void set_state(thread_state s);

diff --git a/threads.cc b/threads.cc
index 8b55a91b186b61534ec124ca2a990283c11a3ffb..3d6b0863234273684de989ce7dd199e9f1931a72 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -60,7 +60,7 @@ Thread * thread_current(void)
 }
 
 void modelexit() {
-       model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
+       model->switch_thread(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, thread_current()));
 }
 
 void initMainThread() {
@@ -330,6 +330,16 @@ int Thread::swap(ucontext_t *ctxt, Thread *t)
        return model_swapcontext(ctxt, &t->context);
 }
 
+int Thread::swap(Thread *t, Thread *t2)
+{
+       t->set_state(THREAD_READY);
+       t2->set_state(THREAD_RUNNING);
+#ifdef TLS
+       if (t2->tls != NULL)
+               set_tls_addr((uintptr_t)t2->tls);
+#endif
+       return model_swapcontext(&t->context, &t2->context);
+}
 
 /** Terminate a thread and free its stack. */
 void Thread::complete()