From: Brian Norris <banorris@uci.edu>
Date: Wed, 12 Dec 2012 02:08:31 +0000 (-0800)
Subject: model: return value from switch_to_master
X-Git-Tag: oopsla2013~436
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=commitdiff_plain;h=b35625b0499717b3caab5344d7278a31fbee9cb6

model: return value from switch_to_master
---

diff --git a/cmodelint.cc b/cmodelint.cc
index 7e52d10..76b4c90 100644
--- a/cmodelint.cc
+++ b/cmodelint.cc
@@ -4,8 +4,7 @@
 
 /** Performs a read action.*/
 uint64_t model_read_action(void * obj, memory_order ord) {
-	model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
-	return thread_current()->get_return_value();
+	return model->switch_to_master(new ModelAction(ATOMIC_READ, ord, obj));
 }
 
 /** Performs a write action.*/
@@ -24,8 +23,7 @@ void model_init_action(void * obj, uint64_t val) {
  * a write.
  */
 uint64_t model_rmwr_action(void *obj, memory_order ord) {
-	model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
-	return thread_current()->get_return_value();
+	return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
 }
 
 /** Performs the write part of a RMW action. */
diff --git a/impatomic.cc b/impatomic.cc
index 571789d..c10c43e 100644
--- a/impatomic.cc
+++ b/impatomic.cc
@@ -7,8 +7,7 @@ namespace std {
 
 bool atomic_flag_test_and_set_explicit ( volatile atomic_flag * __a__, memory_order __x__ ) {
 	volatile bool * __p__ = &((__a__)->__f__);
-	model->switch_to_master(new ModelAction(ATOMIC_RMWR, __x__, (void *) __p__));
-	bool result = (bool) thread_current()->get_return_value();
+	bool result = (bool) model->switch_to_master(new ModelAction(ATOMIC_RMWR, __x__, (void *) __p__));
 	model->switch_to_master(new ModelAction(ATOMIC_RMW, __x__, (void *) __p__, true));
 	return result;
 }
diff --git a/model.cc b/model.cc
index e4b6431..e364267 100644
--- a/model.cc
+++ b/model.cc
@@ -2680,15 +2680,19 @@ bool ModelChecker::is_enabled(thread_id_t tid) const
  * @param act The current action that will be explored. May be NULL only if
  * trace is exiting via an assertion (see ModelChecker::set_assert and
  * ModelChecker::has_asserted).
- * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
+ * @return Return the value returned by the current action
  */
-int ModelChecker::switch_to_master(ModelAction *act)
+uint64_t ModelChecker::switch_to_master(ModelAction *act)
 {
 	DBG();
 	Thread *old = thread_current();
 	set_current_action(act);
 	old->set_state(THREAD_READY);
-	return Thread::swap(old, &system_context);
+	if (Thread::swap(old, &system_context) < 0) {
+		perror("swap threads");
+		exit(EXIT_FAILURE);
+	}
+	return old->get_return_value();
 }
 
 /**
diff --git a/model.h b/model.h
index 4f13987..9b63f0f 100644
--- a/model.h
+++ b/model.h
@@ -116,7 +116,7 @@ public:
 	unsigned int get_num_threads() const;
 	Thread * get_current_thread() const;
 
-	int switch_to_master(ModelAction *act);
+	uint64_t switch_to_master(ModelAction *act);
 	ClockVector * get_cv(thread_id_t tid) const;
 	ModelAction * get_parent_action(thread_id_t tid) const;
 	void check_promises_thread_disabled();
diff --git a/mutex.cc b/mutex.cc
index 91b0b9a..7fa0b58 100644
--- a/mutex.cc
+++ b/mutex.cc
@@ -17,8 +17,7 @@ void mutex::lock() {
 }
 	
 bool mutex::try_lock() {
-  model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
-  return thread_current()->get_return_value();
+  return model->switch_to_master(new ModelAction(ATOMIC_TRYLOCK, std::memory_order_seq_cst, this));
 }
 
 void mutex::unlock() {