From ed4c0c4095856c1cfadf14ec868acd487ed88600 Mon Sep 17 00:00:00 2001 From: weiyu Date: Mon, 24 Aug 2020 15:39:35 -0700 Subject: [PATCH] Bug fix --- conditionvariable.cc | 6 +++--- model.cc | 15 ++++++++++++--- model.h | 1 + mutex.cc | 6 +++--- 4 files changed, 19 insertions(+), 9 deletions(-) diff --git a/conditionvariable.cc b/conditionvariable.cc index 1d049f18..9d569e97 100644 --- a/conditionvariable.cc +++ b/conditionvariable.cc @@ -14,15 +14,15 @@ condition_variable::~condition_variable() { } void condition_variable::notify_one() { - model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ONE, std::memory_order_seq_cst, this)); + model->switch_thread(new ModelAction(ATOMIC_NOTIFY_ONE, std::memory_order_seq_cst, this)); } void condition_variable::notify_all() { - model->switch_to_master(new ModelAction(ATOMIC_NOTIFY_ALL, std::memory_order_seq_cst, this)); + model->switch_thread(new ModelAction(ATOMIC_NOTIFY_ALL, std::memory_order_seq_cst, this)); } void condition_variable::wait(mutex& lock) { - model->switch_to_master(new ModelAction(ATOMIC_WAIT, std::memory_order_seq_cst, this, (uint64_t) &lock)); + model->switch_thread(new ModelAction(ATOMIC_WAIT, std::memory_order_seq_cst, this, (uint64_t) &lock)); //relock as a second action lock.lock(); } diff --git a/model.cc b/model.cc index 54f01855..1e425b2e 100644 --- a/model.cc +++ b/model.cc @@ -423,6 +423,7 @@ void ModelChecker::finishRunExecution(Thread *old) void ModelChecker::finishRunExecution(ucontext_t *old) { scheduler->set_current_thread(NULL); + break_execution = true; } void ModelChecker::consumeAction() @@ -544,12 +545,16 @@ void ModelChecker::handleChosenThread(Thread *old) void ModelChecker::handleChosenThread(ucontext_t *old) { - if (execution->has_asserted()) + if (execution->has_asserted()) { finishRunExecution(old); + return; + } if (!chosen_thread) chosen_thread = get_next_thread(); - if (!chosen_thread || chosen_thread->is_model_thread()) + if (!chosen_thread || chosen_thread->is_model_thread()) { finishRunExecution(old); + return; + } /* if (chosen_thread->just_woken_up()) { chosen_thread->set_wakeup_state(false); chosen_thread->set_pending(NULL); @@ -559,7 +564,7 @@ void ModelChecker::handleChosenThread(ucontext_t *old) finishRunExecution(old); else startRunExecution(old); - } else*/ + } */ { /* Consume the next action for a Thread */ @@ -604,7 +609,11 @@ void ModelChecker::run() checkfree = params.checkthreshold; for(int exec = 0;exec < params.maxexecutions;exec++) { chosen_thread = init_thread; + break_execution = false; do { + if (break_execution) + break; + thread_chosen = false; curr_thread_num = 1; startRunExecution(&system_context); diff --git a/model.h b/model.h index b98e7505..08f51b41 100644 --- a/model.h +++ b/model.h @@ -94,6 +94,7 @@ private: Thread * chosen_thread; bool thread_chosen; + bool break_execution; modelclock_t checkfree; diff --git a/mutex.cc b/mutex.cc index 0776db8e..27e4a080 100644 --- a/mutex.cc +++ b/mutex.cc @@ -19,17 +19,17 @@ mutex::mutex() void mutex::lock() { - model->switch_to_master(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this)); + model->switch_thread(new ModelAction(ATOMIC_LOCK, std::memory_order_seq_cst, this)); } bool mutex::try_lock() { - return model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this)); + return model->switch_thread(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this)); } void mutex::unlock() { - model->switch_to_master(new ModelAction(ATOMIC_UNLOCK, std::memory_order_seq_cst, this)); + model->switch_thread(new ModelAction(ATOMIC_UNLOCK, std::memory_order_seq_cst, this)); } } -- 2.34.1