From 86b818595e02c86250a17ed88f2d6af15a3141f3 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 31 Jul 2019 21:15:34 -0700
Subject: [PATCH] Get GDAX working.

---
 main.cc     |  9 ++++++++-
 model.cc    | 14 --------------
 model.h     |  1 +
 params.h    |  1 +
 snapshot.cc |  5 +++--
 threads.cc  |  8 +++++++-
 6 files changed, 20 insertions(+), 18 deletions(-)

diff --git a/main.cc b/main.cc
index 53968233..53495072 100644
--- a/main.cc
+++ b/main.cc
@@ -23,6 +23,7 @@ void param_defaults(struct model_params *params)
 	params->uninitvalue = 0;
 	params->maxexecutions = 10;
 	params->nofork = false;
+	params->threadsnocleanup = false;
 }
 
 static void print_usage(const char *program_name, struct model_params *params)
@@ -56,6 +57,9 @@ static void print_usage(const char *program_name, struct model_params *params)
 		"                            Default: %u\n"
 		"                            -o help for a list of options\n"
 		"-n                          No fork\n"
+#ifdef TLS
+		"-d                          Don't allow threads to cleanup\n"
+#endif
 		" --                         Program arguments follow.\n\n",
 		program_name,
 		params->verbose,
@@ -86,7 +90,7 @@ bool install_plugin(char * name) {
 
 static void parse_options(struct model_params *params, int argc, char **argv)
 {
-	const char *shortopts = "hnt:o:u:x:v::";
+	const char *shortopts = "hdnt:o:u:x:v::";
 	const struct option longopts[] = {
 		{"help", no_argument, NULL, 'h'},
 		{"verbose", optional_argument, NULL, 'v'},
@@ -103,6 +107,9 @@ static void parse_options(struct model_params *params, int argc, char **argv)
 		case 'h':
 			print_usage(argv[0], params);
 			break;
+		case 'd':
+			params->threadsnocleanup = true;
+			break;
 		case 'n':
 			params->nofork = true;
 			break;
diff --git a/model.cc b/model.cc
index b0540699..66af9888 100644
--- a/model.cc
+++ b/model.cc
@@ -392,20 +392,6 @@ void ModelChecker::startMainThread() {
 	main_thread_startup();
 }
 
-static bool is_nonsc_write(const ModelAction *act) {
-	if (act->get_type() == ATOMIC_WRITE) {
-		std::memory_order order = act->get_mo();
-		switch(order) {
-		case std::memory_order_relaxed:
-		case std::memory_order_release:
-			return true;
-		default:
-			return false;
-		}
-	}
-	return false;
-}
-
 /** @brief Run ModelChecker for the user program */
 void ModelChecker::run()
 {
diff --git a/model.h b/model.h
index 2f137a3a..82d9bc8c 100644
--- a/model.h
+++ b/model.h
@@ -68,6 +68,7 @@ public:
 	void startMainThread();
 	void startChecker();
 	Thread * getInitThread() {return init_thread;}
+	Scheduler * getScheduler() {return scheduler;}
 	MEMALLOC
 private:
 	/** Flag indicates whether to restart the model checker. */
diff --git a/params.h b/params.h
index 7f749cae..9a2cf3b9 100644
--- a/params.h
+++ b/params.h
@@ -9,6 +9,7 @@ struct model_params {
 	unsigned int uninitvalue;
 	int maxexecutions;
 	bool nofork;
+	bool threadsnocleanup;
 
 	/** @brief Verbosity (0 = quiet; 1 = noisy; 2 = noisier) */
 	int verbose;
diff --git a/snapshot.cc b/snapshot.cc
index 2402bbde..24e8d073 100644
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -14,6 +14,9 @@
 #include "context.h"
 #include "model.h"
 
+
+#if USE_MPROTECT_SNAPSHOT
+
 /** PageAlignedAdressUpdate return a page aligned address for the
  * address being added as a side effect the numBytes are also changed.
  */
@@ -22,8 +25,6 @@ static void * PageAlignAddressUpward(void *addr)
 	return (void *)((((uintptr_t)addr) + PAGESIZE - 1) & ~(PAGESIZE - 1));
 }
 
-#if USE_MPROTECT_SNAPSHOT
-
 /* Each SnapShotRecord lists the firstbackingpage that must be written to
  * revert to that snapshot */
 struct SnapShotRecord {
diff --git a/threads.cc b/threads.cc
index 8d078b51..0da9282a 100644
--- a/threads.cc
+++ b/threads.cc
@@ -13,6 +13,7 @@
 /* global "model" object */
 #include "model.h"
 #include "execution.h"
+#include "schedule.h"
 
 #ifdef TLS
 #include <dlfcn.h>
@@ -319,10 +320,15 @@ void Thread::complete()
 	if (stack)
 		stack_free(stack);
 #ifdef TLS
-	if (this != model->getInitThread()) {
+	if (this != model->getInitThread() && !model->getParams()->threadsnocleanup) {
 		modellock = 1;
+		ASSERT(thread_current()==NULL);
+		Thread * curr_thread = model->getScheduler()->get_current_thread();
+		//Make any current_thread calls work in code to free
+		model->getScheduler()->set_current_thread(this);
 		real_pthread_mutex_unlock(&mutex2);
 		real_pthread_join(thread, NULL);
+		model->getScheduler()->set_current_thread(curr_thread);
 		modellock = 0;
 	}
 #endif
-- 
2.34.1