cyclegraph: template-ize checkReachable()
[model-checker.git] / threads.cc
1 /** @file threads.cc
2  *  @brief Thread functions.
3  */
4
5 #include <string.h>
6
7 #include <threads.h>
8 #include "common.h"
9 #include "threads-model.h"
10
11 /* global "model" object */
12 #include "model.h"
13
14 /** Allocate a stack for a new thread. */
15 static void * stack_allocate(size_t size)
16 {
17         return snapshot_malloc(size);
18 }
19
20 /** Free a stack for a terminated thread. */
21 static void stack_free(void *stack)
22 {
23         snapshot_free(stack);
24 }
25
26 /** Return the currently executing thread. */
27 Thread * thread_current(void)
28 {
29         ASSERT(model);
30         return model->get_current_thread();
31 }
32
33 /**
34  * Provides a startup wrapper for each thread, allowing some initial
35  * model-checking data to be recorded. This method also gets around makecontext
36  * not being 64-bit clean
37  */
38 void thread_startup()
39 {
40         Thread * curr_thread = thread_current();
41
42         /* Add dummy "start" action, just to create a first clock vector */
43         model->switch_to_master(new ModelAction(THREAD_START, std::memory_order_seq_cst, curr_thread));
44
45         /* Call the actual thread function */
46         curr_thread->start_routine(curr_thread->arg);
47
48         /* Finish thread properly */
49         model->switch_to_master(new ModelAction(THREAD_FINISH, std::memory_order_seq_cst, curr_thread));
50 }
51
52 /**
53  * Create a thread context for a new thread so we can use
54  * setcontext/getcontext/swapcontext to swap it out.
55  * @return 0 on success; otherwise, non-zero error condition
56  */
57 int Thread::create_context()
58 {
59         int ret;
60
61         ret = getcontext(&context);
62         if (ret)
63                 return ret;
64
65         /* Initialize new managed context */
66         stack = stack_allocate(STACK_SIZE);
67         context.uc_stack.ss_sp = stack;
68         context.uc_stack.ss_size = STACK_SIZE;
69         context.uc_stack.ss_flags = 0;
70         context.uc_link = model->get_system_context();
71         makecontext(&context, thread_startup, 0);
72
73         return 0;
74 }
75
76 /**
77  * Swaps the current context to another thread of execution. This form switches
78  * from a user Thread to a system context.
79  * @param t Thread representing the currently-running thread. The current
80  * context is saved here.
81  * @param ctxt Context to which we will swap. Must hold a valid system context.
82  * @return Does not return, unless we return to Thread t's context. See
83  * swapcontext(3) (returns 0 for success, -1 for failure).
84  */
85 int Thread::swap(Thread *t, ucontext_t *ctxt)
86 {
87         return swapcontext(&t->context, ctxt);
88 }
89
90 /**
91  * Swaps the current context to another thread of execution. This form switches
92  * from a system context to a user Thread.
93  * @param ctxt System context variable to which to save the current context.
94  * @param t Thread to which we will swap. Must hold a valid user context.
95  * @return Does not return, unless we return to the system context (ctxt). See
96  * swapcontext(3) (returns 0 for success, -1 for failure).
97  */
98 int Thread::swap(ucontext_t *ctxt, Thread *t)
99 {
100         return swapcontext(ctxt, &t->context);
101 }
102
103
104 /** Terminate a thread and free its stack. */
105 void Thread::complete()
106 {
107         ASSERT(!is_complete());
108         DEBUG("completed thread %d\n", id_to_int(get_id()));
109         state = THREAD_COMPLETED;
110         if (stack)
111                 stack_free(stack);
112 }
113
114 /**
115  * @brief Construct a new model-checker Thread
116  *
117  * A model-checker Thread is used for accounting purposes only. It will never
118  * have its own stack, and it should never be inserted into the Scheduler.
119  *
120  * @param tid The thread ID to assign
121  */
122 Thread::Thread(thread_id_t tid) :
123         parent(NULL),
124         creation(NULL),
125         pending(NULL),
126         start_routine(NULL),
127         arg(NULL),
128         stack(NULL),
129         user_thread(NULL),
130         id(tid),
131         state(THREAD_READY), /* Thread is always ready? */
132         wait_list(),
133         last_action_val(0),
134         model_thread(true)
135 {
136         memset(&context, 0, sizeof(context));
137 }
138
139 /**
140  * Construct a new thread.
141  * @param t The thread identifier of the newly created thread.
142  * @param func The function that the thread will call.
143  * @param a The parameter to pass to this function.
144  */
145 Thread::Thread(thrd_t *t, void (*func)(void *), void *a) :
146         creation(NULL),
147         pending(NULL),
148         start_routine(func),
149         arg(a),
150         user_thread(t),
151         state(THREAD_CREATED),
152         wait_list(),
153         last_action_val(VALUE_NONE),
154         model_thread(false)
155 {
156         int ret;
157
158         /* Initialize state */
159         ret = create_context();
160         if (ret)
161                 model_print("Error in create_context\n");
162
163         id = model->get_next_id();
164         user_thread->priv = this;
165         parent = thread_current();
166 }
167
168 /** Destructor */
169 Thread::~Thread()
170 {
171         if (!is_complete())
172                 complete();
173         model->remove_thread(this);
174 }
175
176 /** @return The thread_id_t corresponding to this Thread object. */
177 thread_id_t Thread::get_id() const
178 {
179         return id;
180 }
181
182 /**
183  * Set a thread's THREAD_* state (@see thread_state)
184  * @param s The state to enter
185  */
186 void Thread::set_state(thread_state s)
187 {
188         ASSERT(s == THREAD_COMPLETED || state != THREAD_COMPLETED);
189         state = s;
190 }