threads: don't make direct call into scheduler
[model-checker.git] / threads.cc
1 #include <stdlib.h>
2
3 #include "libthreads.h"
4 #include "schedule.h"
5 #include "common.h"
6 #include "threads.h"
7
8 /* global "model" object */
9 #include "model.h"
10
11 #define STACK_SIZE (1024 * 1024)
12
13 static void * stack_allocate(size_t size)
14 {
15         return malloc(size);
16 }
17
18 static void stack_free(void *stack)
19 {
20         free(stack);
21 }
22
23 Thread * thread_current(void)
24 {
25         return model->scheduler->get_current_thread();
26 }
27
28 int Thread::create_context()
29 {
30         int ret;
31
32         ret = getcontext(&context);
33         if (ret)
34                 return ret;
35
36         /* start_routine == NULL means this is our initial context */
37         if (!start_routine)
38                 return 0;
39
40         /* Initialize new managed context */
41         stack = stack_allocate(STACK_SIZE);
42         context.uc_stack.ss_sp = stack;
43         context.uc_stack.ss_size = STACK_SIZE;
44         context.uc_stack.ss_flags = 0;
45         context.uc_link = &model->system_thread->context;
46         makecontext(&context, start_routine, 1, arg);
47
48         return 0;
49 }
50
51 int Thread::swap(Thread *t)
52 {
53         return swapcontext(&this->context, &t->context);
54 }
55
56 void Thread::dispose()
57 {
58         DEBUG("completed thread %d\n", thread_current()->get_id());
59         state = THREAD_COMPLETED;
60         stack_free(stack);
61 }
62
63 Thread::Thread(thrd_t *t, void (*func)(), void *a) {
64         int ret;
65
66         user_thread = t;
67         start_routine = func;
68         arg = a;
69
70         /* Initialize state */
71         ret = create_context();
72         if (ret)
73                 printf("Error in create_context\n");
74
75         state = THREAD_CREATED;
76         id = model->get_next_id();
77         *user_thread = id;
78 }
79
80 Thread::Thread(thrd_t *t) {
81         /* system thread */
82         user_thread = t;
83         start_routine = NULL;
84         arg = NULL;
85
86         state = THREAD_CREATED;
87         id = model->get_next_id();
88         *user_thread = id;
89         create_context();
90         model->add_system_thread(this);
91 }
92
93 thread_id_t Thread::get_id()
94 {
95         return id;
96 }
97
98 /*
99  * Return 1 if found next thread, 0 otherwise
100  */
101 static int thread_system_next(void)
102 {
103         Thread *curr, *next;
104
105         curr = thread_current();
106         model->check_current_action();
107         if (curr) {
108                 if (curr->get_state() == THREAD_READY)
109                         model->scheduler->add_thread(curr);
110                 else if (curr->get_state() == THREAD_RUNNING)
111                         /* Stopped while running; i.e., completed */
112                         curr->dispose();
113                 else
114                         DEBUG("ERROR: current thread in unexpected state??\n");
115         }
116         next = model->scheduler->next_thread();
117         if (next)
118                 next->set_state(THREAD_RUNNING);
119         DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
120         if (!next)
121                 return 1;
122         return model->system_thread->swap(next);
123 }
124
125 static void thread_wait_finish(void)
126 {
127
128         DBG();
129
130         while (!thread_system_next());
131 }
132
133 /*
134  * Main system function
135  */
136 int main()
137 {
138         thrd_t user_thread, main_thread;
139         Thread *th;
140
141         model = new ModelChecker();
142
143         th = new Thread(&main_thread);
144
145         do {
146                 /* Start user program */
147                 thrd_create(&user_thread, &user_main, NULL);
148
149                 /* Wait for all threads to complete */
150                 thread_wait_finish();
151
152                 model->print_trace();
153         } while (model->next_execution());
154
155         delete th;
156         delete model;
157
158         DEBUG("Exiting\n");
159         return 0;
160 }