threads/model: move switch_to_master from class Thread to class ModelChecker

diff --git a/libatomic.cc b/libatomic.cc
index 059d2ae8d6aab1ac456a212b1b455d03214c33b9..e224a8a3d412bffa96bb052c61a5132b936a0495 100644 (file)
--- a/libatomic.cc
+++ b/libatomic.cc
@@ -1,14 +1,13 @@
 #include "libatomic.h"
 #include "model.h"
-#include "threads_internal.h"
 
 void atomic_store_explicit(struct atomic_object *obj, int value, memory_order order)
 {
-       thread_current()->switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
+       model->switch_to_master(new ModelAction(ATOMIC_WRITE, order, obj, value));
 }
 
 int atomic_load_explicit(struct atomic_object *obj, memory_order order)
 {
-       thread_current()->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, VALUE_NONE));
+       model->switch_to_master(new ModelAction(ATOMIC_READ, order, obj, VALUE_NONE));
        return 0;
 }

diff --git a/libthreads.cc b/libthreads.cc
index fd6259ad64d62474e0f7b7565cc72685e56288ad..7ed5491f675fe91d646a8bec1d056ae712ea2ab3 100644 (file)
--- a/libthreads.cc
+++ b/libthreads.cc
@@ -23,14 +23,14 @@ int thrd_join(thrd_t t)
        Thread *th = model->get_thread(thrd_to_id(t));
        while (th->get_state() != THREAD_COMPLETED && !ret)
                /* seq_cst is just a 'don't care' parameter */
-               ret = thread_current()->switch_to_master(new ModelAction(THREAD_JOIN, memory_order_seq_cst, NULL, VALUE_NONE));
+               ret = model->switch_to_master(new ModelAction(THREAD_JOIN, memory_order_seq_cst, NULL, VALUE_NONE));
        return ret;
 }
 
 int thrd_yield(void)
 {
        /* seq_cst is just a 'don't care' parameter */
-       return thread_current()->switch_to_master(new ModelAction(THREAD_YIELD, memory_order_seq_cst, NULL, VALUE_NONE));
+       return model->switch_to_master(new ModelAction(THREAD_YIELD, memory_order_seq_cst, NULL, VALUE_NONE));
 }
 
 thrd_t thrd_current(void)

diff --git a/model.cc b/model.cc
index 42d31b385c5fab84d2bed8eafc54286c1885e510..1015701d917803c75541fb2d3b830a0f223c301c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -55,6 +55,18 @@ int ModelChecker::add_thread(Thread *t)
        return 0;
 }
 
+int ModelChecker::switch_to_master(ModelAction *act)
+{
+       Thread *old, *next;
+
+       DBG();
+       old = thread_current();
+       set_current_action(act);
+       old->set_state(THREAD_READY);
+       next = system_thread;
+       return old->swap(next);
+}
+
 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, int value)
 {
        Thread *t = thread_current();

diff --git a/model.h b/model.h
index f26ab55b5608da6a97d90f5015e2db7c28c5fe50..05cdf5ccb54b2f41ee4e45519e477ce0e9021a1b 100644 (file)
--- a/model.h
+++ b/model.h
@@ -48,6 +48,8 @@ public:
        Thread *get_thread(thread_id_t tid) { return thread_map[tid]; }
 
        void assign_id(Thread *t);
+
+       int switch_to_master(ModelAction *act);
 private:
        int used_thread_id;
        class ModelAction *current_action;

diff --git a/threads.cc b/threads.cc
index 38a0dce8775a4f3490f50163477582b43db6de76..397c7894b70291b10016d1d3774ea74f7c840c73 100644 (file)
--- a/threads.cc
+++ b/threads.cc
@@ -60,17 +60,6 @@ void Thread::dispose()
        stack_free(stack);
 }
 
-int Thread::switch_to_master(ModelAction *act)
-{
-       Thread *next;
-
-       DBG();
-       model->set_current_action(act);
-       state = THREAD_READY;
-       next = model->system_thread;
-       return swap(next);
-}
-
 Thread::Thread(thrd_t *t, void (*func)(), void *a) {
        int ret;
 

diff --git a/threads_internal.h b/threads_internal.h
index bdef9a5240ea16d0ad0be80aaff3ba1d7d9bf0d0..4c1e36a4115bd6b21f261491d368139ab987a6a8 100644 (file)
--- a/threads_internal.h
+++ b/threads_internal.h
@@ -20,7 +20,6 @@ public:
        Thread(thrd_t *t);
        int swap(Thread *t);
        void dispose();
-       int switch_to_master(ModelAction *act);
 
        thread_state get_state() { return state; }
        void set_state(thread_state s) { state = s; }