nodestack.cc

   1 #define __STDC_FORMAT_MACROS
   2 #include <inttypes.h>
   3 #include <cstdlib>
   4
   5 #include <string.h>
   6
   7 #include "nodestack.h"
   8 #include "action.h"
   9 #include "common.h"
  10 #include "threads-model.h"
  11 #include "modeltypes.h"
  12 #include "execution.h"
  13 #include "params.h"
  14
  15 /**
  16  * @brief Node constructor
  17  *
  18  * Constructs a single Node for use in a NodeStack. Each Node is associated
  19  * with exactly one ModelAction (exception: the first Node should be created
  20  * as an empty stub, to represent the first thread "choice") and up to one
  21  * parent.
  22  *
  23  * @param params The model-checker parameters
  24  * @param act The ModelAction to associate with this Node. May be NULL.
  25  * @param par The parent Node in the NodeStack. May be NULL if there is no
  26  * parent.
  27  * @param nthreads The number of threads which exist at this point in the
  28  * execution trace.
  29  */
  30 Node::Node(const struct model_params *params, ModelAction *act, Node *par,
  31                 int nthreads, Node *prevfairness) :
  32         read_from_status(READ_FROM_PAST),
  33         action(act),
  34         params(params),
  35         uninit_action(NULL),
  36         parent(par),
  37         num_threads(nthreads),
  38         explored_children(num_threads),
  39         backtrack(num_threads),
  40         fairness(num_threads),
  41         numBacktracks(0),
  42         enabled_array(NULL),
  43         read_from_past(),
  44         read_from_past_idx(0),
  45         relseq_break_writes(),
  46         relseq_break_index(0),
  47         misc_index(0),
  48         misc_max(0),
  49         yield_data(NULL)
  50 {
  51         ASSERT(act);
  52         act->set_node(this);
  53         int currtid = id_to_int(act->get_tid());
  54         int prevtid = prevfairness ? id_to_int(prevfairness->action->get_tid()) : 0;
  55
  56         if (get_params()->fairwindow != 0) {
  57                 for (int i = 0; i < num_threads; i++) {
  58                         ASSERT(i < ((int)fairness.size()));
  59                         struct fairness_info *fi = &fairness[i];
  60                         struct fairness_info *prevfi = (parent && i < parent->get_num_threads()) ? &parent->fairness[i] : NULL;
  61                         if (prevfi) {
  62                                 *fi = *prevfi;
  63                         }
  64                         if (parent && parent->is_enabled(int_to_id(i))) {
  65                                 fi->enabled_count++;
  66                         }
  67                         if (i == currtid) {
  68                                 fi->turns++;
  69                                 fi->priority = false;
  70                         }
  71                         /* Do window processing */
  72                         if (prevfairness != NULL) {
  73                                 if (prevfairness->parent->is_enabled(int_to_id(i)))
  74                                         fi->enabled_count--;
  75                                 if (i == prevtid) {
  76                                         fi->turns--;
  77                                 }
  78                                 /* Need full window to start evaluating
  79                                  * conditions
  80                                  * If we meet the enabled count and have no
  81                                  * turns, give us priority */
  82                                 if ((fi->enabled_count >= get_params()->enabledcount) &&
  83                                                 (fi->turns == 0))
  84                                         fi->priority = true;
  85                         }
  86                 }
  87         }
  88 }
  89
  90 int Node::get_yield_data(int tid1, int tid2) const {
  91         if (tid1<num_threads && tid2 < num_threads)
  92                 return yield_data[YIELD_INDEX(tid1,tid2,num_threads)];
  93         else
  94                 return YIELD_S | YIELD_D;
  95 }
  96
  97 void Node::update_yield(Scheduler * scheduler) {
  98         if (yield_data==NULL)
  99                 yield_data=(int *) model_calloc(1, sizeof(int)*num_threads*num_threads);
 100         //handle base case
 101         if (parent == NULL) {
 102                 for(int i = 0; i < num_threads*num_threads; i++) {
 103                         yield_data[i] = YIELD_S | YIELD_D;
 104                 }
 105                 return;
 106         }
 107         int curr_tid=id_to_int(action->get_tid());
 108
 109         for(int u = 0; u < num_threads; u++) {
 110                 for(int v = 0; v < num_threads; v++) {
 111                         int yield_state=parent->get_yield_data(u, v);
 112                         bool next_enabled=scheduler->is_enabled(int_to_id(v));
 113                         bool curr_enabled=parent->is_enabled(int_to_id(v));
 114                         if (!next_enabled) {
 115                                 //Compute intersection of ES and E
 116                                 yield_state&=~YIELD_E;
 117                                 //Check to see if we disabled the thread
 118                                 if (u==curr_tid && curr_enabled)
 119                                         yield_state|=YIELD_D;
 120                         }
 121                         yield_data[YIELD_INDEX(u, v, num_threads)]=yield_state;
 122                 }
 123                 yield_data[YIELD_INDEX(u, curr_tid, num_threads)]=(yield_data[YIELD_INDEX(u, curr_tid, num_threads)]&~YIELD_P)|YIELD_S;
 124         }
 125         //handle curr.yield(t) part of computation
 126         if (action->is_yield()) {
 127                 for(int v = 0; v < num_threads; v++) {
 128                         int yield_state=yield_data[YIELD_INDEX(curr_tid, v, num_threads)];
 129                         if ((yield_state & (YIELD_E | YIELD_D)) && (!(yield_state & YIELD_S)))
 130                                 yield_state |= YIELD_P;
 131                         yield_state &= YIELD_P;
 132                         if (scheduler->is_enabled(int_to_id(v))) {
 133                                 yield_state|=YIELD_E;
 134                         }
 135                         yield_data[YIELD_INDEX(curr_tid, v, num_threads)]=yield_state;
 136                 }
 137         }
 138 }
 139
 140 /** @brief Node desctructor */
 141 Node::~Node()
 142 {
 143         delete action;
 144         if (uninit_action)
 145                 delete uninit_action;
 146         if (enabled_array)
 147                 model_free(enabled_array);
 148         if (yield_data)
 149                 model_free(yield_data);
 150 }
 151
 152 /** Prints debugging info for the ModelAction associated with this Node */
 153 void Node::print() const
 154 {
 155         action->print();
 156         model_print("          thread status: ");
 157         if (enabled_array) {
 158                 for (int i = 0; i < num_threads; i++) {
 159                         char str[20];
 160                         enabled_type_to_string(enabled_array[i], str);
 161                         model_print("[%d: %s]", i, str);
 162                 }
 163                 model_print("\n");
 164         } else
 165                 model_print("(info not available)\n");
 166         model_print("          backtrack: %s", backtrack_empty() ? "empty" : "non-empty ");
 167         for (int i = 0; i < (int)backtrack.size(); i++)
 168                 if (backtrack[i] == true)
 169                         model_print("[%d]", i);
 170         model_print("\n");
 171
 172         model_print("          read from past: %s", read_from_past_empty() ? "empty" : "non-empty ");
 173         for (int i = read_from_past_idx + 1; i < (int)read_from_past.size(); i++)
 174                 model_print("[%d]", read_from_past[i]->get_seq_number());
 175         model_print("\n");
 176
 177         model_print("          misc: %s\n", misc_empty() ? "empty" : "non-empty");
 178         model_print("          rel seq break: %s\n", relseq_break_empty() ? "empty" : "non-empty");
 179 }
 180
 181 /****************************** threads backtracking **************************/
 182
 183 /**
 184  * Checks if the Thread associated with this thread ID has been explored from
 185  * this Node already.
 186  * @param tid is the thread ID to check
 187  * @return true if this thread choice has been explored already, false
 188  * otherwise
 189  */
 190 bool Node::has_been_explored(thread_id_t tid) const
 191 {
 192         int id = id_to_int(tid);
 193         return explored_children[id];
 194 }
 195
 196 /**
 197  * Checks if the backtracking set is empty.
 198  * @return true if the backtracking set is empty
 199  */
 200 bool Node::backtrack_empty() const
 201 {
 202         return (numBacktracks == 0);
 203 }
 204
 205 void Node::explore(thread_id_t tid)
 206 {
 207         int i = id_to_int(tid);
 208         ASSERT(i < ((int)backtrack.size()));
 209         if (backtrack[i]) {
 210                 backtrack[i] = false;
 211                 numBacktracks--;
 212         }
 213         explored_children[i] = true;
 214 }
 215
 216 /**
 217  * Mark the appropriate backtracking information for exploring a thread choice.
 218  * @param act The ModelAction to explore
 219  */
 220 void Node::explore_child(ModelAction *act, enabled_type_t *is_enabled)
 221 {
 222         if (!enabled_array)
 223                 enabled_array = (enabled_type_t *)model_malloc(sizeof(enabled_type_t) * num_threads);
 224         if (is_enabled != NULL)
 225                 memcpy(enabled_array, is_enabled, sizeof(enabled_type_t) * num_threads);
 226         else {
 227                 for (int i = 0; i < num_threads; i++)
 228                         enabled_array[i] = THREAD_DISABLED;
 229         }
 230
 231         explore(act->get_tid());
 232 }
 233
 234 /**
 235  * Records a backtracking reference for a thread choice within this Node.
 236  * Provides feedback as to whether this thread choice is already set for
 237  * backtracking.
 238  * @return false if the thread was already set to be backtracked, true
 239  * otherwise
 240  */
 241 bool Node::set_backtrack(thread_id_t id)
 242 {
 243         int i = id_to_int(id);
 244         ASSERT(i < ((int)backtrack.size()));
 245         if (backtrack[i])
 246                 return false;
 247         backtrack[i] = true;
 248         numBacktracks++;
 249         return true;
 250 }
 251
 252 thread_id_t Node::get_next_backtrack()
 253 {
 254         /** @todo Find next backtrack */
 255         unsigned int i;
 256         for (i = 0; i < backtrack.size(); i++)
 257                 if (backtrack[i] == true)
 258                         break;
 259         /* Backtrack set was empty? */
 260         ASSERT(i != backtrack.size());
 261
 262         backtrack[i] = false;
 263         numBacktracks--;
 264         return int_to_id(i);
 265 }
 266
 267 void Node::clear_backtracking()
 268 {
 269         for (unsigned int i = 0; i < backtrack.size(); i++)
 270                 backtrack[i] = false;
 271         for (unsigned int i = 0; i < explored_children.size(); i++)
 272                 explored_children[i] = false;
 273         numBacktracks = 0;
 274 }
 275
 276 /************************** end threads backtracking **************************/
 277
 278 void Node::set_misc_max(int i)
 279 {
 280         misc_max = i;
 281 }
 282
 283 int Node::get_misc() const
 284 {
 285         return misc_index;
 286 }
 287
 288 bool Node::increment_misc()
 289 {
 290         return (misc_index < misc_max) && ((++misc_index) < misc_max);
 291 }
 292
 293 bool Node::misc_empty() const
 294 {
 295         return (misc_index + 1) >= misc_max;
 296 }
 297
 298 bool Node::is_enabled(Thread *t) const
 299 {
 300         int thread_id = id_to_int(t->get_id());
 301         return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
 302 }
 303
 304 enabled_type_t Node::enabled_status(thread_id_t tid) const
 305 {
 306         int thread_id = id_to_int(tid);
 307         if (thread_id < num_threads)
 308                 return enabled_array[thread_id];
 309         else
 310                 return THREAD_DISABLED;
 311 }
 312
 313 bool Node::is_enabled(thread_id_t tid) const
 314 {
 315         int thread_id = id_to_int(tid);
 316         return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
 317 }
 318
 319 bool Node::has_priority(thread_id_t tid) const
 320 {
 321         return fairness[id_to_int(tid)].priority;
 322 }
 323
 324 bool Node::has_priority_over(thread_id_t tid1, thread_id_t tid2) const
 325 {
 326         return get_yield_data(id_to_int(tid1), id_to_int(tid2)) & YIELD_P;
 327 }
 328
 329 /*********************************** read from ********************************/
 330
 331 /**
 332  * Get the current state of the may-read-from set iteration
 333  * @return The read-from type we should currently be checking (past)
 334  */
 335 read_from_type_t Node::get_read_from_status()
 336 {
 337         if (read_from_status == READ_FROM_PAST && read_from_past.empty())
 338                 increment_read_from();
 339         return read_from_status;
 340 }
 341
 342 /**
 343  * Iterate one step in the may-read-from iteration. This includes a step in
 344  * reading from the either the past or the future.
 345  * @return True if there is a new read-from to explore; false otherwise
 346  */
 347 bool Node::increment_read_from()
 348 {
 349         if (increment_read_from_past()) {
 350                read_from_status = READ_FROM_PAST;
 351                return true;
 352         }
 353         read_from_status = READ_FROM_NONE;
 354         return false;
 355 }
 356
 357 /**
 358  * @return True if there are any new read-froms to explore
 359  */
 360 bool Node::read_from_empty() const
 361 {
 362   return read_from_past_empty();
 363 }
 364
 365 /**
 366  * Get the total size of the may-read-from set, including both past
 367  * @return The size of may-read-from
 368  */
 369 unsigned int Node::read_from_size() const
 370 {
 371   return read_from_past.size();
 372 }
 373
 374 /******************************* end read from ********************************/
 375
 376 /****************************** read from past ********************************/
 377
 378 /** @brief Prints info about read_from_past set */
 379 void Node::print_read_from_past()
 380 {
 381         for (unsigned int i = 0; i < read_from_past.size(); i++)
 382                 read_from_past[i]->print();
 383 }
 384
 385 /**
 386  * Add an action to the read_from_past set.
 387  * @param act is the action to add
 388  */
 389 void Node::add_read_from_past(const ModelAction *act)
 390 {
 391         read_from_past.push_back(act);
 392 }
 393
 394 /**
 395  * Gets the next 'read_from_past' action from this Node. Only valid for a node
 396  * where this->action is a 'read'.
 397  * @return The first element in read_from_past
 398  */
 399 const ModelAction * Node::get_read_from_past() const
 400 {
 401         if (read_from_past_idx < read_from_past.size()) {
 402                 int random_index = rand() % read_from_past.size();
 403                 return read_from_past[random_index];
 404         }
 405 //              return read_from_past[read_from_past_idx];
 406         else
 407                 return NULL;
 408 }
 409
 410 const ModelAction * Node::get_read_from_past(int i) const
 411 {
 412         return read_from_past[i];
 413 }
 414
 415 int Node::get_read_from_past_size() const
 416 {
 417         return read_from_past.size();
 418 }
 419
 420 /**
 421  * Checks whether the readsfrom set for this node is empty.
 422  * @return true if the readsfrom set is empty.
 423  */
 424 bool Node::read_from_past_empty() const
 425 {
 426         return ((read_from_past_idx + 1) >= read_from_past.size());
 427 }
 428
 429 /**
 430  * Increments the index into the readsfrom set to explore the next item.
 431  * @return Returns false if we have explored all items.
 432  */
 433 bool Node::increment_read_from_past()
 434 {
 435         DBG();
 436         if (read_from_past_idx < read_from_past.size()) {
 437                 read_from_past_idx++;
 438                 return read_from_past_idx < read_from_past.size();
 439         }
 440         return false;
 441 }
 442
 443 /************************** end read from past ********************************/
 444
 445 /*********************** breaking release sequences ***************************/
 446
 447 /**
 448  * Add a write ModelAction to the set of writes that may break the release
 449  * sequence. This is used during replay exploration of pending release
 450  * sequences. This Node must correspond to a release sequence fixup action.
 451  *
 452  * @param write The write that may break the release sequence. NULL means we
 453  * allow the release sequence to synchronize.
 454  */
 455 void Node::add_relseq_break(const ModelAction *write)
 456 {
 457         relseq_break_writes.push_back(write);
 458 }
 459
 460 /**
 461  * Get the write that may break the current pending release sequence,
 462  * according to the replay / divergence pattern.
 463  *
 464  * @return A write that may break the release sequence. If NULL, that means
 465  * the release sequence should not be broken.
 466  */
 467 const ModelAction * Node::get_relseq_break() const
 468 {
 469         if (relseq_break_index < (int)relseq_break_writes.size())
 470                 return relseq_break_writes[relseq_break_index];
 471         else
 472                 return NULL;
 473 }
 474
 475 /**
 476  * Increments the index into the relseq_break_writes set to explore the next
 477  * item.
 478  * @return Returns false if we have explored all values.
 479  */
 480 bool Node::increment_relseq_break()
 481 {
 482         DBG();
 483         if (relseq_break_index < ((int)relseq_break_writes.size())) {
 484                 relseq_break_index++;
 485                 return (relseq_break_index < ((int)relseq_break_writes.size()));
 486         }
 487         return false;
 488 }
 489
 490 /**
 491  * @return True if all writes that may break the release sequence have been
 492  * explored
 493  */
 494 bool Node::relseq_break_empty() const
 495 {
 496         return ((relseq_break_index + 1) >= ((int)relseq_break_writes.size()));
 497 }
 498
 499 /******************* end breaking release sequences ***************************/
 500
 501 /**
 502  * Increments some behavior's index, if a new behavior is available
 503  * @return True if there is a new behavior available; otherwise false
 504  */
 505 bool Node::increment_behaviors()
 506 {
 507         /* satisfy a different misc_index values */
 508         if (increment_misc())
 509                 return true;
 510         /* read from a different value */
 511         if (increment_read_from())
 512                 return true;
 513         /* resolve a release sequence differently */
 514         if (increment_relseq_break())
 515                 return true;
 516         return false;
 517 }
 518
 519 NodeStack::NodeStack() :
 520         node_list(),
 521         head_idx(-1),
 522         total_nodes(0)
 523 {
 524         total_nodes++;
 525 }
 526
 527 NodeStack::~NodeStack()
 528 {
 529         for (unsigned int i = 0; i < node_list.size(); i++)
 530                 delete node_list[i];
 531 }
 532
 533 /**
 534  * @brief Register the model-checker object with this NodeStack
 535  * @param exec The execution structure for the ModelChecker
 536  */
 537 void NodeStack::register_engine(const ModelExecution *exec)
 538 {
 539         this->execution = exec;
 540 }
 541
 542 const struct model_params * NodeStack::get_params() const
 543 {
 544         return execution->get_params();
 545 }
 546
 547 void NodeStack::print() const
 548 {
 549         model_print("............................................\n");
 550         model_print("NodeStack printing node_list:\n");
 551         for (unsigned int it = 0; it < node_list.size(); it++) {
 552                 if ((int)it == this->head_idx)
 553                         model_print("vvv following action is the current iterator vvv\n");
 554                 node_list[it]->print();
 555         }
 556         model_print("............................................\n");
 557 }
 558
 559 /** Note: The is_enabled set contains what actions were enabled when
 560  *  act was chosen. */
 561 ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_enabled)
 562 {
 563         DBG();
 564
 565         if ((head_idx + 1) < (int)node_list.size()) {
 566                 head_idx++;
 567                 return node_list[head_idx]->get_action();
 568         }
 569
 570         /* Record action */
 571         Node *head = get_head();
 572         Node *prevfairness = NULL;
 573         if (head) {
 574                 head->explore_child(act, is_enabled);
 575                 if (get_params()->fairwindow != 0 && head_idx > (int)get_params()->fairwindow)
 576                         prevfairness = node_list[head_idx - get_params()->fairwindow];
 577         }
 578
 579         int next_threads = execution->get_num_threads();
 580         if (act->get_type() == THREAD_CREATE || act->get_type() == PTHREAD_CREATE ) // may need to be changed
 581                 next_threads++;
 582         node_list.push_back(new Node(get_params(), act, head, next_threads, prevfairness));
 583         total_nodes++;
 584         head_idx++;
 585         return NULL;
 586 }
 587
 588 /**
 589  * Empties the stack of all trailing nodes after a given position and calls the
 590  * destructor for each. This function is provided an offset which determines
 591  * how many nodes (relative to the current replay state) to save before popping
 592  * the stack.
 593  * @param numAhead gives the number of Nodes (including this Node) to skip over
 594  * before removing nodes.
 595  */
 596 void NodeStack::pop_restofstack(int numAhead)
 597 {
 598         /* Diverging from previous execution; clear out remainder of list */
 599         unsigned int it = head_idx + numAhead;
 600         for (unsigned int i = it; i < node_list.size(); i++)
 601                 delete node_list[i];
 602         node_list.resize(it);
 603         node_list.back()->clear_backtracking();
 604 }
 605
 606 /** Reset the node stack. */
 607 void NodeStack::full_reset()
 608 {
 609         for (unsigned int i = 0; i < node_list.size(); i++)
 610                 delete node_list[i];
 611         node_list.clear();
 612         reset_execution();
 613         total_nodes = 1;
 614 }
 615
 616 Node * NodeStack::get_head() const
 617 {
 618         if (node_list.empty() || head_idx < 0)
 619                 return NULL;
 620         return node_list[head_idx];
 621 }
 622
 623 Node * NodeStack::get_next() const
 624 {
 625         if (node_list.empty()) {
 626                 DEBUG("Empty\n");
 627                 return NULL;
 628         }
 629         unsigned int it = head_idx + 1;
 630         if (it == node_list.size()) {
 631                 DEBUG("At end\n");
 632                 return NULL;
 633         }
 634         return node_list[it];
 635 }
 636
 637 void NodeStack::reset_execution()
 638 {
 639         head_idx = -1;
 640 }