From 8127a0c80483af6e238f8cf2b6910a1e7da22416 Mon Sep 17 00:00:00 2001 From: weiyu Date: Tue, 11 Aug 2020 12:30:52 -0700 Subject: [PATCH] Replace some switch_to_master with switch_thread --- cmodelint.cc | 6 +++--- model.cc | 6 ++++-- threads.cc | 2 +- 3 files changed, 8 insertions(+), 6 deletions(-) diff --git a/cmodelint.cc b/cmodelint.cc index d3fcbb46..0cb67091 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -80,12 +80,12 @@ uint64_t model_rmwrcas_action_helper(void *obj, int atomic_index, uint64_t oldva uint64_t model_rmwr_action_helper(void *obj, int atomic_index, const char *position) { ensureModel(); - return model->switch_to_master(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)); + return model->switch_thread(new ModelAction(ATOMIC_RMWR, position, orders[atomic_index], obj)); } void model_rmw_action_helper(void *obj, uint64_t val, int atomic_index, const char * position) { ensureModel(); - model->switch_to_master(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)); + model->switch_thread(new ModelAction(ATOMIC_RMW, position, orders[atomic_index], obj, val)); } void model_rmwc_action_helper(void *obj, int atomic_index, const char *position) { @@ -161,7 +161,7 @@ CDSATOMICLOAD(64) #define CDSATOMICSTORE(size) \ void cds_atomic_store ## size(void * obj, uint ## size ## _t val, int atomic_index, const char * position) { \ ensureModel(); \ - model->switch_to_master(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)); \ + model->switch_thread(new ModelAction(ATOMIC_WRITE, position, orders[atomic_index], obj, (uint64_t) val)); \ *((volatile uint ## size ## _t *)obj) = val; \ thread_id_t tid = thread_current()->get_id(); \ for(int i=0;i < size / 8;i++) { \ diff --git a/model.cc b/model.cc index 70ea4cd6..136898e9 100644 --- a/model.cc +++ b/model.cc @@ -488,8 +488,10 @@ uint64_t ModelChecker::switch_thread(ModelAction *act) Thread* next = getNextThread(); if (next != nullptr) handleNewValidThread(old, next); - else + else { + old->set_state(THREAD_READY); // Just to avoid the first ASSERT in ModelExecution::take_step handleChosenThread(old); + } return old->get_return_value(); } @@ -593,8 +595,8 @@ void ModelChecker::run() initstate(423121, random_state, sizeof(random_state)); checkfree = params.checkthreshold; for(int exec = 0;exec < params.maxexecutions;exec++) { + chosen_thread = init_thread; do { - chosen_thread = init_thread; thread_chosen = false; curr_thread_num = 1; startRunExecution(&system_context); diff --git a/threads.cc b/threads.cc index fc5c84a1..8af66bde 100644 --- a/threads.cc +++ b/threads.cc @@ -242,7 +242,7 @@ void setup_context() { Thread * curr_thread = thread_current(); /* Add dummy "start" action, just to create a first clock vector */ - model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread)); + model->switch_thread(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread)); real_init_all(); -- 2.34.1