From: root <root@dw-6.eecs.uci.edu>
Date: Sat, 27 Jul 2019 07:33:35 +0000 (-0700)
Subject: Lock model check when we terminate proxy thread
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=809d0f8a8f05ad2464c5e4df5b14ad2650d59fe8

Lock model check when we terminate proxy thread
---

diff --git a/action.cc b/action.cc
index c9b920c8..72cf9724 100644
--- a/action.cc
+++ b/action.cc
@@ -49,7 +49,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
 	ASSERT(loc || type == ATOMIC_FENCE || type == NOOP);
 
 	Thread *t = thread ? thread : thread_current();
-	this->tid = t->get_id();
+	this->tid = t!= NULL ? t->get_id() : -1;
 }
 
 
diff --git a/classlist.h b/classlist.h
index d3d9d3d2..c7c84759 100644
--- a/classlist.h
+++ b/classlist.h
@@ -23,5 +23,5 @@ typedef SnapList<ModelAction *> action_list_t;
 typedef SnapList<uint32_t> func_id_list_t;
 typedef SnapList<FuncInst *> func_inst_list_t;
 
-extern volatile int forklock;
+extern volatile int modellock;
 #endif
diff --git a/model.cc b/model.cc
index 2fabb082..65b597de 100644
--- a/model.cc
+++ b/model.cc
@@ -319,11 +319,11 @@ void ModelChecker::switch_from_master(Thread *thread)
  */
 uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
-	if (forklock) {
+	if (modellock) {
 		static bool fork_message_printed = false;
 
 		if (!fork_message_printed) {
-			model_print("Fork handler trying to call into model checker...\n");
+			model_print("Fork handler or dead thread trying to call into model checker...\n");
 			fork_message_printed = true;
 		}
 		delete act;
diff --git a/snapshot.cc b/snapshot.cc
index 6725a7ae..dab1a480 100644
--- a/snapshot.cc
+++ b/snapshot.cc
@@ -375,7 +375,7 @@ static void fork_snapshot_init(unsigned int numbackingpages,
 	model_snapshot_space = create_mspace(numheappages * PAGESIZE, 1);
 }
 
-volatile int forklock = 0;
+volatile int modellock = 0;
 
 static void fork_loop() {
 	/* switch back here when takesnapshot is called */
@@ -389,9 +389,9 @@ static void fork_loop() {
 		pid_t forkedID;
 		fork_snap->currSnapShotID = snapshotid + 1;
 
-		forklock = 1;
+		modellock = 1;
 		forkedID = fork();
-		forklock = 0;
+		modellock = 0;
 
 		if (0 == forkedID) {
 			setcontext(&fork_snap->shared_ctxt);
diff --git a/threads.cc b/threads.cc
index 35929be6..c668b288 100644
--- a/threads.cc
+++ b/threads.cc
@@ -305,8 +305,10 @@ void Thread::complete()
 		stack_free(stack);
 #ifdef TLS
 	if (this != model->getInitThread()) {
+		modellock = 1;
 		real_pthread_mutex_unlock(&mutex2);
 		real_pthread_join(thread, NULL);
+		modellock = 0;
 	}
 #endif
 }