nodestack: don't create empty base node
[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 #include "threads-model.h"
8
9 /**
10  * @brief Node constructor
11  *
12  * Constructs a single Node for use in a NodeStack. Each Node is associated
13  * with exactly one ModelAction (exception: the first Node should be created
14  * as an empty stub, to represent the first thread "choice") and up to one
15  * parent.
16  *
17  * @param act The ModelAction to associate with this Node. May be NULL.
18  * @param par The parent Node in the NodeStack. May be NULL if there is no
19  * parent.
20  * @param nthreads The number of threads which exist at this point in the
21  * execution trace.
22  */
23 Node::Node(ModelAction *act, Node *par, int nthreads, Node *prevfairness)
24         : action(act),
25         parent(par),
26         num_threads(nthreads),
27         explored_children(num_threads),
28         backtrack(num_threads),
29         fairness(num_threads),
30         numBacktracks(0),
31         enabled_array(NULL),
32         may_read_from(),
33         read_from_index(0),
34         future_values(),
35         future_index(-1),
36         relseq_break_writes(),
37         relseq_break_index(0),
38         misc_index(0),
39         misc_max(0)
40 {
41         if (act) {
42                 act->set_node(this);
43                 int currtid = id_to_int(act->get_tid());
44                 int prevtid = (prevfairness != NULL) ? id_to_int(prevfairness->action->get_tid()) : 0;
45
46                 if (model->params.fairwindow != 0) {
47                         for (int i = 0; i < nthreads; i++) {
48                                 ASSERT(i < ((int)fairness.size()));
49                                 struct fairness_info *fi = &fairness[i];
50                                 struct fairness_info *prevfi = (par != NULL) && (i < par->get_num_threads()) ? &par->fairness[i] : NULL;
51                                 if (prevfi) {
52                                         *fi = *prevfi;
53                                 }
54                                 if (parent && parent->is_enabled(int_to_id(i))) {
55                                         fi->enabled_count++;
56                                 }
57                                 if (i == currtid) {
58                                         fi->turns++;
59                                         fi->priority = false;
60                                 }
61                                 /* Do window processing */
62                                 if (prevfairness != NULL) {
63                                         if (prevfairness->parent->is_enabled(int_to_id(i)))
64                                                 fi->enabled_count--;
65                                         if (i == prevtid) {
66                                                 fi->turns--;
67                                         }
68                                         /* Need full window to start evaluating
69                                          * conditions
70                                          * If we meet the enabled count and
71                                          * have no turns, give us priority */
72                                         if ((fi->enabled_count >= model->params.enabledcount) &&
73                                                         (fi->turns == 0))
74                                                 fi->priority = true;
75                                 }
76                         }
77                 }
78         }
79 }
80
81 /** @brief Node desctructor */
82 Node::~Node()
83 {
84         if (action)
85                 delete action;
86         if (enabled_array)
87                 model_free(enabled_array);
88 }
89
90 /** Prints debugging info for the ModelAction associated with this Node */
91 void Node::print()
92 {
93         if (action) {
94                 action->print();
95                 model_print("          backtrack: %s\n", backtrack_empty() ? "empty" : "non-empty");
96                 model_print("          future values: %s\n", future_value_empty() ? "empty" : "non-empty");
97                 model_print("          read-from: %s\n", read_from_empty() ? "empty" : "non-empty");
98                 model_print("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
99                 model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
100                 model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
101         } else
102                 model_print("******** empty action ********\n");
103 }
104
105 /** @brief Prints info about may_read_from set */
106 void Node::print_may_read_from()
107 {
108         for (unsigned int i = 0; i < may_read_from.size(); i++)
109                 may_read_from[i]->print();
110 }
111
112 /**
113  * Sets a promise to explore meeting with the given node.
114  * @param i is the promise index.
115  */
116 void Node::set_promise(unsigned int i, bool is_rmw) {
117         if (i >= promises.size())
118                 promises.resize(i + 1, PROMISE_IGNORE);
119         if (promises[i] == PROMISE_IGNORE) {
120                 promises[i] = PROMISE_UNFULFILLED;
121                 if (is_rmw)
122                         promises[i] |= PROMISE_RMW;
123         }
124 }
125
126 /**
127  * Looks up whether a given promise should be satisfied by this node.
128  * @param i The promise index.
129  * @return true if the promise should be satisfied by the given model action.
130  */
131 bool Node::get_promise(unsigned int i) const
132 {
133         return (i < promises.size()) && ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED);
134 }
135
136 /**
137  * Increments to the next combination of promises.
138  * @return true if we have a valid combination.
139  */
140 bool Node::increment_promise() {
141         DBG();
142         unsigned int rmw_count = 0;
143         for (unsigned int i = 0; i < promises.size(); i++) {
144                 if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED))
145                         rmw_count++;
146         }
147
148         for (unsigned int i = 0; i < promises.size(); i++) {
149                 if ((promises[i] & PROMISE_MASK) == PROMISE_UNFULFILLED) {
150                         if ((rmw_count > 0) && (promises[i] & PROMISE_RMW)) {
151                                 //sending our value to two rmws... not going to work..try next combination
152                                 continue;
153                         }
154                         promises[i] = (promises[i] & PROMISE_RMW) |PROMISE_FULFILLED;
155                         while (i > 0) {
156                                 i--;
157                                 if ((promises[i] & PROMISE_MASK) == PROMISE_FULFILLED)
158                                         promises[i] = (promises[i] & PROMISE_RMW) | PROMISE_UNFULFILLED;
159                         }
160                         return true;
161                 } else if (promises[i] == (PROMISE_RMW|PROMISE_FULFILLED)) {
162                         rmw_count--;
163                 }
164         }
165         return false;
166 }
167
168 /**
169  * Returns whether the promise set is empty.
170  * @return true if we have explored all promise combinations.
171  */
172 bool Node::promise_empty() const
173 {
174         bool fulfilledrmw = false;
175         for (int i = promises.size() - 1; i >= 0; i--) {
176                 if (promises[i] == PROMISE_UNFULFILLED)
177                         return false;
178                 if (!fulfilledrmw && ((promises[i]&PROMISE_MASK) == PROMISE_UNFULFILLED))
179                         return false;
180                 if (promises[i] == (PROMISE_FULFILLED|PROMISE_RMW))
181                         fulfilledrmw = true;
182         }
183         return true;
184 }
185
186
187 void Node::set_misc_max(int i)
188 {
189         misc_max = i;
190 }
191
192 int Node::get_misc() const
193 {
194         return misc_index;
195 }
196
197 bool Node::increment_misc() {
198         return (misc_index < misc_max) && ((++misc_index) < misc_max);
199 }
200
201 bool Node::misc_empty() const
202 {
203         return (misc_index + 1) >= misc_max;
204 }
205
206
207 /**
208  * Adds a value from a weakly ordered future write to backtrack to. This
209  * operation may "fail" if the future value has already been run (within some
210  * sloppiness window of this expiration), or if the futurevalues set has
211  * reached its maximum.
212  * @see model_params.maxfuturevalues
213  *
214  * @param value is the value to backtrack to.
215  * @return True if the future value was successully added; false otherwise
216  */
217 bool Node::add_future_value(uint64_t value, modelclock_t expiration) {
218         int idx = -1; /* Highest index where value is found */
219         for (unsigned int i = 0; i < future_values.size(); i++) {
220                 if (future_values[i].value == value) {
221                         if (expiration <= future_values[i].expiration)
222                                 return false;
223                         idx = i;
224                 }
225         }
226         if (idx > future_index) {
227                 /* Future value hasn't been explored; update expiration */
228                 future_values[idx].expiration = expiration;
229                 return true;
230         } else if (idx >= 0 && expiration <= future_values[idx].expiration + model->params.expireslop) {
231                 /* Future value has been explored and is within the "sloppy" window */
232                 return false;
233         }
234
235         /* Limit the size of the future-values set */
236         if (model->params.maxfuturevalues > 0 &&
237                         (int)future_values.size() >= model->params.maxfuturevalues)
238                 return false;
239
240         struct future_value newfv = {value, expiration};
241         future_values.push_back(newfv);
242         return true;
243 }
244
245 /**
246  * Checks whether the future_values set for this node is empty.
247  * @return true if the future_values set is empty.
248  */
249 bool Node::future_value_empty() const
250 {
251         return ((future_index + 1) >= ((int)future_values.size()));
252 }
253
254 /**
255  * Checks if the Thread associated with this thread ID has been explored from
256  * this Node already.
257  * @param tid is the thread ID to check
258  * @return true if this thread choice has been explored already, false
259  * otherwise
260  */
261 bool Node::has_been_explored(thread_id_t tid) const
262 {
263         int id = id_to_int(tid);
264         return explored_children[id];
265 }
266
267 /**
268  * Checks if the backtracking set is empty.
269  * @return true if the backtracking set is empty
270  */
271 bool Node::backtrack_empty() const
272 {
273         return (numBacktracks == 0);
274 }
275
276 /**
277  * Checks whether the readsfrom set for this node is empty.
278  * @return true if the readsfrom set is empty.
279  */
280 bool Node::read_from_empty() const
281 {
282         return ((read_from_index + 1) >= may_read_from.size());
283 }
284
285 /**
286  * Mark the appropriate backtracking information for exploring a thread choice.
287  * @param act The ModelAction to explore
288  */
289 void Node::explore_child(ModelAction *act, enabled_type_t *is_enabled)
290 {
291         if (!enabled_array)
292                 enabled_array = (enabled_type_t *)model_malloc(sizeof(enabled_type_t) * num_threads);
293         if (is_enabled != NULL)
294                 memcpy(enabled_array, is_enabled, sizeof(enabled_type_t) * num_threads);
295         else {
296                 for (int i = 0; i < num_threads; i++)
297                         enabled_array[i] = THREAD_DISABLED;
298         }
299
300         explore(act->get_tid());
301 }
302
303 /**
304  * Records a backtracking reference for a thread choice within this Node.
305  * Provides feedback as to whether this thread choice is already set for
306  * backtracking.
307  * @return false if the thread was already set to be backtracked, true
308  * otherwise
309  */
310 bool Node::set_backtrack(thread_id_t id)
311 {
312         int i = id_to_int(id);
313         ASSERT(i < ((int)backtrack.size()));
314         if (backtrack[i])
315                 return false;
316         backtrack[i] = true;
317         numBacktracks++;
318         return true;
319 }
320
321 thread_id_t Node::get_next_backtrack()
322 {
323         /** @todo Find next backtrack */
324         unsigned int i;
325         for (i = 0; i < backtrack.size(); i++)
326                 if (backtrack[i] == true)
327                         break;
328         /* Backtrack set was empty? */
329         ASSERT(i != backtrack.size());
330
331         backtrack[i] = false;
332         numBacktracks--;
333         return int_to_id(i);
334 }
335
336 bool Node::is_enabled(Thread *t) const
337 {
338         int thread_id = id_to_int(t->get_id());
339         return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
340 }
341
342 enabled_type_t Node::enabled_status(thread_id_t tid) const
343 {
344         int thread_id = id_to_int(tid);
345         if (thread_id < num_threads)
346                 return enabled_array[thread_id];
347         else
348                 return THREAD_DISABLED;
349 }
350
351 bool Node::is_enabled(thread_id_t tid) const
352 {
353         int thread_id = id_to_int(tid);
354         return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
355 }
356
357 bool Node::has_priority(thread_id_t tid) const
358 {
359         return fairness[id_to_int(tid)].priority;
360 }
361
362 /**
363  * Add an action to the may_read_from set.
364  * @param act is the action to add
365  */
366 void Node::add_read_from(const ModelAction *act)
367 {
368         may_read_from.push_back(act);
369 }
370
371 /**
372  * Gets the next 'future_value' value from this Node. Only valid for a node
373  * where this->action is a 'read'.
374  * @return The first element in future_values
375  */
376 uint64_t Node::get_future_value() const
377 {
378         ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
379         return future_values[future_index].value;
380 }
381
382 modelclock_t Node::get_future_value_expiration() const
383 {
384         ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
385         return future_values[future_index].expiration;
386 }
387
388
389 int Node::get_read_from_size() const
390 {
391         return may_read_from.size();
392 }
393
394 const ModelAction * Node::get_read_from_at(int i) {
395         return may_read_from[i];
396 }
397
398 /**
399  * Gets the next 'may_read_from' action from this Node. Only valid for a node
400  * where this->action is a 'read'.
401  * @return The first element in may_read_from
402  */
403 const ModelAction * Node::get_read_from() const
404 {
405         if (read_from_index < may_read_from.size())
406                 return may_read_from[read_from_index];
407         else
408                 return NULL;
409 }
410
411 /**
412  * Increments the index into the readsfrom set to explore the next item.
413  * @return Returns false if we have explored all items.
414  */
415 bool Node::increment_read_from() {
416         DBG();
417         promises.clear();
418         if (read_from_index < may_read_from.size()) {
419                 read_from_index++;
420                 return read_from_index < may_read_from.size();
421         }
422         return false;
423 }
424
425 /**
426  * Increments the index into the future_values set to explore the next item.
427  * @return Returns false if we have explored all values.
428  */
429 bool Node::increment_future_value() {
430         DBG();
431         promises.clear();
432         if (future_index < ((int)future_values.size())) {
433                 future_index++;
434                 return (future_index < ((int)future_values.size()));
435         }
436         return false;
437 }
438
439 /**
440  * Add a write ModelAction to the set of writes that may break the release
441  * sequence. This is used during replay exploration of pending release
442  * sequences. This Node must correspond to a release sequence fixup action.
443  *
444  * @param write The write that may break the release sequence. NULL means we
445  * allow the release sequence to synchronize.
446  */
447 void Node::add_relseq_break(const ModelAction *write)
448 {
449         relseq_break_writes.push_back(write);
450 }
451
452 /**
453  * Get the write that may break the current pending release sequence,
454  * according to the replay / divergence pattern.
455  *
456  * @return A write that may break the release sequence. If NULL, that means
457  * the release sequence should not be broken.
458  */
459 const ModelAction * Node::get_relseq_break() const
460 {
461         if (relseq_break_index < (int)relseq_break_writes.size())
462                 return relseq_break_writes[relseq_break_index];
463         else
464                 return NULL;
465 }
466
467 /**
468  * Increments the index into the relseq_break_writes set to explore the next
469  * item.
470  * @return Returns false if we have explored all values.
471  */
472 bool Node::increment_relseq_break()
473 {
474         DBG();
475         promises.clear();
476         if (relseq_break_index < ((int)relseq_break_writes.size())) {
477                 relseq_break_index++;
478                 return (relseq_break_index < ((int)relseq_break_writes.size()));
479         }
480         return false;
481 }
482
483 /**
484  * @return True if all writes that may break the release sequence have been
485  * explored
486  */
487 bool Node::relseq_break_empty() const
488 {
489         return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
490 }
491
492 void Node::explore(thread_id_t tid)
493 {
494         int i = id_to_int(tid);
495         ASSERT(i < ((int)backtrack.size()));
496         if (backtrack[i]) {
497                 backtrack[i] = false;
498                 numBacktracks--;
499         }
500         explored_children[i] = true;
501 }
502
503 NodeStack::NodeStack() :
504         node_list(),
505         head_idx(-1),
506         total_nodes(0)
507 {
508         total_nodes++;
509 }
510
511 NodeStack::~NodeStack()
512 {
513         for (unsigned int i = 0; i < node_list.size(); i++)
514                 delete node_list[i];
515 }
516
517 void NodeStack::print() const
518 {
519         model_print("............................................\n");
520         model_print("NodeStack printing node_list:\n");
521         for (unsigned int it = 0; it < node_list.size(); it++) {
522                 if ((int)it == this->head_idx)
523                         model_print("vvv following action is the current iterator vvv\n");
524                 node_list[it]->print();
525         }
526         model_print("............................................\n");
527 }
528
529 /** Note: The is_enabled set contains what actions were enabled when
530  *  act was chosen. */
531 ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_enabled)
532 {
533         DBG();
534
535         if ((head_idx + 1) < (int)node_list.size()) {
536                 head_idx++;
537                 return node_list[head_idx]->get_action();
538         }
539
540         /* Record action */
541         Node *head = get_head();
542         Node *prevfairness = NULL;
543         if (head) {
544                 head->explore_child(act, is_enabled);
545                 if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow)
546                         prevfairness = node_list[head_idx - model->params.fairwindow];
547         }
548         node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness));
549         total_nodes++;
550         head_idx++;
551         return NULL;
552 }
553
554 /**
555  * Empties the stack of all trailing nodes after a given position and calls the
556  * destructor for each. This function is provided an offset which determines
557  * how many nodes (relative to the current replay state) to save before popping
558  * the stack.
559  * @param numAhead gives the number of Nodes (including this Node) to skip over
560  * before removing nodes.
561  */
562 void NodeStack::pop_restofstack(int numAhead)
563 {
564         /* Diverging from previous execution; clear out remainder of list */
565         unsigned int it = head_idx + numAhead;
566         for (unsigned int i = it; i < node_list.size(); i++)
567                 delete node_list[i];
568         node_list.resize(it);
569 }
570
571 Node * NodeStack::get_head() const
572 {
573         if (node_list.empty() || head_idx < 0)
574                 return NULL;
575         return node_list[head_idx];
576 }
577
578 Node * NodeStack::get_next() const
579 {
580         if (node_list.empty()) {
581                 DEBUG("Empty\n");
582                 return NULL;
583         }
584         unsigned int it = head_idx + 1;
585         if (it == node_list.size()) {
586                 DEBUG("At end\n");
587                 return NULL;
588         }
589         return node_list[it];
590 }
591
592 void NodeStack::reset_execution()
593 {
594         head_idx = -1;
595 }