X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=blobdiff_plain;f=threads-model.h;h=2cd09ab53739de7d327de3e5758af6b7ba66465d;hp=d4d2da29e82a7fc1c58a2a61db7ee61aac7206a5;hb=ad52dcdb3a75a69242a392165934e942cb76513b;hpb=82df62c2b0805848b87bb71df5b66a4a66f8e25d diff --git a/threads-model.h b/threads-model.h index d4d2da29..2cd09ab5 100644 --- a/threads-model.h +++ b/threads-model.h @@ -41,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(); @@ -95,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 @@ -119,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;