X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=threads.h;h=a97a04c704449963981fe443a711c64abc716fb3;hb=5d9ce304699f07a7203ca4ceb246b482720c031e;hp=ebe33a3631d3e6815b33ed12b1e47ba972f1a8b1;hpb=10df540dad6ba429731920c5e36638a3ac557eab;p=model-checker.git diff --git a/threads.h b/threads.h index ebe33a3..a97a04c 100644 --- a/threads.h +++ b/threads.h @@ -1,3 +1,7 @@ +/** @file threads.h + * @brief Model Checker Thread class. + */ + #ifndef __THREADS_H__ #define __THREADS_H__ @@ -16,6 +20,9 @@ typedef enum thread_state { THREAD_COMPLETED } thread_state; +class ModelAction; + +/** @brief A Thread is created for each user-space thread */ class Thread { public: Thread(thrd_t *t, void (*func)(void *), void *a); @@ -31,12 +38,16 @@ public: thrd_t get_thrd_t() { return *user_thread; } Thread * get_parent() { return parent; } + void set_creation(ModelAction *act) { creation = act; } + ModelAction * get_creation() { return creation; } + friend void thread_startup(); - MEMALLOC + SNAPSHOTALLOC private: int create_context(); Thread *parent; + ModelAction *creation; void (*start_routine)(void *); void *arg;