From 563d0da13f38cf55a88673c2a712b797d4938df1 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Sat, 29 Aug 2020 14:24:35 -0700
Subject: [PATCH] add support for freeing threads

---
 execution.cc    |  2 +-
 model.cc        | 18 +++++++++++-------
 model.h         |  2 +-
 threads-model.h |  8 ++++++--
 threads.cc      |  5 ++++-
 5 files changed, 23 insertions(+), 12 deletions(-)

diff --git a/execution.cc b/execution.cc
index 53b6bccf..c1a53087 100644
--- a/execution.cc
+++ b/execution.cc
@@ -1819,7 +1819,7 @@ ClockVector * ModelExecution::computeMinimalCV() {
 	//Thread 0 isn't a real thread, so skip it..
 	for(unsigned int i = 1;i < thread_map.size();i++) {
 		Thread * t = thread_map[i];
-		if (t->get_state() == THREAD_COMPLETED)
+		if (t->is_complete())
 			continue;
 		thread_id_t tid = int_to_id(i);
 		ClockVector * cv = get_cv(tid);
diff --git a/model.cc b/model.cc
index c2de3130..596e528d 100644
--- a/model.cc
+++ b/model.cc
@@ -332,7 +332,7 @@ void ModelChecker::startRunExecution(Thread *old) {
 		thread_chosen = false;
 		curr_thread_num = 1;
 
-		Thread *thr = getNextThread();
+		Thread *thr = getNextThread(old);
 		if (thr != nullptr) {
 			scheduler->set_current_thread(thr);
 
@@ -371,17 +371,21 @@ void ModelChecker::startRunExecution(Thread *old) {
 	}
 }
 
-Thread* ModelChecker::getNextThread()
+Thread* ModelChecker::getNextThread(Thread *old)
 {
 	Thread *nextThread = nullptr;
 	for (unsigned int i = curr_thread_num;i < get_num_threads();i++) {
 		thread_id_t tid = int_to_id(i);
 		Thread *thr = get_thread(tid);
 
-		if (!thr->is_complete() && !thr->get_pending()) {
-			curr_thread_num = i;
-			nextThread = thr;
-			break;
+		if (!thr->is_complete()) {
+			if (!thr->get_pending()) {
+				curr_thread_num = i;
+				nextThread = thr;
+				break;
+			}
+		} else if (thr != old && !thr->is_freed()) {
+			thr->freeResources();
 		}
 
 		/* Don't schedule threads which should be disabled */
@@ -481,7 +485,7 @@ uint64_t ModelChecker::switch_thread(ModelAction *act)
 	chooseThread(act, old);
 
 	curr_thread_num++;
-	Thread* next = getNextThread();
+	Thread* next = getNextThread(old);
 	if (next != nullptr) {
 		scheduler->set_current_thread(next);
 		if (Thread::swap(old, next) < 0) {
diff --git a/model.h b/model.h
index 44ed858f..12aeebcc 100644
--- a/model.h
+++ b/model.h
@@ -79,7 +79,7 @@ private:
 	void finishRunExecution(Thread *old);
 	void consumeAction();
 	void chooseThread(ModelAction *act, Thread *thr);
-	Thread * getNextThread();
+	Thread * getNextThread(Thread *old);
 	void handleChosenThread(Thread *old);
 
 	modelclock_t checkfree;
diff --git a/threads-model.h b/threads-model.h
index 73c1d8f7..b1aa9013 100644
--- a/threads-model.h
+++ b/threads-model.h
@@ -33,7 +33,8 @@ typedef enum thread_state {
 	 */
 	THREAD_BLOCKED,
 	/** Thread has completed its execution */
-	THREAD_COMPLETED
+	THREAD_COMPLETED,
+	THREAD_FREED
 } thread_state;
 
 
@@ -81,7 +82,10 @@ public:
 	void * get_pthread_return() { return pthread_return; }
 
 	/** @return True if this thread is finished executing */
-	bool is_complete() const { return state == THREAD_COMPLETED; }
+	bool is_complete() const { return state == THREAD_COMPLETED || state == THREAD_FREED; }
+
+	/** @return True if this thread has finished and its resources have been freed */
+	bool is_freed() const { return state == THREAD_FREED; }
 
 	/** @return True if this thread is blocked */
 	bool is_blocked() const { return state == THREAD_BLOCKED; }
diff --git a/threads.cc b/threads.cc
index 942d183f..aef263ec 100644
--- a/threads.cc
+++ b/threads.cc
@@ -357,12 +357,12 @@ void Thread::freeResources() {
 		stack_free(stack);
 #ifdef TLS
 	if (this != model->getInitThread()) {
-		ASSERT(thread_current()==NULL);
 		real_pthread_mutex_unlock(&mutex2);
 		real_pthread_join(thread, NULL);
 		stack_free(helper_stack);
 	}
 #endif
+	state = THREAD_FREED;
 }
 
 /**
@@ -378,6 +378,7 @@ Thread::Thread(thread_id_t tid) :
 	acq_fence_cv(new ClockVector()),
 	creation(NULL),
 	pending(NULL),
+	wakeup_state(false),
 	start_routine(NULL),
 	arg(NULL),
 	stack(NULL),
@@ -404,6 +405,7 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void (*func)(void *), void *a, Thread
 	acq_fence_cv(new ClockVector()),
 	creation(NULL),
 	pending(NULL),
+	wakeup_state(false),
 	start_routine(func),
 	pstart_routine(NULL),
 	arg(a),
@@ -437,6 +439,7 @@ Thread::Thread(thread_id_t tid, thrd_t *t, void *(*func)(void *), void *a, Threa
 	acq_fence_cv(new ClockVector()),
 	creation(NULL),
 	pending(NULL),
+	wakeup_state(false),
 	start_routine(NULL),
 	pstart_routine(func),
 	arg(a),
-- 
2.34.1