change the data structure of thrd_func_inst_list because more information about the...

[c11tester.git] / model.cc

diff --git a/model.cc b/model.cc
index 2fabb08291965adfa512930cfbe48d438b05e716..b0540699aee48bdca071ef1894d9690e7395c38e 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;
@@ -353,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()
@@ -363,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;
 }
@@ -419,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);