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