From: Brian Norris <banorris@uci.edu>
Date: Wed, 3 Oct 2012 00:14:46 +0000 (-0700)
Subject: model: refactor mutex thread-blocking code
X-Git-Tag: pldi2013~121^2~4
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=28a8923983a54f838c7a1667795d37c1d801877c;p=model-checker.git

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 40519e5..2c5ad5a 100644
--- 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);
 	}