model: refactor mutex thread-blocking code

There are a few functions that are used in suboptimal ways.

* use the ModelChecker::get_thread(ModelAction *) version of overloaded
  'get_thread()' function

* the add/remove interfaces were used inconsistently previously; for
  "waking" we directly utilized Scheduler::add_thread, whereas the
  "sleeping" case used ModelChecker::remove_thread

* use the Scheduler::sleep and Scheduler::wake functions for sleep/wake
  instead of explicitly adding/removing

diff --git a/model.cc b/model.cc
index 40519e5315a62b12d78d6427a5ab5001236c267f..2c5ad5ad93b9e9939042ac0d6e42947ed4bab613 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -426,7 +426,7 @@ bool ModelChecker::process_mutex(ModelAction *curr) {
                action_list_t *waiters = lock_waiters_map->get_safe_ptr(curr->get_location());
                //activate all the waiting threads
                for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
-                       scheduler->add_thread(get_thread((*rit)->get_tid()));
+                       scheduler->wake(get_thread(*rit));
                }
                waiters->clear();
                break;
@@ -615,7 +615,7 @@ Thread * ModelChecker::check_current_action(ModelAction *curr)
                /* Make the execution look like we chose to run this action
                 * much later, when a lock is actually available to release */
                get_current_thread()->set_pending(curr);
-               remove_thread(get_current_thread());
+               scheduler->sleep(get_current_thread());
                return get_next_thread(NULL);
        }