Lock model check when we terminate proxy thread
authorroot <root@dw-6.eecs.uci.edu>
Sat, 27 Jul 2019 07:33:35 +0000 (00:33 -0700)
committerroot <root@dw-6.eecs.uci.edu>
Sat, 27 Jul 2019 07:33:35 +0000 (00:33 -0700)
action.cc
classlist.h
model.cc
snapshot.cc
threads.cc

index c9b920c..72cf972 100644 (file)
--- 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;
 }
 
 
index d3d9d3d..c7c8475 100644 (file)
@@ -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
index 2fabb08..65b597d 100644 (file)
--- 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;
index 6725a7a..dab1a48 100644 (file)
@@ -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);
index 35929be..c668b28 100644 (file)
@@ -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
 }