Lock model check when we terminate proxy thread

diff --git a/action.cc b/action.cc
index c9b920c8e6299ac514290d239e4b64bbc06c7d4d..72cf97246765403360275604d1076501e4a94bf7 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;
 }
 
 

diff --git a/classlist.h b/classlist.h
index d3d9d3d2c0f2389ae7214f9a0527585c06deb2a5..c7c84759ce1065687fad0c4e55bb85dcb5e0db09 100644 (file)
--- 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 2fabb08291965adfa512930cfbe48d438b05e716..65b597defb0b10294083f57a468b6886e7ae17b0 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;

diff --git a/snapshot.cc b/snapshot.cc
index 6725a7aed80ffefab54247fde99e87d848c60329..dab1a480d5910d84ed97ec2782e6fa73d7e50a85 100644 (file)
--- 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 35929be6e79ced5ec9a1e1add478d22380a9b122..c668b288c21fa9d647c008a7931e1e7287a3748e 100644 (file)
--- 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
 }