From db5cad55a147218984ef544439ee8a936303ddf8 Mon Sep 17 00:00:00 2001
From: Brian Norris <banorris@uci.edu>
Date: Sat, 2 Mar 2013 23:24:51 -0800
Subject: [PATCH] action: add get_mutex()

---
 action.cc | 14 ++++++++++++++
 action.h  |  5 +++++
 model.cc  |  9 ++-------
 3 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/action.cc b/action.cc
index 1007e762..be8c4a6c 100644
--- a/action.cc
+++ b/action.cc
@@ -651,3 +651,17 @@ bool ModelAction::may_read_from(const Promise *promise) const
 			return true;
 	return false;
 }
+
+/**
+ * Only valid for LOCK, TRY_LOCK, UNLOCK, and WAIT operations.
+ * @return The mutex operated on by this action, if any; otherwise NULL
+ */
+std::mutex * ModelAction::get_mutex() const
+{
+	if (is_trylock() || is_lock() || is_unlock())
+		return (std::mutex *)get_location();
+	else if (is_wait())
+		return (std::mutex *)get_value();
+	else
+		return NULL;
+}
diff --git a/action.h b/action.h
index 1b03bc48..a2079203 100644
--- a/action.h
+++ b/action.h
@@ -17,6 +17,10 @@ class ClockVector;
 class Thread;
 class Promise;
 
+namespace std {
+	class mutex;
+}
+
 using std::memory_order;
 using std::memory_order_relaxed;
 using std::memory_order_acquire;
@@ -85,6 +89,7 @@ public:
 	uint64_t get_return_value() const;
 	const ModelAction * get_reads_from() const { return reads_from; }
 	Promise * get_reads_from_promise() const { return reads_from_promise; }
+	std::mutex * get_mutex() const;
 
 	Node * get_node() const;
 	void set_node(Node *n) { node = n; }
diff --git a/model.cc b/model.cc
index 86289a07..77417600 100644
--- a/model.cc
+++ b/model.cc
@@ -927,16 +927,11 @@ bool ModelChecker::process_read(ModelAction *curr)
  */
 bool ModelChecker::process_mutex(ModelAction *curr)
 {
-	std::mutex *mutex = NULL;
+	std::mutex *mutex = curr->get_mutex();
 	struct std::mutex_state *state = NULL;
 
-	if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
-		mutex = (std::mutex *)curr->get_location();
+	if (mutex)
 		state = mutex->get_state();
-	} else if (curr->is_wait()) {
-		mutex = (std::mutex *)curr->get_value();
-		state = mutex->get_state();
-	}
 
 	switch (curr->get_type()) {
 	case ATOMIC_TRYLOCK: {
-- 
2.34.1