model: return value from switch_to_master

diff --git a/cmodelint.cc b/cmodelint.cc
index 7e52d10798ffc8777ebe2d7d4915055300b32c4d..76b4c90fa51b139cb8e70f891d8cc13692a34515 100644 (file)
--- 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 571789d662f154e109025e23c6d09ac89f998692..c10c43e596682a960896f1cef7380e1dea5de9f7 100644 (file)
--- 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 e4b6431336050c89043f45851214c632b2e943ce..e36426721ca44b53b7029cedb7de53ee79b22634 100644 (file)
--- 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 4f139878ce00300f4252c1705537deabd7643a5f..9b63f0fcdbce350fa04c272d2091c676af3dd42b 100644 (file)
--- 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 91b0b9a33f8a4109d82e9334f127534b1d6ec137..7fa0b589c8a4535a276c7f8f95eda76782bff554 100644 (file)
--- 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() {