model: return value from switch_to_master
authorBrian Norris <banorris@uci.edu>
Wed, 12 Dec 2012 02:08:31 +0000 (18:08 -0800)
committerBrian Norris <banorris@uci.edu>
Wed, 12 Dec 2012 02:09:07 +0000 (18:09 -0800)
cmodelint.cc
impatomic.cc
model.cc
model.h
mutex.cc

index 7e52d10..76b4c90 100644 (file)
@@ -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. */
index 571789d..c10c43e 100644 (file)
@@ -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;
 }
index e4b6431..e364267 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 4f13987..9b63f0f 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();
index 91b0b9a..7fa0b58 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() {