X-Git-Url: http://plrg.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=b0540699aee48bdca071ef1894d9690e7395c38e;hb=04a39b7be7672034249091a7df9a4c8407a8b787;hp=e4d6b75f95cb8178d34184d838999b3a9b62b08f;hpb=11349f4e83c1446d5c678384a7d45e410c82c3e2;p=c11tester.git

diff --git a/model.cc b/model.cc
index e4d6b75f..b0540699 100644
--- a/model.cc
+++ b/model.cc
@@ -24,9 +24,6 @@ ModelChecker *model = NULL;
 /** Wrapper to run the user's main function, with appropriate arguments */
 void user_main_wrapper(void *)
 {
-#ifdef TLS
-	model->get_execution()->getTLSSize();
-#endif
 	user_main(model->params.argc, model->params.argv);
 }
 
@@ -322,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;
@@ -356,6 +353,8 @@ static void runChecker() {
 
 void ModelChecker::startChecker() {
 	startExecution(get_system_context(), runChecker);
+	snapshot_stack_init();
+	snapshot_record(0);
 }
 
 bool ModelChecker::should_terminate_execution()
@@ -366,6 +365,8 @@ bool ModelChecker::should_terminate_execution()
 	else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
 		execution->set_assert();
 		return true;
+	} else if (execution->isFinished()) {
+		return true;
 	}
 	return false;
 }
@@ -388,7 +389,7 @@ void ModelChecker::do_restart()
 void ModelChecker::startMainThread() {
 	init_thread->set_state(THREAD_RUNNING);
 	scheduler->set_current_thread(init_thread);
-	thread_startup();
+	main_thread_startup();
 }
 
 static bool is_nonsc_write(const ModelAction *act) {
@@ -422,11 +423,10 @@ void ModelChecker::run()
 			 * thread which just took a step--plus the first step
 			 * for any newly-created thread
 			 */
-			ModelAction * pending;
 			for (unsigned int i = 0;i < get_num_threads();i++) {
 				thread_id_t tid = int_to_id(i);
 				Thread *thr = get_thread(tid);
-				if (!thr->is_model_thread() && !thr->is_complete() && ((!(pending=thr->get_pending())) || is_nonsc_write(pending)) ) {
+				if (!thr->is_model_thread() && !thr->is_complete() && (!thr->get_pending())) {
 					switch_from_master(thr);	// L: context swapped, and action type of thr changed.
 					if (thr->is_waiting_on(thr))
 						assert_bug("Deadlock detected (thread %u)", i);