From: Derek Yeh <djyeh@plrg-1.ics.uci.edu>
Date: Fri, 17 Jul 2020 03:30:31 +0000 (-0700)
Subject: add switch thread function
X-Git-Url: http://demsky.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=c6d52a276448fdaaec65fe5a2e126c301d537c40

add switch thread function
---

diff --git a/model.cc b/model.cc
index d1e94e5e..03f4648e 100644
--- 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 62b227e4..a1a04d13 100644
--- 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 c6078200..5756c102 100644
--- 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 8b55a91b..3d6b0863 100644
--- 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()