threads_internal: pass the current 'action' to the internal thread system

I build a ModelAction object to represent the properties of the current action
that are relevant to the model checker. This action should be passed from the
basic action (atomic_load, atomic_store, thread_yield, etc.) into our thread
library and eventually to the model checker.

I don't use these actions yet, but they will be shortly.

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

diff --git a/libthreads.cc b/libthreads.cc
index 42e91989f6bdd42cb9ba7883ba1c6a0924eeb7e1..fb828b18aa079e2d726d0cfc851600d7ec6d53d0 100644 (file)
--- a/libthreads.cc
+++ b/libthreads.cc
@@ -98,11 +98,12 @@ static void thread_wait_finish(void)
        while (!thread_system_next());
 }
 
-int thread_switch_to_master()
+int thread_switch_to_master(ModelAction *act)
 {
        struct thread *old, *next;
 
        DBG();
+       model->set_current_action(act);
        old = thread_current();
        old->state = THREAD_READY;
        next = model->system_thread;
@@ -140,12 +141,14 @@ void thread_join(struct thread *t)
 {
        int ret = 0;
        while (t->state != THREAD_COMPLETED && !ret)
-               ret = thread_switch_to_master();
+               /* seq_cst is just a 'don't care' parameter */
+               ret = thread_switch_to_master(new ModelAction(THREAD_JOIN, memory_order_seq_cst, NULL, VALUE_NONE));
 }
 
 int thread_yield(void)
 {
-       return thread_switch_to_master();
+       /* seq_cst is just a 'don't care' parameter */
+       return thread_switch_to_master(new ModelAction(THREAD_YIELD, memory_order_seq_cst, NULL, VALUE_NONE));
 }
 
 struct thread *thread_current(void)

diff --git a/model.cc b/model.cc
index 19194cda06a766ccb84b1674b6fb5142bcc4bef4..88d5ce32e21195d7106c291220d4eb2af7bb80a0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -11,6 +11,8 @@ ModelChecker::ModelChecker()
        this->used_thread_id = 0;
        /* Initialize default scheduler */
        this->scheduler = new DefaultScheduler();
+
+       this->current_action = NULL;
 }
 
 ModelChecker::~ModelChecker()

diff --git a/model.h b/model.h
index d3229b296526db6ee54c07d0055e22a336011b5a..205b8d0bd236989a6131efa45cdefba0f7cc1096 100644 (file)
--- a/model.h
+++ b/model.h
@@ -37,8 +37,11 @@ public:
        void add_system_thread(struct thread *t);
        void assign_id(struct thread *t);
 
+       void set_current_action(ModelAction *act) { current_action = act; }
+
 private:
        int used_thread_id;
+       class ModelAction *current_action;
 };
 
 extern ModelChecker *model;

diff --git a/threads_internal.h b/threads_internal.h
index 37b446c0227591438d2257439c61857bce2e68fe..0fde64b768bb2cb7f37efc943fca5c4a42b8e3ca 100644 (file)
--- a/threads_internal.h
+++ b/threads_internal.h
@@ -1,8 +1,9 @@
 #ifndef __THREADS_INTERNAL_H__
 #define __THREADS_INTERNAL_H__
 
+#include "model.h"
 #include "libthreads.h"
 
-int thread_switch_to_master();
+int thread_switch_to_master(ModelAction *act);
 
 #endif /* __THREADS_INTERNAL_H__ */