Add yield block support. The idea is to not generate executions with yield actions.
[cdsspec-compiler.git] / nodestack.cc
1 #define __STDC_FORMAT_MACROS
2 #include <inttypes.h>
3
4 #include <string.h>
5
6 #include "nodestack.h"
7 #include "action.h"
8 #include "common.h"
9 #include "threads-model.h"
10 #include "modeltypes.h"
11 #include "execution.h"
12 #include "params.h"
13
14 /**
15  * @brief Node constructor
16  *
17  * Constructs a single Node for use in a NodeStack. Each Node is associated
18  * with exactly one ModelAction (exception: the first Node should be created
19  * as an empty stub, to represent the first thread "choice") and up to one
20  * parent.
21  *
22  * @param params The model-checker parameters
23  * @param act The ModelAction to associate with this Node. May be NULL.
24  * @param par The parent Node in the NodeStack. May be NULL if there is no
25  * parent.
26  * @param nthreads The number of threads which exist at this point in the
27  * execution trace.
28  */
29 Node::Node(const struct model_params *params, ModelAction *act, Node *par,
30                 int nthreads, Node *prevfairness) :
31         read_from_status(READ_FROM_PAST),
32         action(act),
33         params(params),
34         uninit_action(NULL),
35         parent(par),
36         num_threads(nthreads),
37         explored_children(num_threads),
38         backtrack(num_threads),
39         fairness(num_threads),
40         numBacktracks(0),
41         enabled_array(NULL),
42         read_from_past(),
43         read_from_past_idx(0),
44         read_from_promises(),
45         read_from_promise_idx(-1),
46         future_values(),
47         future_index(-1),
48         resolve_promise(),
49         resolve_promise_idx(-1),
50         relseq_break_writes(),
51         relseq_break_index(0),
52         misc_index(0),
53         misc_max(0),
54         yield_data(NULL)
55 {
56         ASSERT(act);
57         act->set_node(this);
58         int currtid = id_to_int(act->get_tid());
59         int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0;
60
61         if (get_params()->fairwindow != 0) {
62                 for (int i = 0; i < num_threads; i++) {
63                         ASSERT(i < ((int)fairness.size()));
64                         struct fairness_info *fi = &fairness[i];
65                         struct fairness_info *prevfi = (parent && i < parent->get_num_threads()) ? &parent->fairness[i] : NULL;
66                         if (prevfi) {
67                                 *fi = *prevfi;
68                         }
69                         if (parent && parent->is_enabled(int_to_id(i))) {
70                                 fi->enabled_count++;
71                         }
72                         if (i == currtid) {
73                                 fi->turns++;
74                                 fi->priority = false;
75                         }
76                         /* Do window processing */
77                         if (prevfairness != NULL) {
78                                 if (prevfairness->parent->is_enabled(int_to_id(i)))
79                                         fi->enabled_count--;
80                                 if (i == prevtid) {
81                                         fi->turns--;
82                                 }
83                                 /* Need full window to start evaluating
84                                  * conditions
85                                  * If we meet the enabled count and have no
86                                  * turns, give us priority */
87                                 if ((fi->enabled_count >= get_params()->enabledcount) &&
88                                                 (fi->turns == 0))
89                                         fi->priority = true;
90                         }
91                 }
92         }
93 }
94
95 int Node::get_yield_data(int tid1, int tid2) const {
96         if (tid1<num_threads && tid2 < num_threads)
97                 return yield_data[YIELD_INDEX(tid1,tid2,num_threads)];
98         else
99                 return YIELD_S | YIELD_D;
100 }
101
102 void Node::update_yield(Scheduler * scheduler) {
103         if (yield_data==NULL)
104                 yield_data=(int *) model_calloc(1, sizeof(int)*num_threads*num_threads);
105         //handle base case
106         if (parent == NULL) {
107                 for(int i = 0; i < num_threads*num_threads; i++) {
108                         yield_data[i] = YIELD_S | YIELD_D;
109                 }
110                 return;
111         }
112         int curr_tid=id_to_int(action->get_tid());
113
114         for(int u = 0; u < num_threads; u++) {
115                 for(int v = 0; v < num_threads; v++) {
116                         int yield_state=parent->get_yield_data(u, v);
117                         bool next_enabled=scheduler->is_enabled(int_to_id(v));
118                         bool curr_enabled=parent->is_enabled(int_to_id(v));
119                         if (!next_enabled) {
120                                 //Compute intersection of ES and E
121                                 yield_state&=~YIELD_E;
122                                 //Check to see if we disabled the thread
123                                 if (u==curr_tid && curr_enabled)
124                                         yield_state|=YIELD_D;
125                         }
126                         yield_data[YIELD_INDEX(u, v, num_threads)]=yield_state;
127                 }
128                 yield_data[YIELD_INDEX(u, curr_tid, num_threads)]=(yield_data[YIELD_INDEX(u, curr_tid, num_threads)]&~YIELD_P)|YIELD_S;
129         }
130         //handle curr.yield(t) part of computation
131         if (action->is_yield()) {
132                 for(int v = 0; v < num_threads; v++) {
133                         int yield_state=yield_data[YIELD_INDEX(curr_tid, v, num_threads)];
134                         if ((yield_state & (YIELD_E | YIELD_D)) && (!(yield_state & YIELD_S)))
135                                 yield_state |= YIELD_P;
136                         yield_state &= YIELD_P;
137                         if (scheduler->is_enabled(int_to_id(v))) {
138                                 yield_state|=YIELD_E;
139                         }
140                         yield_data[YIELD_INDEX(curr_tid, v, num_threads)]=yield_state;
141                 }
142         }
143 }
144
145 /** @brief Node desctructor */
146 Node::~Node()
147 {
148         delete action;
149         if (uninit_action)
150                 delete uninit_action;
151         if (enabled_array)
152                 model_free(enabled_array);
153         if (yield_data)
154                 model_free(yield_data);
155 }
156
157 /** Prints debugging info for the ModelAction associated with this Node */
158 void Node::print() const
159 {
160         action->print();
161         model_print("          thread status: ");
162         if (enabled_array) {
163                 for (int i = 0; i < num_threads; i++) {
164                         char str[20];
165                         enabled_type_to_string(enabled_array[i], str);
166                         model_print("[%d: %s]", i, str);
167                 }
168                 model_print("\n");
169         } else
170                 model_print("(info not available)\n");
171         model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
172         for (int i = 0; i < (int)backtrack.size(); i++)
173                 if (backtrack[i] == true)
174                         model_print("[%d]", i);
175         model_print("\n");
176
177         model_print("          read from past: %s", read_from_past_empty() ? "empty" : "non-empty ");
178         for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++)
179                 model_print("[%d]", read_from_past[i]->get_seq_number());
180         model_print("\n");
181
182         model_print("          read-from promises: %s", read_from_promise_empty() ? "empty" : "non-empty ");
183         for (int i = read_from_promise_idx + 1; i < (int)read_from_promises.size(); i++)
184                 model_print("[%d]", read_from_promises[i]->get_seq_number());
185         model_print("\n");
186
187         model_print("          future values: %s", future_value_empty() ? "empty" : "non-empty ");
188         for (int i = future_index + 1; i < (int)future_values.size(); i++)
189                 model_print("[%#" PRIx64 "]", future_values[i].value);
190         model_print("\n");
191
192         model_print("          promises: %s\n", promise_empty() ? "empty" : "non-empty");
193         model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
194         model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
195 }
196
197 /****************************** threads backtracking **************************/
198
199 /**
200  * Checks if the Thread associated with this thread ID has been explored from
201  * this Node already.
202  * @param tid is the thread ID to check
203  * @return true if this thread choice has been explored already, false
204  * otherwise
205  */
206 bool Node::has_been_explored(thread_id_t tid) const
207 {
208         int id = id_to_int(tid);
209         return explored_children[id];
210 }
211
212 /**
213  * Checks if the backtracking set is empty.
214  * @return true if the backtracking set is empty
215  */
216 bool Node::backtrack_empty() const
217 {
218         return (numBacktracks == 0);
219 }
220
221 void Node::explore(thread_id_t tid)
222 {
223         int i = id_to_int(tid);
224         ASSERT(i < ((int)backtrack.size()));
225         if (backtrack[i]) {
226                 backtrack[i] = false;
227                 numBacktracks--;
228         }
229         explored_children[i] = true;
230 }
231
232 /**
233  * Mark the appropriate backtracking information for exploring a thread choice.
234  * @param act The ModelAction to explore
235  */
236 void Node::explore_child(ModelAction *act, enabled_type_t *is_enabled)
237 {
238         if (!enabled_array)
239                 enabled_array = (enabled_type_t *)model_malloc(sizeof(enabled_type_t) * num_threads);
240         if (is_enabled != NULL)
241                 memcpy(enabled_array, is_enabled, sizeof(enabled_type_t) * num_threads);
242         else {
243                 for (int i = 0; i < num_threads; i++)
244                         enabled_array[i] = THREAD_DISABLED;
245         }
246
247         explore(act->get_tid());
248 }
249
250 /**
251  * Records a backtracking reference for a thread choice within this Node.
252  * Provides feedback as to whether this thread choice is already set for
253  * backtracking.
254  * @return false if the thread was already set to be backtracked, true
255  * otherwise
256  */
257 bool Node::set_backtrack(thread_id_t id)
258 {
259         int i = id_to_int(id);
260         ASSERT(i < ((int)backtrack.size()));
261         if (backtrack[i])
262                 return false;
263         backtrack[i] = true;
264         numBacktracks++;
265         return true;
266 }
267
268 thread_id_t Node::get_next_backtrack()
269 {
270         /** @todo Find next backtrack */
271         unsigned int i;
272         for (i = 0; i < backtrack.size(); i++)
273                 if (backtrack[i] == true)
274                         break;
275         /* Backtrack set was empty? */
276         ASSERT(i != backtrack.size());
277
278         backtrack[i] = false;
279         numBacktracks--;
280         return int_to_id(i);
281 }
282
283 void Node::clear_backtracking()
284 {
285         for (unsigned int i = 0; i < backtrack.size(); i++)
286                 backtrack[i] = false;
287         for (unsigned int i = 0; i < explored_children.size(); i++)
288                 explored_children[i] = false;
289         numBacktracks = 0;
290 }
291
292 /************************** end threads backtracking **************************/
293
294 /*********************************** promise **********************************/
295
296 /**
297  * Sets a promise to explore meeting with the given node.
298  * @param i is the promise index.
299  */
300 void Node::set_promise(unsigned int i)
301 {
302         if (i >= resolve_promise.size())
303                 resolve_promise.resize(i + 1, false);
304         resolve_promise[i] = true;
305 }
306
307 /**
308  * Looks up whether a given promise should be satisfied by this node.
309  * @param i The promise index.
310  * @return true if the promise should be satisfied by the given ModelAction.
311  */
312 bool Node::get_promise(unsigned int i) const
313 {
314         return (i < resolve_promise.size()) && (int)i == resolve_promise_idx;
315 }
316
317 /**
318  * Increments to the next promise to resolve.
319  * @return true if we have a valid combination.
320  */
321 bool Node::increment_promise()
322 {
323         DBG();
324         if (resolve_promise.empty())
325                 return false;
326         int prev_idx = resolve_promise_idx;
327         resolve_promise_idx++;
328         for ( ; resolve_promise_idx < (int)resolve_promise.size(); resolve_promise_idx++)
329                 if (resolve_promise[resolve_promise_idx])
330                         return true;
331         resolve_promise_idx = prev_idx;
332         return false;
333 }
334
335 /**
336  * Returns whether the promise set is empty.
337  * @return true if we have explored all promise combinations.
338  */
339 bool Node::promise_empty() const
340 {
341         for (int i = resolve_promise_idx + 1; i < (int)resolve_promise.size(); i++)
342                 if (i >= 0 && resolve_promise[i])
343                         return false;
344         return true;
345 }
346
347 /** @brief Clear any promise-resolution information for this Node */
348 void Node::clear_promise_resolutions()
349 {
350         resolve_promise.clear();
351         resolve_promise_idx = -1;
352 }
353
354 /******************************* end promise **********************************/
355
356 void Node::set_misc_max(int i)
357 {
358         misc_max = i;
359 }
360
361 int Node::get_misc() const
362 {
363         return misc_index;
364 }
365
366 bool Node::increment_misc()
367 {
368         return (misc_index < misc_max) && ((++misc_index) < misc_max);
369 }
370
371 bool Node::misc_empty() const
372 {
373         return (misc_index + 1) >= misc_max;
374 }
375
376 bool Node::is_enabled(Thread *t) const
377 {
378         int thread_id = id_to_int(t->get_id());
379         return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
380 }
381
382 enabled_type_t Node::enabled_status(thread_id_t tid) const
383 {
384         int thread_id = id_to_int(tid);
385         if (thread_id < num_threads)
386                 return enabled_array[thread_id];
387         else
388                 return THREAD_DISABLED;
389 }
390
391 bool Node::is_enabled(thread_id_t tid) const
392 {
393         int thread_id = id_to_int(tid);
394         return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
395 }
396
397 bool Node::has_priority(thread_id_t tid) const
398 {
399         return fairness[id_to_int(tid)].priority;
400 }
401
402 bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const
403 {
404         return get_yield_data(id_to_int(tid1), id_to_int(tid2)) & YIELD_P;
405 }
406
407 /*********************************** read from ********************************/
408
409 /**
410  * Get the current state of the may-read-from set iteration
411  * @return The read-from type we should currently be checking (past or future)
412  */
413 read_from_type_t Node::get_read_from_status()
414 {
415         if (read_from_status == READ_FROM_PAST && read_from_past.empty())
416                 increment_read_from();
417         return read_from_status;
418 }
419
420 /**
421  * Iterate one step in the may-read-from iteration. This includes a step in
422  * reading from the either the past or the future.
423  * @return True if there is a new read-from to explore; false otherwise
424  */
425 bool Node::increment_read_from()
426 {
427         clear_promise_resolutions();
428         if (increment_read_from_past()) {
429                read_from_status = READ_FROM_PAST;
430                return true;
431         } else if (increment_read_from_promise()) {
432                 read_from_status = READ_FROM_PROMISE;
433                 return true;
434         } else if (increment_future_value()) {
435                 read_from_status = READ_FROM_FUTURE;
436                 return true;
437         }
438         read_from_status = READ_FROM_NONE;
439         return false;
440 }
441
442 /**
443  * @return True if there are any new read-froms to explore
444  */
445 bool Node::read_from_empty() const
446 {
447         return read_from_past_empty() &&
448                 read_from_promise_empty() &&
449                 future_value_empty();
450 }
451
452 /**
453  * Get the total size of the may-read-from set, including both past and future
454  * values
455  * @return The size of may-read-from
456  */
457 unsigned int Node::read_from_size() const
458 {
459         return read_from_past.size() +
460                 read_from_promises.size() +
461                 future_values.size();
462 }
463
464 /******************************* end read from ********************************/
465
466 /****************************** read from past ********************************/
467
468 /** @brief Prints info about read_from_past set */
469 void Node::print_read_from_past()
470 {
471         for (unsigned int i = 0; i < read_from_past.size(); i++)
472                 read_from_past[i]->print();
473 }
474
475 /**
476  * Add an action to the read_from_past set.
477  * @param act is the action to add
478  */
479 void Node::add_read_from_past(const ModelAction *act)
480 {
481         read_from_past.push_back(act);
482 }
483
484 /**
485  * Gets the next 'read_from_past' action from this Node. Only valid for a node
486  * where this->action is a 'read'.
487  * @return The first element in read_from_past
488  */
489 const ModelAction * Node::get_read_from_past() const
490 {
491         if (read_from_past_idx < read_from_past.size())
492                 return read_from_past[read_from_past_idx];
493         else
494                 return NULL;
495 }
496
497 const ModelAction * Node::get_read_from_past(int i) const
498 {
499         return read_from_past[i];
500 }
501
502 int Node::get_read_from_past_size() const
503 {
504         return read_from_past.size();
505 }
506
507 /**
508  * Checks whether the readsfrom set for this node is empty.
509  * @return true if the readsfrom set is empty.
510  */
511 bool Node::read_from_past_empty() const
512 {
513         return ((read_from_past_idx + 1) >= read_from_past.size());
514 }
515
516 /**
517  * Increments the index into the readsfrom set to explore the next item.
518  * @return Returns false if we have explored all items.
519  */
520 bool Node::increment_read_from_past()
521 {
522         DBG();
523         if (read_from_past_idx < read_from_past.size()) {
524                 read_from_past_idx++;
525                 return read_from_past_idx < read_from_past.size();
526         }
527         return false;
528 }
529
530 /************************** end read from past ********************************/
531
532 /***************************** read_from_promises *****************************/
533
534 /**
535  * Add an action to the read_from_promises set.
536  * @param reader The read which generated the Promise; we use the ModelAction
537  * instead of the Promise because the Promise does not last across executions
538  */
539 void Node::add_read_from_promise(const ModelAction *reader)
540 {
541         read_from_promises.push_back(reader);
542 }
543
544 /**
545  * Gets the next 'read-from-promise' from this Node. Only valid for a node
546  * where this->action is a 'read'.
547  * @return The current element in read_from_promises
548  */
549 Promise * Node::get_read_from_promise() const
550 {
551         ASSERT(read_from_promise_idx >= 0 && read_from_promise_idx < ((int)read_from_promises.size()));
552         return read_from_promises[read_from_promise_idx]->get_reads_from_promise();
553 }
554
555 /**
556  * Gets a particular 'read-from-promise' form this Node. Only vlaid for a node
557  * where this->action is a 'read'.
558  * @param i The index of the Promise to get
559  * @return The Promise at index i, if the Promise is still available; NULL
560  * otherwise
561  */
562 Promise * Node::get_read_from_promise(int i) const
563 {
564         return read_from_promises[i]->get_reads_from_promise();
565 }
566
567 /** @return The size of the read-from-promise set */
568 int Node::get_read_from_promise_size() const
569 {
570         return read_from_promises.size();
571 }
572
573 /**
574  * Checks whether the read_from_promises set for this node is empty.
575  * @return true if the read_from_promises set is empty.
576  */
577 bool Node::read_from_promise_empty() const
578 {
579         return ((read_from_promise_idx + 1) >= ((int)read_from_promises.size()));
580 }
581
582 /**
583  * Increments the index into the read_from_promises set to explore the next item.
584  * @return Returns false if we have explored all promises.
585  */
586 bool Node::increment_read_from_promise()
587 {
588         DBG();
589         if (read_from_promise_idx < ((int)read_from_promises.size())) {
590                 read_from_promise_idx++;
591                 return (read_from_promise_idx < ((int)read_from_promises.size()));
592         }
593         return false;
594 }
595
596 /************************* end read_from_promises *****************************/
597
598 /****************************** future values *********************************/
599
600 /**
601  * Adds a value from a weakly ordered future write to backtrack to. This
602  * operation may "fail" if the future value has already been run (within some
603  * sloppiness window of this expiration), or if the futurevalues set has
604  * reached its maximum.
605  * @see model_params.maxfuturevalues
606  *
607  * @param value is the value to backtrack to.
608  * @return True if the future value was successully added; false otherwise
609  */
610 bool Node::add_future_value(struct future_value fv)
611 {
612         uint64_t value = fv.value;
613         modelclock_t expiration = fv.expiration;
614         thread_id_t tid = fv.tid;
615         int idx = -1; /* Highest index where value is found */
616         for (unsigned int i = 0; i < future_values.size(); i++) {
617                 if (future_values[i].value == value && future_values[i].tid == tid) {
618                         if (expiration <= future_values[i].expiration)
619                                 return false;
620                         idx = i;
621                 }
622         }
623         if (idx > future_index) {
624                 /* Future value hasn't been explored; update expiration */
625                 future_values[idx].expiration = expiration;
626                 return true;
627         } else if (idx >= 0 && expiration <= future_values[idx].expiration + get_params()->expireslop) {
628                 /* Future value has been explored and is within the "sloppy" window */
629                 return false;
630         }
631
632         /* Limit the size of the future-values set */
633         if (get_params()->maxfuturevalues > 0 &&
634                         (int)future_values.size() >= get_params()->maxfuturevalues)
635                 return false;
636
637         future_values.push_back(fv);
638         return true;
639 }
640
641 /**
642  * Gets the next 'future_value' from this Node. Only valid for a node where
643  * this->action is a 'read'.
644  * @return The first element in future_values
645  */
646 struct future_value Node::get_future_value() const
647 {
648         ASSERT(future_index >= 0 && future_index < ((int)future_values.size()));
649         return future_values[future_index];
650 }
651
652 /**
653  * Checks whether the future_values set for this node is empty.
654  * @return true if the future_values set is empty.
655  */
656 bool Node::future_value_empty() const
657 {
658         return ((future_index + 1) >= ((int)future_values.size()));
659 }
660
661 /**
662  * Increments the index into the future_values set to explore the next item.
663  * @return Returns false if we have explored all values.
664  */
665 bool Node::increment_future_value()
666 {
667         DBG();
668         if (future_index < ((int)future_values.size())) {
669                 future_index++;
670                 return (future_index < ((int)future_values.size()));
671         }
672         return false;
673 }
674
675 /************************** end future values *********************************/
676
677 /*********************** breaking release sequences ***************************/
678
679 /**
680  * Add a write ModelAction to the set of writes that may break the release
681  * sequence. This is used during replay exploration of pending release
682  * sequences. This Node must correspond to a release sequence fixup action.
683  *
684  * @param write The write that may break the release sequence. NULL means we
685  * allow the release sequence to synchronize.
686  */
687 void Node::add_relseq_break(const ModelAction *write)
688 {
689         relseq_break_writes.push_back(write);
690 }
691
692 /**
693  * Get the write that may break the current pending release sequence,
694  * according to the replay / divergence pattern.
695  *
696  * @return A write that may break the release sequence. If NULL, that means
697  * the release sequence should not be broken.
698  */
699 const ModelAction * Node::get_relseq_break() const
700 {
701         if (relseq_break_index < (int)relseq_break_writes.size())
702                 return relseq_break_writes[relseq_break_index];
703         else
704                 return NULL;
705 }
706
707 /**
708  * Increments the index into the relseq_break_writes set to explore the next
709  * item.
710  * @return Returns false if we have explored all values.
711  */
712 bool Node::increment_relseq_break()
713 {
714         DBG();
715         if (relseq_break_index < ((int)relseq_break_writes.size())) {
716                 relseq_break_index++;
717                 return (relseq_break_index < ((int)relseq_break_writes.size()));
718         }
719         return false;
720 }
721
722 /**
723  * @return True if all writes that may break the release sequence have been
724  * explored
725  */
726 bool Node::relseq_break_empty() const
727 {
728         return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
729 }
730
731 /******************* end breaking release sequences ***************************/
732
733 /**
734  * Increments some behavior's index, if a new behavior is available
735  * @return True if there is a new behavior available; otherwise false
736  */
737 bool Node::increment_behaviors()
738 {
739         /* satisfy a different misc_index values */
740         if (increment_misc())
741                 return true;
742         /* satisfy a different set of promises */
743         if (increment_promise())
744                 return true;
745         /* read from a different value */
746         if (increment_read_from())
747                 return true;
748         /* resolve a release sequence differently */
749         if (increment_relseq_break())
750                 return true;
751         return false;
752 }
753
754 NodeStack::NodeStack() :
755         node_list(),
756         head_idx(-1),
757         total_nodes(0)
758 {
759         total_nodes++;
760 }
761
762 NodeStack::~NodeStack()
763 {
764         for (unsigned int i = 0; i < node_list.size(); i++)
765                 delete node_list[i];
766 }
767
768 /**
769  * @brief Register the model-checker object with this NodeStack
770  * @param exec The execution structure for the ModelChecker
771  */
772 void NodeStack::register_engine(const ModelExecution *exec)
773 {
774         this->execution = exec;
775 }
776
777 const struct model_params * NodeStack::get_params() const
778 {
779         return execution->get_params();
780 }
781
782 void NodeStack::print() const
783 {
784         model_print("............................................\n");
785         model_print("NodeStack printing node_list:\n");
786         for (unsigned int it = 0; it < node_list.size(); it++) {
787                 if ((int)it == this->head_idx)
788                         model_print("vvv following action is the current iterator vvv\n");
789                 node_list[it]->print();
790         }
791         model_print("............................................\n");
792 }
793
794 /** Note: The is_enabled set contains what actions were enabled when
795  *  act was chosen. */
796 ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_enabled)
797 {
798         DBG();
799
800         if ((head_idx + 1) < (int)node_list.size()) {
801                 head_idx++;
802                 return node_list[head_idx]->get_action();
803         }
804
805         /* Record action */
806         Node *head = get_head();
807         Node *prevfairness = NULL;
808         if (head) {
809                 head->explore_child(act, is_enabled);
810                 if (get_params()->fairwindow != 0 && head_idx > (int)get_params()->fairwindow)
811                         prevfairness = node_list[head_idx - get_params()->fairwindow];
812         }
813
814         int next_threads = execution->get_num_threads();
815         if (act->get_type() == THREAD_CREATE)
816                 next_threads++;
817         node_list.push_back(new Node(get_params(), act, head, next_threads, prevfairness));
818         total_nodes++;
819         head_idx++;
820         return NULL;
821 }
822
823 /**
824  * Empties the stack of all trailing nodes after a given position and calls the
825  * destructor for each. This function is provided an offset which determines
826  * how many nodes (relative to the current replay state) to save before popping
827  * the stack.
828  * @param numAhead gives the number of Nodes (including this Node) to skip over
829  * before removing nodes.
830  */
831 void NodeStack::pop_restofstack(int numAhead)
832 {
833         /* Diverging from previous execution; clear out remainder of list */
834         unsigned int it = head_idx + numAhead;
835         for (unsigned int i = it; i < node_list.size(); i++)
836                 delete node_list[i];
837         node_list.resize(it);
838         node_list.back()->clear_backtracking();
839 }
840
841 Node * NodeStack::get_head() const
842 {
843         if (node_list.empty() || head_idx < 0)
844                 return NULL;
845         return node_list[head_idx];
846 }
847
848 Node * NodeStack::get_next() const
849 {
850         if (node_list.empty()) {
851                 DEBUG("Empty\n");
852                 return NULL;
853         }
854         unsigned int it = head_idx + 1;
855         if (it == node_list.size()) {
856                 DEBUG("At end\n");
857                 return NULL;
858         }
859         return node_list[it];
860 }
861
862 void NodeStack::reset_execution()
863 {
864         head_idx = -1;
865 }