From 6a0e918d9c3b534d025afdaeac5d931d0a6f323e Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Thu, 20 Sep 2012 15:26:37 -0700 Subject: [PATCH] model: mutex synchronization -> re-check release sequences All synchronization updates should generate a re-check of release sequences. This commit corrects this for mutexes. --- model.cc | 18 +++++++++++++----- model.h | 2 +- 2 files changed, 14 insertions(+), 6 deletions(-) diff --git a/model.cc b/model.cc index e7ab3bb..1e08120 100644 --- a/model.cc +++ b/model.cc @@ -374,8 +374,10 @@ bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw) * * The unlock operation has to re-enable all of the threads that are * waiting on the lock. + * + * @return True if synchronization was updated; false otherwise */ -void ModelChecker::process_mutex(ModelAction *curr) { +bool ModelChecker::process_mutex(ModelAction *curr) { std::mutex *mutex = (std::mutex *)curr->get_location(); struct std::mutex_state *state = mutex->get_state(); switch (curr->get_type()) { @@ -397,8 +399,10 @@ void ModelChecker::process_mutex(ModelAction *curr) { state->islocked = true; ModelAction *unlock = get_last_unlock(curr); //synchronize with the previous unlock statement - if (unlock != NULL) + if (unlock != NULL) { curr->synchronize_with(unlock); + return true; + } break; } case ATOMIC_UNLOCK: { @@ -416,6 +420,7 @@ void ModelChecker::process_mutex(ModelAction *curr) { default: ASSERT(0); } + return false; } /** @@ -618,6 +623,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) case WORK_CHECK_CURR_ACTION: { ModelAction *act = work.action; bool update = false; /* update this location's release seq's */ + bool update_all = false; /* update all release seq's */ process_thread_action(curr); @@ -627,10 +633,12 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) if (act->is_write() && process_write(act)) update = true; - if (act->is_mutex_op()) - process_mutex(act); + if (act->is_mutex_op() && process_mutex(act)) + update_all = true; - if (update) + if (update_all) + work_queue.push_back(CheckRelSeqWorkEntry(NULL)); + else if (update) work_queue.push_back(CheckRelSeqWorkEntry(act->get_location())); break; } diff --git a/model.h b/model.h index 42e023e..fa1bb6f 100644 --- a/model.h +++ b/model.h @@ -116,7 +116,7 @@ private: ModelAction * initialize_curr_action(ModelAction *curr); bool process_read(ModelAction *curr, bool second_part_of_rmw); bool process_write(ModelAction *curr); - void process_mutex(ModelAction *curr); + bool process_mutex(ModelAction *curr); bool process_thread_action(ModelAction *curr); bool check_action_enabled(ModelAction *curr); -- 2.34.1