Merge branch 'master' of ssh://demsky.eecs.uci.edu/home/git/model-checker
[model-checker.git] / schedule.cc
1 #include <string.h>
2 #include <stdlib.h>
3
4 #include "threads-model.h"
5 #include "schedule.h"
6 #include "common.h"
7 #include "model.h"
8 #include "nodestack.h"
9
10 /** Constructor */
11 Scheduler::Scheduler() :
12         enabled(NULL),
13         enabled_len(0),
14         curr_thread_index(0),
15         current(NULL)
16 {
17 }
18
19 void Scheduler::set_enabled(Thread *t, enabled_type_t enabled_status) {
20         int threadid=id_to_int(t->get_id());
21         if (threadid>=enabled_len) {
22                 enabled_type_t *new_enabled = (enabled_type_t *)snapshot_malloc(sizeof(enabled_type_t) * (threadid + 1));
23                 memset(&new_enabled[enabled_len], 0, (threadid+1-enabled_len)*sizeof(enabled_type_t));
24                 if (enabled != NULL) {
25                         memcpy(new_enabled, enabled, enabled_len*sizeof(enabled_type_t));
26                         snapshot_free(enabled);
27                 }
28                 enabled=new_enabled;
29                 enabled_len=threadid+1;
30         }
31         enabled[threadid]=enabled_status;
32 }
33
34 /**
35  * @brief Check if a Thread is currently enabled
36  * @param t The Thread to check
37  * @return True if the Thread is currently enabled
38  */
39 bool Scheduler::is_enabled(Thread *t) const
40 {
41         int id = id_to_int(t->get_id());
42         return (id >= enabled_len) ? false : (enabled[id] != THREAD_DISABLED);
43 }
44
45 enabled_type_t Scheduler::get_enabled(Thread *t) {
46         int id = id_to_int(t->get_id());
47         ASSERT(id<enabled_len);
48         return enabled[id];
49 }
50
51 void Scheduler::update_sleep_set(Node *n) {
52         enabled_type_t *enabled_array=n->get_enabled_array();
53         for(int i=0;i<enabled_len;i++) {
54                 if (enabled_array[i]==THREAD_SLEEP_SET) {
55                         enabled[i]=THREAD_SLEEP_SET;
56                 }
57         }
58 }
59
60 /**
61  * Add a Thread to the sleep set.
62  * @param t The Thread to add
63  */
64 void Scheduler::add_sleep(Thread *t)
65 {
66         DEBUG("thread %d\n", id_to_int(t->get_id()));
67         set_enabled(t, THREAD_SLEEP_SET);
68 }
69
70 /**
71  * Remove a Thread from the sleep set.
72  * @param t The Thread to remove
73  */
74 void Scheduler::remove_sleep(Thread *t)
75 {
76         DEBUG("thread %d\n", id_to_int(t->get_id()));
77         set_enabled(t, THREAD_ENABLED);
78 }
79
80 /**
81  * Add a Thread to the scheduler's ready list.
82  * @param t The Thread to add
83  */
84 void Scheduler::add_thread(Thread *t)
85 {
86         DEBUG("thread %d\n", id_to_int(t->get_id()));
87         ASSERT(!t->is_model_thread());
88         set_enabled(t, THREAD_ENABLED);
89 }
90
91 /**
92  * Remove a given Thread from the scheduler.
93  * @param t The Thread to remove
94  */
95 void Scheduler::remove_thread(Thread *t)
96 {
97         if (current == t)
98                 current = NULL;
99         set_enabled(t, THREAD_DISABLED);
100 }
101
102 /**
103  * Prevent a Thread from being scheduled. The sleeping Thread should be
104  * re-awoken via Scheduler::wake.
105  * @param thread The Thread that should sleep
106  */
107 void Scheduler::sleep(Thread *t)
108 {
109         set_enabled(t, THREAD_DISABLED);
110         t->set_state(THREAD_BLOCKED);
111 }
112
113 /**
114  * Wake a Thread up that was previously waiting (see Scheduler::wait)
115  * @param t The Thread to wake up
116  */
117 void Scheduler::wake(Thread *t)
118 {
119         ASSERT(!t->is_model_thread());
120         set_enabled(t, THREAD_ENABLED);
121         t->set_state(THREAD_READY);
122 }
123
124 /**
125  * Select a Thread. This implementation defaults to round-robin, if a
126  * thread is not already provided.
127  *
128  * @param t Thread to run, if chosen by an external entity (e.g.,
129  * ModelChecker). May be NULL to indicate no external choice.
130  * @return The next Thread to run
131  */
132 Thread * Scheduler::next_thread(Thread *t)
133 {
134         if ( t == NULL ) {
135                 int old_curr_thread = curr_thread_index;
136                 bool have_enabled_thread_with_priority=false;
137                 Node *n=model->get_curr_node();
138
139                 for(int i=0;i<enabled_len;i++) {
140                         thread_id_t tid=int_to_id(i);
141                         if (n->has_priority(tid)) {
142                                 //Have a thread with priority
143                                 if (enabled[i]!=THREAD_DISABLED)
144                                         have_enabled_thread_with_priority=true;
145                         }
146                 }
147
148                 while(true) {
149                         curr_thread_index = (curr_thread_index+1) % enabled_len;
150                         thread_id_t curr_tid=int_to_id(curr_thread_index);
151                         if (enabled[curr_thread_index]==THREAD_ENABLED&&
152                                         (!have_enabled_thread_with_priority||n->has_priority(curr_tid))) {
153                                 t = model->get_thread(curr_tid);
154                                 break;
155                         }
156                         if (curr_thread_index == old_curr_thread) {
157                                 print();
158                                 return NULL;
159                         }
160                 }
161         } else if (t->is_model_thread()) {
162                 /* model-checker threads never run */
163                 t = NULL;
164         } else {
165                 curr_thread_index = id_to_int(t->get_id());
166         }
167
168         current = t;
169         print();
170         return t;
171 }
172
173 /**
174  * @return The currently-running Thread
175  */
176 Thread * Scheduler::get_current_thread() const
177 {
178         ASSERT(!current || !current->is_model_thread());
179         return current;
180 }
181
182 /**
183  * Print debugging information about the current state of the scheduler. Only
184  * prints something if debugging is enabled.
185  */
186 void Scheduler::print() const
187 {
188         if (current)
189                 DEBUG("Current thread: %d\n", id_to_int(current->get_id()));
190         else
191                 DEBUG("No current thread\n");
192 }