From: weiyu Date: Mon, 24 Aug 2020 22:45:26 +0000 (-0700) Subject: Bug fix for spsc-queue test X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=edf082882ea7a2d27d3a3322a84e42b040f186a4;hp=829aac4055269992c26fed5530cfdaf59775b2a9;p=c11tester.git Bug fix for spsc-queue test --- 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 078a1ce7..ea8f268f 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,9 +564,7 @@ void ModelChecker::handleChosenThread(ucontext_t *old) finishRunExecution(old); else startRunExecution(old); - } else - - { + } else { /* Consume the next action for a Thread */ consumeAction(); @@ -604,7 +607,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)); } }