X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=threads-model.h;h=2cd09ab53739de7d327de3e5758af6b7ba66465d;hp=344d58badada9f13297a149c220c0f33d505238a;hb=745b71256a4b96ddf4843c7f66b11d0cb3daa3cb;hpb=a330eb33b1b62dfa71f3f0cb055367a30090c180 diff --git a/threads-model.h b/threads-model.h index 344d58ba..2cd09ab5 100644 --- a/threads-model.h +++ b/threads-model.h @@ -13,6 +13,11 @@ #include #include "modeltypes.h" +struct thread_params { + thrd_start_t func; + void *arg; +}; + /** @brief Represents the state of a user Thread */ typedef enum thread_state { /** Thread was just created and hasn't run yet */ @@ -36,7 +41,7 @@ class ModelAction; class Thread { public: Thread(thread_id_t tid); - Thread(thrd_t *t, void (*func)(void *), void *a); + Thread(thrd_t *t, void (*func)(void *), void *a, Thread *parent); ~Thread(); void complete(); @@ -90,8 +95,15 @@ public: return wait_list[i]; } + /** @return The pending (next) ModelAction for this Thread + * @see Thread::pending */ ModelAction * get_pending() const { return pending; } + + /** @brief Set the pending (next) ModelAction for this Thread + * @param act The pending ModelAction + * @see Thread::pending */ void set_pending(ModelAction *act) { pending = act; } + /** * Remove one ModelAction from the waiting list * @return The ModelAction that was removed from the waiting list @@ -114,10 +126,22 @@ public: */ private: int create_context(); - Thread *parent; + + /** @brief The parent Thread which created this Thread */ + Thread * const parent; + + /** @brief The THREAD_CREATE ModelAction which created this Thread */ ModelAction *creation; + /** + * @brief The next ModelAction to be run by this Thread + * + * This action should be kept updated by the ModelChecker, so that we + * always know what the next ModelAction's memory_order, action type, + * and location are. + */ ModelAction *pending; + void (*start_routine)(void *); void *arg; ucontext_t context; @@ -148,7 +172,7 @@ Thread * thread_current(); static inline thread_id_t thrd_to_id(thrd_t t) { - return t; + return t.priv->get_id(); } /**