From: Brian Norris <banorris@uci.edu>
Date: Wed, 3 Apr 2013 00:25:04 +0000 (-0700)
Subject: model: get_mutex() for locating the lock map
X-Git-Tag: oopsla2013~115
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=4a86aaeab8ac67de02b4c692dead5fba243ab09b;hp=776279c18c4a4e6b763c4aeffc65fafe37205824;p=model-checker.git

model: get_mutex() for locating the lock map

The mutex can already be located via get_mutex(), so don't try to guess
whether it was store in the value or location fields of the ModelAction.
---

diff --git a/model.cc b/model.cc
index e6f9afd..a18754d 100644
--- a/model.cc
+++ b/model.cc
@@ -972,7 +972,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 		//unlock the lock
 		state->locked = NULL;
 		//wake up the other threads
-		action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
+		action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, mutex);
 		//activate all the waiting threads
 		for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 			scheduler->wake(get_thread(*rit));
@@ -984,7 +984,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 		//unlock the lock
 		state->locked = NULL;
 		//wake up the other threads
-		action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
+		action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, mutex);
 		//activate all the waiting threads
 		for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 			scheduler->wake(get_thread(*rit));