c6ca076d734aa2460ed9efa1aa25cbe1aca04afa
[model-checker.git] / nodestack.cc
1 #include <string.h>
2
3 #include "nodestack.h"
4 #include "action.h"
5 #include "common.h"
6 #include "model.h"
7
8 /**
9  * @brief Node constructor
10  *
11  * Constructs a single Node for use in a NodeStack. Each Node is associated
12  * with exactly one ModelAction (exception: the first Node should be created
13  * as an empty stub, to represent the first thread "choice") and up to one
14  * parent.
15  *
16  * @param act The ModelAction to associate with this Node. May be NULL.
17  * @param par The parent Node in the NodeStack. May be NULL if there is no
18  * parent.
19  * @param nthreads The number of threads which exist at this point in the
20  * execution trace.
21  */
22 Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
23         : action(act),
24         parent(par),
25         num_threads(nthreads),
26         explored_children(num_threads),
27         backtrack(num_threads),
28         fairness(num_threads),
29         numBacktracks(0),
30         enabled_array(NULL),
31         may_read_from(),
32         read_from_index(0),
33         future_values(),
34         future_index(-1)
35 {
36         if (act) {
37                 act->set_node(this);
38                 int currtid=id_to_int(act->get_tid());
39                 int prevtid=(prevfairness != NULL)?id_to_int(prevfairness->action->get_tid()):0;
40                 
41                 if ( model->params.fairwindow != 0 ) {
42                         for(int i=0;i<nthreads;i++) {
43                                 ASSERT(i<((int)fairness.size()));
44                                 struct fairness_info * fi=& fairness[i];
45                                 struct fairness_info * prevfi=(par!=NULL)&&(i<par->get_num_threads())?&par->fairness[i]:NULL;
46                                 if (prevfi) {
47                                         *fi=*prevfi;
48                                 }
49                                 if (parent->enabled_array[i]) {
50                                         fi->enabled_count++;
51                                 }
52                                 if (i==currtid) {
53                                         fi->turns++;
54                                         fi->priority = false;
55                                 }
56                                 //Do window processing
57                                 if (prevfairness != NULL) {
58                                         if (prevfairness -> parent->enabled_array[i])
59                                                 fi->enabled_count--;
60                                         if (i==prevtid) {
61                                                 fi->turns--;
62                                         }
63                                         //Need full window to start evaluating conditions
64                                         //If we meet the enabled count and have no turns, give us priority
65                                         if ((fi->enabled_count >= model->params.enabledcount) &&
66                                                         (fi->turns == 0))
67                                                 fi->priority = true;
68                                 }
69                         }
70                 }
71         }
72 }
73
74 /** @brief Node desctructor */
75 Node::~Node()
76 {
77         if (action)
78                 delete action;
79         if (enabled_array)
80                 model_free(enabled_array);
81 }
82
83 /** Prints debugging info for the ModelAction associated with this Node */
84 void Node::print()
85 {
86         if (action)
87                 action->print();
88         else
89                 printf("******** empty action ********\n");
90 }
91
92 /** @brief Prints info about may_read_from set */
93 void Node::print_may_read_from()
94 {
95         for (unsigned int i = 0; i < may_read_from.size(); i++)
96                 may_read_from[i]->print();
97 }
98
99 /**
100  * Sets a promise to explore meeting with the given node.
101  * @param i is the promise index.
102  */
103 void Node::set_promise(unsigned int i) {
104         if (i >= promises.size())
105                 promises.resize(i + 1, PROMISE_IGNORE);
106         if (promises[i] == PROMISE_IGNORE)
107                 promises[i] = PROMISE_UNFULFILLED;
108 }
109
110 /**
111  * Looks up whether a given promise should be satisfied by this node.
112  * @param i The promise index.
113  * @return true if the promise should be satisfied by the given model action.
114  */
115 bool Node::get_promise(unsigned int i) {
116         return (i < promises.size()) && (promises[i] == PROMISE_FULFILLED);
117 }
118
119 /**
120  * Increments to the next combination of promises.
121  * @return true if we have a valid combination.
122  */
123 bool Node::increment_promise() {
124         DBG();
125
126         for (unsigned int i = 0; i < promises.size(); i++) {
127                 if (promises[i] == PROMISE_UNFULFILLED) {
128                         promises[i] = PROMISE_FULFILLED;
129                         while (i > 0) {
130                                 i--;
131                                 if (promises[i] == PROMISE_FULFILLED)
132                                         promises[i] = PROMISE_UNFULFILLED;
133                         }
134                         return true;
135                 }
136         }
137         return false;
138 }
139
140 /**
141  * Returns whether the promise set is empty.
142  * @return true if we have explored all promise combinations.
143  */
144 bool Node::promise_empty() {
145         for (unsigned int i = 0; i < promises.size();i++)
146                 if (promises[i] == PROMISE_UNFULFILLED)
147                         return false;
148         return true;
149 }
150
151 /**
152  * Adds a value from a weakly ordered future write to backtrack to.
153  * @param value is the value to backtrack to.
154  */
155 bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
156         int suitableindex=-1;
157         for (unsigned int i = 0; i < future_values.size(); i++) {
158                 if (future_values[i].value == value) {
159                         if (future_values[i].expiration>=expiration)
160                                 return false;
161                         if (future_index < ((int) i)) {
162                                 suitableindex=i;
163                         }
164                 }
165         }
166
167         if (suitableindex!=-1) {
168                 future_values[suitableindex].expiration=expiration;
169                 return true;
170         }
171         struct future_value newfv={value, expiration};
172         future_values.push_back(newfv);
173         return true;
174 }
175
176 /**
177  * Checks whether the future_values set for this node is empty.
178  * @return true if the future_values set is empty.
179  */
180 bool Node::future_value_empty() {
181         return ((future_index + 1) >= ((int)future_values.size()));
182 }
183
184 /**
185  * Checks if the Thread associated with this thread ID has been explored from
186  * this Node already.
187  * @param tid is the thread ID to check
188  * @return true if this thread choice has been explored already, false
189  * otherwise
190  */
191 bool Node::has_been_explored(thread_id_t tid)
192 {
193         int id = id_to_int(tid);
194         return explored_children[id];
195 }
196
197 /**
198  * Checks if the backtracking set is empty.
199  * @return true if the backtracking set is empty
200  */
201 bool Node::backtrack_empty()
202 {
203         return (numBacktracks == 0);
204 }
205
206 /**
207  * Checks whether the readsfrom set for this node is empty.
208  * @return true if the readsfrom set is empty.
209  */
210 bool Node::read_from_empty() {
211         return ((read_from_index+1) >= may_read_from.size());
212 }
213
214 /**
215  * Mark the appropriate backtracking information for exploring a thread choice.
216  * @param act The ModelAction to explore
217  */
218 void Node::explore_child(ModelAction *act, bool * is_enabled)
219 {
220         if ( ! enabled_array )
221                 enabled_array=(bool *)model_malloc(sizeof(bool)*num_threads);
222         if (is_enabled != NULL)
223                 memcpy(enabled_array, is_enabled, sizeof(bool)*num_threads);
224         else {
225                 for(int i=0;i<num_threads;i++)
226                         enabled_array[i]=false;
227         }
228
229         explore(act->get_tid());
230 }
231
232 /**
233  * Records a backtracking reference for a thread choice within this Node.
234  * Provides feedback as to whether this thread choice is already set for
235  * backtracking.
236  * @return false if the thread was already set to be backtracked, true
237  * otherwise
238  */
239 bool Node::set_backtrack(thread_id_t id)
240 {
241         int i = id_to_int(id);
242         if (backtrack[i])
243                 return false;
244         backtrack[i] = true;
245         numBacktracks++;
246         return true;
247 }
248
249 thread_id_t Node::get_next_backtrack()
250 {
251         /** @todo Find next backtrack */
252         unsigned int i;
253         for (i = 0; i < backtrack.size(); i++)
254                 if (backtrack[i] == true)
255                         break;
256         /* Backtrack set was empty? */
257         ASSERT(i != backtrack.size());
258
259         backtrack[i] = false;
260         numBacktracks--;
261         return int_to_id(i);
262 }
263
264 bool Node::is_enabled(Thread *t)
265 {
266         int thread_id=id_to_int(t->get_id());
267         return thread_id < num_threads && enabled_array[thread_id];
268 }
269
270 bool Node::is_enabled(thread_id_t tid)
271 {
272         int thread_id=id_to_int(tid);
273         return thread_id < num_threads && enabled_array[thread_id];
274 }
275
276 bool Node::has_priority(thread_id_t tid)
277 {
278         return fairness[id_to_int(tid)].priority;
279 }
280
281 /**
282  * Add an action to the may_read_from set.
283  * @param act is the action to add
284  */
285 void Node::add_read_from(const ModelAction *act)
286 {
287         may_read_from.push_back(act);
288 }
289
290 /**
291  * Gets the next 'future_value' value from this Node. Only valid for a node
292  * where this->action is a 'read'.
293  * @return The first element in future_values
294  */
295 uint64_t Node::get_future_value() {
296         ASSERT(future_index<((int)future_values.size()));
297         return future_values[future_index].value;
298 }
299
300 modelclock_t Node::get_future_value_expiration() {
301         ASSERT(future_index<((int)future_values.size()));
302         return future_values[future_index].expiration;
303 }
304
305
306 int Node::get_read_from_size() {
307         return may_read_from.size();
308 }
309
310 const ModelAction * Node::get_read_from_at(int i) {
311         return may_read_from[i];
312 }
313
314 /**
315  * Gets the next 'may_read_from' action from this Node. Only valid for a node
316  * where this->action is a 'read'.
317  * @return The first element in may_read_from
318  */
319 const ModelAction * Node::get_read_from() {
320         if (read_from_index < may_read_from.size())
321                 return may_read_from[read_from_index];
322         else
323                 return NULL;
324 }
325
326 /**
327  * Increments the index into the readsfrom set to explore the next item.
328  * @return Returns false if we have explored all items.
329  */
330 bool Node::increment_read_from() {
331         DBG();
332         promises.clear();
333         if (read_from_index < may_read_from.size()) {
334                 read_from_index++;
335                 return read_from_index < may_read_from.size();
336         }
337         return false;
338 }
339
340 /**
341  * Increments the index into the future_values set to explore the next item.
342  * @return Returns false if we have explored all values.
343  */
344 bool Node::increment_future_value() {
345         DBG();
346         promises.clear();
347         if (future_index < ((int)future_values.size())) {
348                 future_index++;
349                 return (future_index < ((int)future_values.size()));
350         }
351         return false;
352 }
353
354 void Node::explore(thread_id_t tid)
355 {
356         int i = id_to_int(tid);
357         if (backtrack[i]) {
358                 backtrack[i] = false;
359                 numBacktracks--;
360         }
361         explored_children[i] = true;
362 }
363
364 NodeStack::NodeStack()
365         : total_nodes(0)
366 {
367         node_list.push_back(new Node());
368         total_nodes++;
369         iter = 0;
370 }
371
372 NodeStack::~NodeStack()
373 {
374 }
375
376 void NodeStack::print()
377 {
378         printf("............................................\n");
379         printf("NodeStack printing node_list:\n");
380         for (unsigned int it = 0; it < node_list.size(); it++) {
381                 if (it == this->iter)
382                         printf("vvv following action is the current iterator vvv\n");
383                 node_list[it]->print();
384         }
385         printf("............................................\n");
386 }
387
388 /** Note: The is_enabled set contains what actions were enabled when
389  *  act was chosen. */
390
391 ModelAction * NodeStack::explore_action(ModelAction *act, bool * is_enabled)
392 {
393         DBG();
394
395         ASSERT(!node_list.empty());
396
397         if ((iter+1) < node_list.size()) {
398                 iter++;
399                 return node_list[iter]->get_action();
400         }
401
402         /* Record action */
403         get_head()->explore_child(act, is_enabled);
404         Node *prevfairness = NULL;
405         if ( model->params.fairwindow != 0 && iter > model->params.fairwindow ) {
406                 prevfairness = node_list[iter-model->params.fairwindow];
407         }
408         node_list.push_back(new Node(act, get_head(), model->get_num_threads(), prevfairness));
409         total_nodes++;
410         iter++;
411         return NULL;
412 }
413
414 /**
415  * Empties the stack of all trailing nodes after a given position and calls the
416  * destructor for each. This function is provided an offset which determines
417  * how many nodes (relative to the current replay state) to save before popping
418  * the stack.
419  * @param numAhead gives the number of Nodes (including this Node) to skip over
420  * before removing nodes.
421  */
422 void NodeStack::pop_restofstack(int numAhead)
423 {
424         /* Diverging from previous execution; clear out remainder of list */
425         unsigned int it=iter+numAhead;
426         for(unsigned int i=it;i<node_list.size();i++)
427                 delete node_list[i];
428         node_list.resize(it);
429 }
430
431 Node * NodeStack::get_head()
432 {
433         if (node_list.empty())
434                 return NULL;
435         return node_list[iter];
436 }
437
438 Node * NodeStack::get_next()
439 {
440         if (node_list.empty()) {
441                 DEBUG("Empty\n");
442                 return NULL;
443         }
444         unsigned int it=iter+1;
445         if (it == node_list.size()) {
446                 DEBUG("At end\n");
447                 return NULL;
448         }
449         return node_list[it];
450 }
451
452 void NodeStack::reset_execution()
453 {
454         iter = 0;
455 }