From ad105d2fb3c5f352ac6b7da0e1e910e94692398d Mon Sep 17 00:00:00 2001 From: weiyu Date: Tue, 15 Sep 2020 16:26:24 -0700 Subject: [PATCH] Add back model_thread; it is still needed --- execution.cc | 18 ++++++++++-------- execution.h | 3 ++- model.cc | 6 +++--- threads.cc | 4 +++- 4 files changed, 18 insertions(+), 13 deletions(-) diff --git a/execution.cc b/execution.cc index 61d33cb9..d2efaba7 100644 --- a/execution.cc +++ b/execution.cc @@ -87,6 +87,8 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : isfinished(false) { /* Initialize a model-checker thread, for special ModelActions */ + model_thread = new Thread(get_next_id()); + add_thread(model_thread); fuzzer->register_engine(m, this); scheduler->register_engine(this); #ifdef TLS @@ -97,7 +99,7 @@ ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) : /** @brief Destructor */ ModelExecution::~ModelExecution() { - for (unsigned int i = 0;i < get_num_threads();i++) + for (unsigned int i = INITIAL_THREAD_ID;i < get_num_threads();i++) delete get_thread(int_to_id(i)); delete mo_graph; @@ -266,7 +268,7 @@ bool ModelExecution::should_wake_up(const ModelAction * asleep) const void ModelExecution::wake_up_sleeping_actions() { - for (unsigned int i = 0;i < get_num_threads();i++) { + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { thread_id_t tid = int_to_id(i); if (scheduler->is_sleep_set(tid)) { Thread *thr = get_thread(tid); @@ -345,7 +347,7 @@ void ModelExecution::set_assert() bool ModelExecution::is_deadlocked() const { bool blocking_threads = false; - for (unsigned int i = 0;i < get_num_threads();i++) { + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { thread_id_t tid = int_to_id(i); if (is_enabled(tid)) return false; @@ -365,7 +367,7 @@ bool ModelExecution::is_deadlocked() const */ bool ModelExecution::is_complete_execution() const { - for (unsigned int i = 0;i < get_num_threads();i++) + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) if (is_enabled(int_to_id(i))) return false; return true; @@ -494,7 +496,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) case ATOMIC_WAIT: { Thread *curr_thrd = get_thread(curr); /* wake up the other threads */ - for (unsigned int i = 0;i < get_num_threads();i++) { + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { Thread *t = get_thread(int_to_id(i)); if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock()) scheduler->wake(t); @@ -523,7 +525,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) } /* wake up the other threads */ - for (unsigned int i = 0;i < get_num_threads();i++) { + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { Thread *t = get_thread(int_to_id(i)); if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock()) scheduler->wake(t); @@ -543,7 +545,7 @@ bool ModelExecution::process_mutex(ModelAction *curr) // TODO: lock count for recursive mutexes /* wake up the other threads */ Thread *curr_thrd = get_thread(curr); - for (unsigned int i = 0;i < get_num_threads();i++) { + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { Thread *t = get_thread(int_to_id(i)); if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock()) scheduler->wake(t); @@ -675,7 +677,7 @@ void ModelExecution::process_thread_action(ModelAction *curr) } /* Wake up any joining threads */ - for (unsigned int i = 0;i < get_num_threads();i++) { + for (unsigned int i = MAIN_THREAD_ID;i < get_num_threads();i++) { Thread *waiting = get_thread(int_to_id(i)); if (waiting->waiting_on() == th && waiting->get_pending()->is_thread_join()) diff --git a/execution.h b/execution.h index b8bfb035..5e80e186 100644 --- a/execution.h +++ b/execution.h @@ -19,7 +19,8 @@ #include #include "classlist.h" -#define INITIAL_THREAD_ID 0 +#define INITIAL_THREAD_ID 0 +#define MAIN_THREAD_ID 1 struct PendingFutureValue { PendingFutureValue(ModelAction *writer, ModelAction *reader) : diff --git a/model.cc b/model.cc index 4b94d75a..f7337706 100644 --- a/model.cc +++ b/model.cc @@ -75,7 +75,7 @@ ModelChecker::ModelChecker() : history(new ModelHistory()), execution(new ModelExecution(this, scheduler)), execution_number(1), - curr_thread_num(INITIAL_THREAD_ID), + curr_thread_num(MAIN_THREAD_ID), trace_analyses(), inspect_plugin(NULL) { @@ -353,7 +353,7 @@ void ModelChecker::startRunExecution(Thread *old) { execution->collectActions(); } - curr_thread_num = INITIAL_THREAD_ID; + curr_thread_num = MAIN_THREAD_ID; Thread *thr = getNextThread(old); if (thr != nullptr) { scheduler->set_current_thread(thr); @@ -421,7 +421,7 @@ void ModelChecker::finishRunExecution(Thread *old) scheduler->set_current_thread(NULL); /** Reset curr_thread_num to initial value for next execution. */ - curr_thread_num = INITIAL_THREAD_ID; + curr_thread_num = MAIN_THREAD_ID; /** If we have more executions, we won't make it past this call. */ finish_execution(execution_number < params.maxexecutions); diff --git a/threads.cc b/threads.cc index 024f6ea5..bd1b6249 100644 --- a/threads.cc +++ b/threads.cc @@ -419,7 +419,9 @@ Thread::Thread(thread_id_t tid) : last_action_val(0), model_thread(true) { - real_memset(&context, 0, sizeof(context)); + // real_memset is not defined when + // the model thread is constructed + memset(&context, 0, sizeof(context)); } /** -- 2.34.1