From: Brian Norris <banorris@uci.edu>
Date: Wed, 3 Apr 2013 00:45:24 +0000 (-0700)
Subject: model: merge duplicated code for WAIT and UNLOCK
X-Git-Tag: oopsla2013~113
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=9580c5beb0b9e5425d77ddb142e18574d0dea16c;p=model-checker.git

model: merge duplicated code for WAIT and UNLOCK
---

diff --git a/model.cc b/model.cc
index a18754d..4a35fcd 100644
--- a/model.cc
+++ b/model.cc
@@ -968,6 +968,7 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 		}
 		break;
 	}
+	case ATOMIC_WAIT:
 	case ATOMIC_UNLOCK: {
 		//unlock the lock
 		state->locked = NULL;
@@ -978,22 +979,14 @@ bool ModelChecker::process_mutex(ModelAction *curr)
 			scheduler->wake(get_thread(*rit));
 		}
 		waiters->clear();
-		break;
-	}
-	case ATOMIC_WAIT: {
-		//unlock the lock
-		state->locked = NULL;
-		//wake up the other threads
-		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));
-		}
-		waiters->clear();
-		//check whether we should go to sleep or not...simulate spurious failures
+
+		if (!curr->is_wait())
+			break; /* The rest is only for ATOMIC_WAIT */
+
+		/* Should we go to sleep? (simulate spurious failures) */
 		if (curr->get_node()->get_misc() == 0) {
 			get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
-			//disable us
+			/* disable us */
 			scheduler->sleep(get_thread(curr));
 		}
 		break;