execution.cc

   1 #include <stdio.h>
   2 #include <algorithm>
   3 #include <new>
   4 #include <stdarg.h>
   5
   6 #include "model.h"
   7 #include "execution.h"
   8 #include "action.h"
   9 #include "nodestack.h"
  10 #include "schedule.h"
  11 #include "common.h"
  12 #include "clockvector.h"
  13 #include "cyclegraph.h"
  14 #include "datarace.h"
  15 #include "threads-model.h"
  16 #include "bugmessage.h"
  17 #include "fuzzer.h"
  18
  19 #define INITIAL_THREAD_ID       0
  20
  21 /**
  22  * Structure for holding small ModelChecker members that should be snapshotted
  23  */
  24 struct model_snapshot_members {
  25         model_snapshot_members() :
  26                 /* First thread created will have id INITIAL_THREAD_ID */
  27                 next_thread_id(INITIAL_THREAD_ID),
  28                 used_sequence_numbers(0),
  29                 bugs(),
  30                 bad_synchronization(false),
  31                 bad_sc_read(false),
  32                 asserted(false)
  33         { }
  34
  35         ~model_snapshot_members() {
  36                 for (unsigned int i = 0;i < bugs.size();i++)
  37                         delete bugs[i];
  38                 bugs.clear();
  39         }
  40
  41         unsigned int next_thread_id;
  42         modelclock_t used_sequence_numbers;
  43         SnapVector<bug_message *> bugs;
  44         /** @brief Incorrectly-ordered synchronization was made */
  45         bool bad_synchronization;
  46         bool bad_sc_read;
  47         bool asserted;
  48
  49         SNAPSHOTALLOC
  50 };
  51
  52 /** @brief Constructor */
  53 ModelExecution::ModelExecution(ModelChecker *m,
  54                                                                                                                          Scheduler *scheduler,
  55                                                                                                                          NodeStack *node_stack) :
  56         model(m),
  57         params(NULL),
  58         scheduler(scheduler),
  59         action_trace(),
  60         thread_map(2),  /* We'll always need at least 2 threads */
  61         pthread_map(0),
  62         pthread_counter(0),
  63         obj_map(),
  64         condvar_waiters_map(),
  65         obj_thrd_map(),
  66         mutex_map(),
  67         thrd_last_action(1),
  68         thrd_last_fence_release(),
  69         node_stack(node_stack),
  70         priv(new struct model_snapshot_members ()),
  71                          mo_graph(new CycleGraph()),
  72         fuzzer(new Fuzzer())
  73 {
  74         /* Initialize a model-checker thread, for special ModelActions */
  75         model_thread = new Thread(get_next_id());
  76         add_thread(model_thread);
  77         scheduler->register_engine(this);
  78         node_stack->register_engine(this);
  79 }
  80
  81 /** @brief Destructor */
  82 ModelExecution::~ModelExecution()
  83 {
  84         for (unsigned int i = 0;i < get_num_threads();i++)
  85                 delete get_thread(int_to_id(i));
  86
  87         delete mo_graph;
  88         delete priv;
  89 }
  90
  91 int ModelExecution::get_execution_number() const
  92 {
  93         return model->get_execution_number();
  94 }
  95
  96 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
  97 {
  98         action_list_t *tmp = hash->get(ptr);
  99         if (tmp == NULL) {
 100                 tmp = new action_list_t();
 101                 hash->put(ptr, tmp);
 102         }
 103         return tmp;
 104 }
 105
 106 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
 107 {
 108         SnapVector<action_list_t> *tmp = hash->get(ptr);
 109         if (tmp == NULL) {
 110                 tmp = new SnapVector<action_list_t>();
 111                 hash->put(ptr, tmp);
 112         }
 113         return tmp;
 114 }
 115
 116 action_list_t * ModelExecution::get_actions_on_obj(void * obj, thread_id_t tid) const
 117 {
 118         SnapVector<action_list_t> *wrv = obj_thrd_map.get(obj);
 119         if (wrv==NULL)
 120                 return NULL;
 121         unsigned int thread=id_to_int(tid);
 122         if (thread < wrv->size())
 123                 return &(*wrv)[thread];
 124         else
 125                 return NULL;
 126 }
 127
 128 /** @return a thread ID for a new Thread */
 129 thread_id_t ModelExecution::get_next_id()
 130 {
 131         return priv->next_thread_id++;
 132 }
 133
 134 /** @return the number of user threads created during this execution */
 135 unsigned int ModelExecution::get_num_threads() const
 136 {
 137         return priv->next_thread_id;
 138 }
 139
 140 /** @return a sequence number for a new ModelAction */
 141 modelclock_t ModelExecution::get_next_seq_num()
 142 {
 143         return ++priv->used_sequence_numbers;
 144 }
 145
 146 /**
 147  * @brief Should the current action wake up a given thread?
 148  *
 149  * @param curr The current action
 150  * @param thread The thread that we might wake up
 151  * @return True, if we should wake up the sleeping thread; false otherwise
 152  */
 153 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
 154 {
 155         const ModelAction *asleep = thread->get_pending();
 156         /* Don't allow partial RMW to wake anyone up */
 157         if (curr->is_rmwr())
 158                 return false;
 159         /* Synchronizing actions may have been backtracked */
 160         if (asleep->could_synchronize_with(curr))
 161                 return true;
 162         /* All acquire/release fences and fence-acquire/store-release */
 163         if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
 164                 return true;
 165         /* Fence-release + store can awake load-acquire on the same location */
 166         if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
 167                 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
 168                 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
 169                         return true;
 170         }
 171         return false;
 172 }
 173
 174 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 175 {
 176         for (unsigned int i = 0;i < get_num_threads();i++) {
 177                 Thread *thr = get_thread(int_to_id(i));
 178                 if (scheduler->is_sleep_set(thr)) {
 179                         if (should_wake_up(curr, thr))
 180                                 /* Remove this thread from sleep set */
 181                                 scheduler->remove_sleep(thr);
 182                 }
 183         }
 184 }
 185
 186 /** @brief Alert the model-checker that an incorrectly-ordered
 187  * synchronization was made */
 188 void ModelExecution::set_bad_synchronization()
 189 {
 190         priv->bad_synchronization = true;
 191 }
 192
 193 /** @brief Alert the model-checker that an incorrectly-ordered
 194  * synchronization was made */
 195 void ModelExecution::set_bad_sc_read()
 196 {
 197         priv->bad_sc_read = true;
 198 }
 199
 200 bool ModelExecution::assert_bug(const char *msg)
 201 {
 202         priv->bugs.push_back(new bug_message(msg));
 203
 204         if (isfeasibleprefix()) {
 205                 set_assert();
 206                 return true;
 207         }
 208         return false;
 209 }
 210
 211 /** @return True, if any bugs have been reported for this execution */
 212 bool ModelExecution::have_bug_reports() const
 213 {
 214         return priv->bugs.size() != 0;
 215 }
 216
 217 SnapVector<bug_message *> * ModelExecution::get_bugs() const
 218 {
 219         return &priv->bugs;
 220 }
 221
 222 /**
 223  * Check whether the current trace has triggered an assertion which should halt
 224  * its execution.
 225  *
 226  * @return True, if the execution should be aborted; false otherwise
 227  */
 228 bool ModelExecution::has_asserted() const
 229 {
 230         return priv->asserted;
 231 }
 232
 233 /**
 234  * Trigger a trace assertion which should cause this execution to be halted.
 235  * This can be due to a detected bug or due to an infeasibility that should
 236  * halt ASAP.
 237  */
 238 void ModelExecution::set_assert()
 239 {
 240         priv->asserted = true;
 241 }
 242
 243 /**
 244  * Check if we are in a deadlock. Should only be called at the end of an
 245  * execution, although it should not give false positives in the middle of an
 246  * execution (there should be some ENABLED thread).
 247  *
 248  * @return True if program is in a deadlock; false otherwise
 249  */
 250 bool ModelExecution::is_deadlocked() const
 251 {
 252         bool blocking_threads = false;
 253         for (unsigned int i = 0;i < get_num_threads();i++) {
 254                 thread_id_t tid = int_to_id(i);
 255                 if (is_enabled(tid))
 256                         return false;
 257                 Thread *t = get_thread(tid);
 258                 if (!t->is_model_thread() && t->get_pending())
 259                         blocking_threads = true;
 260         }
 261         return blocking_threads;
 262 }
 263
 264 /**
 265  * Check if this is a complete execution. That is, have all thread completed
 266  * execution (rather than exiting because sleep sets have forced a redundant
 267  * execution).
 268  *
 269  * @return True if the execution is complete.
 270  */
 271 bool ModelExecution::is_complete_execution() const
 272 {
 273         for (unsigned int i = 0;i < get_num_threads();i++)
 274                 if (is_enabled(int_to_id(i)))
 275                         return false;
 276         return true;
 277 }
 278
 279
 280 /**
 281  * Processes a read model action.
 282  * @param curr is the read model action to process.
 283  * @param rf_set is the set of model actions we can possibly read from
 284  * @return True if processing this read updates the mo_graph.
 285  */
 286 bool ModelExecution::process_read(ModelAction *curr, ModelVector<ModelAction *> * rf_set)
 287 {
 288         while(true) {
 289
 290                 int index = fuzzer->selectWrite(curr, rf_set);
 291                 const ModelAction *rf = (*rf_set)[index];
 292
 293
 294                 ASSERT(rf);
 295
 296                 mo_graph->startChanges();
 297                 bool updated = r_modification_order(curr, rf);
 298                 if (!is_infeasible()) {
 299                         read_from(curr, rf);
 300                         mo_graph->commitChanges();
 301                         get_thread(curr)->set_return_value(curr->get_return_value());
 302                         return updated;
 303                 }
 304                 mo_graph->rollbackChanges();
 305                 (*rf_set)[index] = rf_set->back();
 306                 rf_set->pop_back();
 307         }
 308 }
 309
 310 /**
 311  * Processes a lock, trylock, or unlock model action.  @param curr is
 312  * the read model action to process.
 313  *
 314  * The try lock operation checks whether the lock is taken.  If not,
 315  * it falls to the normal lock operation case.  If so, it returns
 316  * fail.
 317  *
 318  * The lock operation has already been checked that it is enabled, so
 319  * it just grabs the lock and synchronizes with the previous unlock.
 320  *
 321  * The unlock operation has to re-enable all of the threads that are
 322  * waiting on the lock.
 323  *
 324  * @return True if synchronization was updated; false otherwise
 325  */
 326 bool ModelExecution::process_mutex(ModelAction *curr)
 327 {
 328         cdsc::mutex *mutex = curr->get_mutex();
 329         struct cdsc::mutex_state *state = NULL;
 330
 331         if (mutex)
 332                 state = mutex->get_state();
 333
 334         switch (curr->get_type()) {
 335         case ATOMIC_TRYLOCK: {
 336                 bool success = !state->locked;
 337                 curr->set_try_lock(success);
 338                 if (!success) {
 339                         get_thread(curr)->set_return_value(0);
 340                         break;
 341                 }
 342                 get_thread(curr)->set_return_value(1);
 343         }
 344         //otherwise fall into the lock case
 345         case ATOMIC_LOCK: {
 346                 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
 347                         assert_bug("Lock access before initialization");
 348                 state->locked = get_thread(curr);
 349                 ModelAction *unlock = get_last_unlock(curr);
 350                 //synchronize with the previous unlock statement
 351                 if (unlock != NULL) {
 352                         synchronize(unlock, curr);
 353                         return true;
 354                 }
 355                 break;
 356         }
 357         case ATOMIC_WAIT:
 358         case ATOMIC_UNLOCK: {
 359                 /* wake up the other threads */
 360                 for (unsigned int i = 0;i < get_num_threads();i++) {
 361                         Thread *t = get_thread(int_to_id(i));
 362                         Thread *curr_thrd = get_thread(curr);
 363                         if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
 364                                 scheduler->wake(t);
 365                 }
 366
 367                 /* unlock the lock - after checking who was waiting on it */
 368                 state->locked = NULL;
 369
 370                 if (!curr->is_wait())
 371                         break;/* The rest is only for ATOMIC_WAIT */
 372
 373                 break;
 374         }
 375         case ATOMIC_NOTIFY_ALL: {
 376                 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
 377                 //activate all the waiting threads
 378                 for (action_list_t::iterator rit = waiters->begin();rit != waiters->end();rit++) {
 379                         scheduler->wake(get_thread(*rit));
 380                 }
 381                 waiters->clear();
 382                 break;
 383         }
 384         case ATOMIC_NOTIFY_ONE: {
 385                 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
 386                 Thread * thread = fuzzer->selectNotify(waiters);
 387                 scheduler->wake(thread);
 388                 break;
 389         }
 390
 391         default:
 392                 ASSERT(0);
 393         }
 394         return false;
 395 }
 396
 397 /**
 398  * Process a write ModelAction
 399  * @param curr The ModelAction to process
 400  * @return True if the mo_graph was updated or promises were resolved
 401  */
 402 bool ModelExecution::process_write(ModelAction *curr)
 403 {
 404
 405         bool updated_mod_order = w_modification_order(curr);
 406
 407         mo_graph->commitChanges();
 408
 409         get_thread(curr)->set_return_value(VALUE_NONE);
 410         return updated_mod_order;
 411 }
 412
 413 /**
 414  * Process a fence ModelAction
 415  * @param curr The ModelAction to process
 416  * @return True if synchronization was updated
 417  */
 418 bool ModelExecution::process_fence(ModelAction *curr)
 419 {
 420         /*
 421          * fence-relaxed: no-op
 422          * fence-release: only log the occurence (not in this function), for
 423          *   use in later synchronization
 424          * fence-acquire (this function): search for hypothetical release
 425          *   sequences
 426          * fence-seq-cst: MO constraints formed in {r,w}_modification_order
 427          */
 428         bool updated = false;
 429         if (curr->is_acquire()) {
 430                 action_list_t *list = &action_trace;
 431                 action_list_t::reverse_iterator rit;
 432                 /* Find X : is_read(X) && X --sb-> curr */
 433                 for (rit = list->rbegin();rit != list->rend();rit++) {
 434                         ModelAction *act = *rit;
 435                         if (act == curr)
 436                                 continue;
 437                         if (act->get_tid() != curr->get_tid())
 438                                 continue;
 439                         /* Stop at the beginning of the thread */
 440                         if (act->is_thread_start())
 441                                 break;
 442                         /* Stop once we reach a prior fence-acquire */
 443                         if (act->is_fence() && act->is_acquire())
 444                                 break;
 445                         if (!act->is_read())
 446                                 continue;
 447                         /* read-acquire will find its own release sequences */
 448                         if (act->is_acquire())
 449                                 continue;
 450
 451                         /* Establish hypothetical release sequences */
 452                         rel_heads_list_t release_heads;
 453                         get_release_seq_heads(curr, act, &release_heads);
 454                         for (unsigned int i = 0;i < release_heads.size();i++)
 455                                 synchronize(release_heads[i], curr);
 456                         if (release_heads.size() != 0)
 457                                 updated = true;
 458                 }
 459         }
 460         return updated;
 461 }
 462
 463 /**
 464  * @brief Process the current action for thread-related activity
 465  *
 466  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
 467  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
 468  * synchronization, etc.  This function is a no-op for non-THREAD actions
 469  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
 470  *
 471  * @param curr The current action
 472  * @return True if synchronization was updated or a thread completed
 473  */
 474 bool ModelExecution::process_thread_action(ModelAction *curr)
 475 {
 476         bool updated = false;
 477
 478         switch (curr->get_type()) {
 479         case THREAD_CREATE: {
 480                 thrd_t *thrd = (thrd_t *)curr->get_location();
 481                 struct thread_params *params = (struct thread_params *)curr->get_value();
 482                 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
 483                 curr->set_thread_operand(th);
 484                 add_thread(th);
 485                 th->set_creation(curr);
 486                 break;
 487         }
 488         case PTHREAD_CREATE: {
 489                 (*(uint32_t *)curr->get_location()) = pthread_counter++;
 490
 491                 struct pthread_params *params = (struct pthread_params *)curr->get_value();
 492                 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
 493                 curr->set_thread_operand(th);
 494                 add_thread(th);
 495                 th->set_creation(curr);
 496
 497                 if ( pthread_map.size() < pthread_counter )
 498                         pthread_map.resize( pthread_counter );
 499                 pthread_map[ pthread_counter-1 ] = th;
 500
 501                 break;
 502         }
 503         case THREAD_JOIN: {
 504                 Thread *blocking = curr->get_thread_operand();
 505                 ModelAction *act = get_last_action(blocking->get_id());
 506                 synchronize(act, curr);
 507                 updated = true; /* trigger rel-seq checks */
 508                 break;
 509         }
 510         case PTHREAD_JOIN: {
 511                 Thread *blocking = curr->get_thread_operand();
 512                 ModelAction *act = get_last_action(blocking->get_id());
 513                 synchronize(act, curr);
 514                 updated = true; /* trigger rel-seq checks */
 515                 break;  // WL: to be add (modified)
 516         }
 517
 518         case THREAD_FINISH: {
 519                 Thread *th = get_thread(curr);
 520                 /* Wake up any joining threads */
 521                 for (unsigned int i = 0;i < get_num_threads();i++) {
 522                         Thread *waiting = get_thread(int_to_id(i));
 523                         if (waiting->waiting_on() == th &&
 524                                         waiting->get_pending()->is_thread_join())
 525                                 scheduler->wake(waiting);
 526                 }
 527                 th->complete();
 528                 updated = true; /* trigger rel-seq checks */
 529                 break;
 530         }
 531         case THREAD_START: {
 532                 break;
 533         }
 534         default:
 535                 break;
 536         }
 537
 538         return updated;
 539 }
 540
 541 /**
 542  * Initialize the current action by performing one or more of the following
 543  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
 544  * in the NodeStack, manipulating backtracking sets, allocating and
 545  * initializing clock vectors, and computing the promises to fulfill.
 546  *
 547  * @param curr The current action, as passed from the user context; may be
 548  * freed/invalidated after the execution of this function, with a different
 549  * action "returned" its place (pass-by-reference)
 550  * @return True if curr is a newly-explored action; false otherwise
 551  */
 552 bool ModelExecution::initialize_curr_action(ModelAction **curr)
 553 {
 554         ModelAction *newcurr;
 555
 556         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
 557                 newcurr = process_rmw(*curr);
 558                 delete *curr;
 559
 560                 *curr = newcurr;
 561                 return false;
 562         }
 563
 564         (*curr)->set_seq_number(get_next_seq_num());
 565
 566         newcurr = node_stack->explore_action(*curr);
 567         if (newcurr) {
 568                 /* First restore type and order in case of RMW operation */
 569                 if ((*curr)->is_rmwr())
 570                         newcurr->copy_typeandorder(*curr);
 571
 572                 ASSERT((*curr)->get_location() == newcurr->get_location());
 573                 newcurr->copy_from_new(*curr);
 574
 575                 /* Discard duplicate ModelAction; use action from NodeStack */
 576                 delete *curr;
 577
 578                 /* Always compute new clock vector */
 579                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 580
 581                 *curr = newcurr;
 582                 return false;   /* Action was explored previously */
 583         } else {
 584                 newcurr = *curr;
 585
 586                 /* Always compute new clock vector */
 587                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 588
 589                 /* Assign most recent release fence */
 590                 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
 591
 592                 return true;    /* This was a new ModelAction */
 593         }
 594 }
 595
 596 /**
 597  * @brief Establish reads-from relation between two actions
 598  *
 599  * Perform basic operations involved with establishing a concrete rf relation,
 600  * including setting the ModelAction data and checking for release sequences.
 601  *
 602  * @param act The action that is reading (must be a read)
 603  * @param rf The action from which we are reading (must be a write)
 604  *
 605  * @return True if this read established synchronization
 606  */
 607
 608 bool ModelExecution::read_from(ModelAction *act, const ModelAction *rf)
 609 {
 610         ASSERT(rf);
 611         ASSERT(rf->is_write());
 612
 613         act->set_read_from(rf);
 614         if (act->is_acquire()) {
 615                 rel_heads_list_t release_heads;
 616                 get_release_seq_heads(act, act, &release_heads);
 617                 int num_heads = release_heads.size();
 618                 for (unsigned int i = 0;i < release_heads.size();i++)
 619                         if (!synchronize(release_heads[i], act))
 620                                 num_heads--;
 621                 return num_heads > 0;
 622         }
 623         return false;
 624 }
 625
 626 /**
 627  * @brief Synchronizes two actions
 628  *
 629  * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
 630  * This function performs the synchronization as well as providing other hooks
 631  * for other checks along with synchronization.
 632  *
 633  * @param first The left-hand side of the synchronizes-with relation
 634  * @param second The right-hand side of the synchronizes-with relation
 635  * @return True if the synchronization was successful (i.e., was consistent
 636  * with the execution order); false otherwise
 637  */
 638 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
 639 {
 640         if (*second < *first) {
 641                 set_bad_synchronization();
 642                 return false;
 643         }
 644         return second->synchronize_with(first);
 645 }
 646
 647 /**
 648  * @brief Check whether a model action is enabled.
 649  *
 650  * Checks whether an operation would be successful (i.e., is a lock already
 651  * locked, or is the joined thread already complete).
 652  *
 653  * For yield-blocking, yields are never enabled.
 654  *
 655  * @param curr is the ModelAction to check whether it is enabled.
 656  * @return a bool that indicates whether the action is enabled.
 657  */
 658 bool ModelExecution::check_action_enabled(ModelAction *curr) {
 659         if (curr->is_lock()) {
 660                 cdsc::mutex *lock = curr->get_mutex();
 661                 struct cdsc::mutex_state *state = lock->get_state();
 662                 if (state->locked)
 663                         return false;
 664         } else if (curr->is_thread_join()) {
 665                 Thread *blocking = curr->get_thread_operand();
 666                 if (!blocking->is_complete()) {
 667                         return false;
 668                 }
 669         }
 670
 671         return true;
 672 }
 673
 674 /**
 675  * This is the heart of the model checker routine. It performs model-checking
 676  * actions corresponding to a given "current action." Among other processes, it
 677  * calculates reads-from relationships, updates synchronization clock vectors,
 678  * forms a memory_order constraints graph, and handles replay/backtrack
 679  * execution when running permutations of previously-observed executions.
 680  *
 681  * @param curr The current action to process
 682  * @return The ModelAction that is actually executed; may be different than
 683  * curr
 684  */
 685 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 686 {
 687         ASSERT(curr);
 688         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
 689         bool newly_explored = initialize_curr_action(&curr);
 690
 691         DBG();
 692
 693         wake_up_sleeping_actions(curr);
 694
 695         /* Add the action to lists before any other model-checking tasks */
 696         if (!second_part_of_rmw)
 697                 add_action_to_lists(curr);
 698
 699         ModelVector<ModelAction *> * rf_set = NULL;
 700         /* Build may_read_from set for newly-created actions */
 701         if (newly_explored && curr->is_read())
 702                 rf_set = build_may_read_from(curr);
 703
 704         process_thread_action(curr);
 705
 706         if (curr->is_read() && !second_part_of_rmw) {
 707                 process_read(curr, rf_set);
 708                 delete rf_set;
 709         } else {
 710                 ASSERT(rf_set == NULL);
 711         }
 712
 713         if (curr->is_write())
 714                 process_write(curr);
 715
 716         if (curr->is_fence())
 717                 process_fence(curr);
 718
 719         if (curr->is_mutex_op())
 720                 process_mutex(curr);
 721
 722         return curr;
 723 }
 724
 725 /**
 726  * This is the strongest feasibility check available.
 727  * @return whether the current trace (partial or complete) must be a prefix of
 728  * a feasible trace.
 729  */
 730 bool ModelExecution::isfeasibleprefix() const
 731 {
 732         return !is_infeasible();
 733 }
 734
 735 /**
 736  * Print disagnostic information about an infeasible execution
 737  * @param prefix A string to prefix the output with; if NULL, then a default
 738  * message prefix will be provided
 739  */
 740 void ModelExecution::print_infeasibility(const char *prefix) const
 741 {
 742         char buf[100];
 743         char *ptr = buf;
 744         if (mo_graph->checkForCycles())
 745                 ptr += sprintf(ptr, "[mo cycle]");
 746         if (priv->bad_synchronization)
 747                 ptr += sprintf(ptr, "[bad sw ordering]");
 748         if (priv->bad_sc_read)
 749                 ptr += sprintf(ptr, "[bad sc read]");
 750         if (ptr != buf)
 751                 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
 752 }
 753
 754 /**
 755  * Check if the current partial trace is infeasible. Does not check any
 756  * end-of-execution flags, which might rule out the execution. Thus, this is
 757  * useful only for ruling an execution as infeasible.
 758  * @return whether the current partial trace is infeasible.
 759  */
 760 bool ModelExecution::is_infeasible() const
 761 {
 762         return mo_graph->checkForCycles() ||
 763                                  priv->bad_synchronization ||
 764                                  priv->bad_sc_read;
 765 }
 766
 767 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 768 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
 769         ModelAction *lastread = get_last_action(act->get_tid());
 770         lastread->process_rmw(act);
 771         if (act->is_rmw()) {
 772                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
 773                 mo_graph->commitChanges();
 774         }
 775         return lastread;
 776 }
 777
 778 /**
 779  * @brief Updates the mo_graph with the constraints imposed from the current
 780  * read.
 781  *
 782  * Basic idea is the following: Go through each other thread and find
 783  * the last action that happened before our read.  Two cases:
 784  *
 785  * -# The action is a write: that write must either occur before
 786  * the write we read from or be the write we read from.
 787  * -# The action is a read: the write that that action read from
 788  * must occur before the write we read from or be the same write.
 789  *
 790  * @param curr The current action. Must be a read.
 791  * @param rf The ModelAction or Promise that curr reads from. Must be a write.
 792  * @return True if modification order edges were added; false otherwise
 793  */
 794 template <typename rf_type>
 795 bool ModelExecution::r_modification_order(ModelAction *curr, const rf_type *rf)
 796 {
 797         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
 798         unsigned int i;
 799         bool added = false;
 800         ASSERT(curr->is_read());
 801
 802         /* Last SC fence in the current thread */
 803         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
 804         ModelAction *last_sc_write = NULL;
 805         if (curr->is_seqcst())
 806                 last_sc_write = get_last_seq_cst_write(curr);
 807
 808         /* Iterate over all threads */
 809         for (i = 0;i < thrd_lists->size();i++) {
 810                 /* Last SC fence in thread i */
 811                 ModelAction *last_sc_fence_thread_local = NULL;
 812                 if (int_to_id((int)i) != curr->get_tid())
 813                         last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
 814
 815                 /* Last SC fence in thread i, before last SC fence in current thread */
 816                 ModelAction *last_sc_fence_thread_before = NULL;
 817                 if (last_sc_fence_local)
 818                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
 819
 820                 /* Iterate over actions in thread, starting from most recent */
 821                 action_list_t *list = &(*thrd_lists)[i];
 822                 action_list_t::reverse_iterator rit;
 823                 for (rit = list->rbegin();rit != list->rend();rit++) {
 824                         ModelAction *act = *rit;
 825
 826                         /* Skip curr */
 827                         if (act == curr)
 828                                 continue;
 829                         /* Don't want to add reflexive edges on 'rf' */
 830                         if (act->equals(rf)) {
 831                                 if (act->happens_before(curr))
 832                                         break;
 833                                 else
 834                                         continue;
 835                         }
 836
 837                         if (act->is_write()) {
 838                                 /* C++, Section 29.3 statement 5 */
 839                                 if (curr->is_seqcst() && last_sc_fence_thread_local &&
 840                                                 *act < *last_sc_fence_thread_local) {
 841                                         added = mo_graph->addEdge(act, rf) || added;
 842                                         break;
 843                                 }
 844                                 /* C++, Section 29.3 statement 4 */
 845                                 else if (act->is_seqcst() && last_sc_fence_local &&
 846                                                                  *act < *last_sc_fence_local) {
 847                                         added = mo_graph->addEdge(act, rf) || added;
 848                                         break;
 849                                 }
 850                                 /* C++, Section 29.3 statement 6 */
 851                                 else if (last_sc_fence_thread_before &&
 852                                                                  *act < *last_sc_fence_thread_before) {
 853                                         added = mo_graph->addEdge(act, rf) || added;
 854                                         break;
 855                                 }
 856                         }
 857
 858                         /*
 859                          * Include at most one act per-thread that "happens
 860                          * before" curr
 861                          */
 862                         if (act->happens_before(curr)) {
 863                                 if (act->is_write()) {
 864                                         added = mo_graph->addEdge(act, rf) || added;
 865                                 } else {
 866                                         const ModelAction *prevrf = act->get_reads_from();
 867                                         if (!prevrf->equals(rf))
 868                                                 added = mo_graph->addEdge(prevrf, rf) || added;
 869                                 }
 870                                 break;
 871                         }
 872                 }
 873         }
 874
 875         return added;
 876 }
 877
 878 /**
 879  * Updates the mo_graph with the constraints imposed from the current write.
 880  *
 881  * Basic idea is the following: Go through each other thread and find
 882  * the lastest action that happened before our write.  Two cases:
 883  *
 884  * (1) The action is a write => that write must occur before
 885  * the current write
 886  *
 887  * (2) The action is a read => the write that that action read from
 888  * must occur before the current write.
 889  *
 890  * This method also handles two other issues:
 891  *
 892  * (I) Sequential Consistency: Making sure that if the current write is
 893  * seq_cst, that it occurs after the previous seq_cst write.
 894  *
 895  * (II) Sending the write back to non-synchronizing reads.
 896  *
 897  * @param curr The current action. Must be a write.
 898  * @param send_fv A vector for stashing reads to which we may pass our future
 899  * value. If NULL, then don't record any future values.
 900  * @return True if modification order edges were added; false otherwise
 901  */
 902 bool ModelExecution::w_modification_order(ModelAction *curr)
 903 {
 904         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
 905         unsigned int i;
 906         bool added = false;
 907         ASSERT(curr->is_write());
 908
 909         if (curr->is_seqcst()) {
 910                 /* We have to at least see the last sequentially consistent write,
 911                          so we are initialized. */
 912                 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
 913                 if (last_seq_cst != NULL) {
 914                         added = mo_graph->addEdge(last_seq_cst, curr) || added;
 915                 }
 916         }
 917
 918         /* Last SC fence in the current thread */
 919         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
 920
 921         /* Iterate over all threads */
 922         for (i = 0;i < thrd_lists->size();i++) {
 923                 /* Last SC fence in thread i, before last SC fence in current thread */
 924                 ModelAction *last_sc_fence_thread_before = NULL;
 925                 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
 926                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
 927
 928                 /* Iterate over actions in thread, starting from most recent */
 929                 action_list_t *list = &(*thrd_lists)[i];
 930                 action_list_t::reverse_iterator rit;
 931                 for (rit = list->rbegin();rit != list->rend();rit++) {
 932                         ModelAction *act = *rit;
 933                         if (act == curr) {
 934                                 /*
 935                                  * 1) If RMW and it actually read from something, then we
 936                                  * already have all relevant edges, so just skip to next
 937                                  * thread.
 938                                  *
 939                                  * 2) If RMW and it didn't read from anything, we should
 940                                  * whatever edge we can get to speed up convergence.
 941                                  *
 942                                  * 3) If normal write, we need to look at earlier actions, so
 943                                  * continue processing list.
 944                                  */
 945                                 if (curr->is_rmw()) {
 946                                         if (curr->get_reads_from() != NULL)
 947                                                 break;
 948                                         else
 949                                                 continue;
 950                                 } else
 951                                         continue;
 952                         }
 953
 954                         /* C++, Section 29.3 statement 7 */
 955                         if (last_sc_fence_thread_before && act->is_write() &&
 956                                         *act < *last_sc_fence_thread_before) {
 957                                 added = mo_graph->addEdge(act, curr) || added;
 958                                 break;
 959                         }
 960
 961                         /*
 962                          * Include at most one act per-thread that "happens
 963                          * before" curr
 964                          */
 965                         if (act->happens_before(curr)) {
 966                                 /*
 967                                  * Note: if act is RMW, just add edge:
 968                                  *   act --mo--> curr
 969                                  * The following edge should be handled elsewhere:
 970                                  *   readfrom(act) --mo--> act
 971                                  */
 972                                 if (act->is_write())
 973                                         added = mo_graph->addEdge(act, curr) || added;
 974                                 else if (act->is_read()) {
 975                                         //if previous read accessed a null, just keep going
 976                                         added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
 977                                 }
 978                                 break;
 979                         } else if (act->is_read() && !act->could_synchronize_with(curr) &&
 980                                                                  !act->same_thread(curr)) {
 981                                 /* We have an action that:
 982                                    (1) did not happen before us
 983                                    (2) is a read and we are a write
 984                                    (3) cannot synchronize with us
 985                                    (4) is in a different thread
 986                                    =>
 987                                    that read could potentially read from our write.  Note that
 988                                    these checks are overly conservative at this point, we'll
 989                                    do more checks before actually removing the
 990                                    pendingfuturevalue.
 991
 992                                  */
 993
 994                         }
 995                 }
 996         }
 997
 998         return added;
 999 }
1000
1001 /**
1002  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1003  * some constraints. This method checks one the following constraint (others
1004  * require compiler support):
1005  *
1006  *   If X --hb-> Y --mo-> Z, then X should not read from Z.
1007  *   If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1008  */
1009 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1010 {
1011         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1012         unsigned int i;
1013         /* Iterate over all threads */
1014         for (i = 0;i < thrd_lists->size();i++) {
1015                 const ModelAction *write_after_read = NULL;
1016
1017                 /* Iterate over actions in thread, starting from most recent */
1018                 action_list_t *list = &(*thrd_lists)[i];
1019                 action_list_t::reverse_iterator rit;
1020                 for (rit = list->rbegin();rit != list->rend();rit++) {
1021                         ModelAction *act = *rit;
1022
1023                         /* Don't disallow due to act == reader */
1024                         if (!reader->happens_before(act) || reader == act)
1025                                 break;
1026                         else if (act->is_write())
1027                                 write_after_read = act;
1028                         else if (act->is_read() && act->get_reads_from() != NULL)
1029                                 write_after_read = act->get_reads_from();
1030                 }
1031
1032                 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1033                         return false;
1034         }
1035         return true;
1036 }
1037
1038 /**
1039  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1040  * The ModelAction under consideration is expected to be taking part in
1041  * release/acquire synchronization as an object of the "reads from" relation.
1042  * Note that this can only provide release sequence support for RMW chains
1043  * which do not read from the future, as those actions cannot be traced until
1044  * their "promise" is fulfilled. Similarly, we may not even establish the
1045  * presence of a release sequence with certainty, as some modification order
1046  * constraints may be decided further in the future. Thus, this function
1047  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1048  * and a boolean representing certainty.
1049  *
1050  * @param rf The action that might be part of a release sequence. Must be a
1051  * write.
1052  * @param release_heads A pass-by-reference style return parameter. After
1053  * execution of this function, release_heads will contain the heads of all the
1054  * relevant release sequences, if any exists with certainty
1055  * @return true, if the ModelExecution is certain that release_heads is complete;
1056  * false otherwise
1057  */
1058 bool ModelExecution::release_seq_heads(const ModelAction *rf,
1059                                                                                                                                                          rel_heads_list_t *release_heads) const
1060 {
1061         /* Only check for release sequences if there are no cycles */
1062         if (mo_graph->checkForCycles())
1063                 return false;
1064
1065         for ( ;rf != NULL;rf = rf->get_reads_from()) {
1066                 ASSERT(rf->is_write());
1067
1068                 if (rf->is_release())
1069                         release_heads->push_back(rf);
1070                 else if (rf->get_last_fence_release())
1071                         release_heads->push_back(rf->get_last_fence_release());
1072                 if (!rf->is_rmw())
1073                         break;/* End of RMW chain */
1074
1075                 /** @todo Need to be smarter here...  In the linux lock
1076                  * example, this will run to the beginning of the program for
1077                  * every acquire. */
1078                 /** @todo The way to be smarter here is to keep going until 1
1079                  * thread has a release preceded by an acquire and you've seen
1080                  *       both. */
1081
1082                 /* acq_rel RMW is a sufficient stopping condition */
1083                 if (rf->is_acquire() && rf->is_release())
1084                         return true;/* complete */
1085         };
1086         ASSERT(rf);     // Needs to be real write
1087
1088         if (rf->is_release())
1089                 return true;/* complete */
1090
1091         /* else relaxed write
1092          * - check for fence-release in the same thread (29.8, stmt. 3)
1093          * - check modification order for contiguous subsequence
1094          *   -> rf must be same thread as release */
1095
1096         const ModelAction *fence_release = rf->get_last_fence_release();
1097         /* Synchronize with a fence-release unconditionally; we don't need to
1098          * find any more "contiguous subsequence..." for it */
1099         if (fence_release)
1100                 release_heads->push_back(fence_release);
1101
1102         return true;    /* complete */
1103 }
1104
1105 /**
1106  * An interface for getting the release sequence head(s) with which a
1107  * given ModelAction must synchronize. This function only returns a non-empty
1108  * result when it can locate a release sequence head with certainty. Otherwise,
1109  * it may mark the internal state of the ModelExecution so that it will handle
1110  * the release sequence at a later time, causing @a acquire to update its
1111  * synchronization at some later point in execution.
1112  *
1113  * @param acquire The 'acquire' action that may synchronize with a release
1114  * sequence
1115  * @param read The read action that may read from a release sequence; this may
1116  * be the same as acquire, or else an earlier action in the same thread (i.e.,
1117  * when 'acquire' is a fence-acquire)
1118  * @param release_heads A pass-by-reference return parameter. Will be filled
1119  * with the head(s) of the release sequence(s), if they exists with certainty.
1120  * @see ModelExecution::release_seq_heads
1121  */
1122 void ModelExecution::get_release_seq_heads(ModelAction *acquire,
1123                                                                                                                                                                          ModelAction *read, rel_heads_list_t *release_heads)
1124 {
1125         const ModelAction *rf = read->get_reads_from();
1126
1127         release_seq_heads(rf, release_heads);
1128 }
1129
1130 /**
1131  * Performs various bookkeeping operations for the current ModelAction. For
1132  * instance, adds action to the per-object, per-thread action vector and to the
1133  * action trace list of all thread actions.
1134  *
1135  * @param act is the ModelAction to add.
1136  */
1137 void ModelExecution::add_action_to_lists(ModelAction *act)
1138 {
1139         int tid = id_to_int(act->get_tid());
1140         ModelAction *uninit = NULL;
1141         int uninit_id = -1;
1142         action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1143         if (list->empty() && act->is_atomic_var()) {
1144                 uninit = get_uninitialized_action(act);
1145                 uninit_id = id_to_int(uninit->get_tid());
1146                 list->push_front(uninit);
1147         }
1148         list->push_back(act);
1149
1150         action_trace.push_back(act);
1151         if (uninit)
1152                 action_trace.push_front(uninit);
1153
1154         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1155         if (tid >= (int)vec->size())
1156                 vec->resize(priv->next_thread_id);
1157         (*vec)[tid].push_back(act);
1158         if (uninit)
1159                 (*vec)[uninit_id].push_front(uninit);
1160
1161         if ((int)thrd_last_action.size() <= tid)
1162                 thrd_last_action.resize(get_num_threads());
1163         thrd_last_action[tid] = act;
1164         if (uninit)
1165                 thrd_last_action[uninit_id] = uninit;
1166
1167         if (act->is_fence() && act->is_release()) {
1168                 if ((int)thrd_last_fence_release.size() <= tid)
1169                         thrd_last_fence_release.resize(get_num_threads());
1170                 thrd_last_fence_release[tid] = act;
1171         }
1172
1173         if (act->is_wait()) {
1174                 void *mutex_loc = (void *) act->get_value();
1175                 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1176
1177                 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1178                 if (tid >= (int)vec->size())
1179                         vec->resize(priv->next_thread_id);
1180                 (*vec)[tid].push_back(act);
1181         }
1182 }
1183
1184 /**
1185  * @brief Get the last action performed by a particular Thread
1186  * @param tid The thread ID of the Thread in question
1187  * @return The last action in the thread
1188  */
1189 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1190 {
1191         int threadid = id_to_int(tid);
1192         if (threadid < (int)thrd_last_action.size())
1193                 return thrd_last_action[id_to_int(tid)];
1194         else
1195                 return NULL;
1196 }
1197
1198 /**
1199  * @brief Get the last fence release performed by a particular Thread
1200  * @param tid The thread ID of the Thread in question
1201  * @return The last fence release in the thread, if one exists; NULL otherwise
1202  */
1203 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1204 {
1205         int threadid = id_to_int(tid);
1206         if (threadid < (int)thrd_last_fence_release.size())
1207                 return thrd_last_fence_release[id_to_int(tid)];
1208         else
1209                 return NULL;
1210 }
1211
1212 /**
1213  * Gets the last memory_order_seq_cst write (in the total global sequence)
1214  * performed on a particular object (i.e., memory location), not including the
1215  * current action.
1216  * @param curr The current ModelAction; also denotes the object location to
1217  * check
1218  * @return The last seq_cst write
1219  */
1220 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1221 {
1222         void *location = curr->get_location();
1223         action_list_t *list = obj_map.get(location);
1224         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1225         action_list_t::reverse_iterator rit;
1226         for (rit = list->rbegin();(*rit) != curr;rit++)
1227                 ;
1228         rit++;  /* Skip past curr */
1229         for ( ;rit != list->rend();rit++)
1230                 if ((*rit)->is_write() && (*rit)->is_seqcst())
1231                         return *rit;
1232         return NULL;
1233 }
1234
1235 /**
1236  * Gets the last memory_order_seq_cst fence (in the total global sequence)
1237  * performed in a particular thread, prior to a particular fence.
1238  * @param tid The ID of the thread to check
1239  * @param before_fence The fence from which to begin the search; if NULL, then
1240  * search for the most recent fence in the thread.
1241  * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1242  */
1243 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1244 {
1245         /* All fences should have location FENCE_LOCATION */
1246         action_list_t *list = obj_map.get(FENCE_LOCATION);
1247
1248         if (!list)
1249                 return NULL;
1250
1251         action_list_t::reverse_iterator rit = list->rbegin();
1252
1253         if (before_fence) {
1254                 for (;rit != list->rend();rit++)
1255                         if (*rit == before_fence)
1256                                 break;
1257
1258                 ASSERT(*rit == before_fence);
1259                 rit++;
1260         }
1261
1262         for (;rit != list->rend();rit++)
1263                 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1264                         return *rit;
1265         return NULL;
1266 }
1267
1268 /**
1269  * Gets the last unlock operation performed on a particular mutex (i.e., memory
1270  * location). This function identifies the mutex according to the current
1271  * action, which is presumed to perform on the same mutex.
1272  * @param curr The current ModelAction; also denotes the object location to
1273  * check
1274  * @return The last unlock operation
1275  */
1276 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1277 {
1278         void *location = curr->get_location();
1279
1280         action_list_t *list = obj_map.get(location);
1281         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1282         action_list_t::reverse_iterator rit;
1283         for (rit = list->rbegin();rit != list->rend();rit++)
1284                 if ((*rit)->is_unlock() || (*rit)->is_wait())
1285                         return *rit;
1286         return NULL;
1287 }
1288
1289 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1290 {
1291         ModelAction *parent = get_last_action(tid);
1292         if (!parent)
1293                 parent = get_thread(tid)->get_creation();
1294         return parent;
1295 }
1296
1297 /**
1298  * Returns the clock vector for a given thread.
1299  * @param tid The thread whose clock vector we want
1300  * @return Desired clock vector
1301  */
1302 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1303 {
1304         return get_parent_action(tid)->get_cv();
1305 }
1306
1307 bool valequals(uint64_t val1, uint64_t val2, int size) {
1308         switch(size) {
1309         case 1:
1310                 return ((uint8_t)val1) == ((uint8_t)val2);
1311         case 2:
1312                 return ((uint16_t)val1) == ((uint16_t)val2);
1313         case 4:
1314                 return ((uint32_t)val1) == ((uint32_t)val2);
1315         case 8:
1316                 return val1==val2;
1317         default:
1318                 ASSERT(0);
1319                 return false;
1320         }
1321 }
1322
1323 /**
1324  * Build up an initial set of all past writes that this 'read' action may read
1325  * from, as well as any previously-observed future values that must still be valid.
1326  *
1327  * @param curr is the current ModelAction that we are exploring; it must be a
1328  * 'read' operation.
1329  */
1330 ModelVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
1331 {
1332         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
1333         unsigned int i;
1334         ASSERT(curr->is_read());
1335
1336         ModelAction *last_sc_write = NULL;
1337
1338         if (curr->is_seqcst())
1339                 last_sc_write = get_last_seq_cst_write(curr);
1340
1341         ModelVector<ModelAction *> * rf_set = new ModelVector<ModelAction *>();
1342
1343         /* Iterate over all threads */
1344         for (i = 0;i < thrd_lists->size();i++) {
1345                 /* Iterate over actions in thread, starting from most recent */
1346                 action_list_t *list = &(*thrd_lists)[i];
1347                 action_list_t::reverse_iterator rit;
1348                 for (rit = list->rbegin();rit != list->rend();rit++) {
1349                         ModelAction *act = *rit;
1350
1351                         /* Only consider 'write' actions */
1352                         if (!act->is_write() || act == curr)
1353                                 continue;
1354
1355                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1356                         bool allow_read = true;
1357
1358                         if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1359                                 allow_read = false;
1360
1361                         /* Need to check whether we will have two RMW reading from the same value */
1362                         if (curr->is_rmwr()) {
1363                                 /* It is okay if we have a failing CAS */
1364                                 if (!curr->is_rmwrcas() ||
1365                                                 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1366                                         //Need to make sure we aren't the second RMW
1367                                         CycleNode * node = mo_graph->getNode_noCreate(act);
1368                                         if (node != NULL && node->getRMW() != NULL) {
1369                                                 //we are the second RMW
1370                                                 allow_read = false;
1371                                         }
1372                                 }
1373                         }
1374
1375                         if (allow_read) {
1376                                 /* Only add feasible reads */
1377                                 mo_graph->startChanges();
1378                                 r_modification_order(curr, act);
1379                                 if (!is_infeasible())
1380                                         rf_set->push_back(act);
1381                                 mo_graph->rollbackChanges();
1382                         }
1383
1384                         /* Include at most one act per-thread that "happens before" curr */
1385                         if (act->happens_before(curr))
1386                                 break;
1387                 }
1388         }
1389
1390         if (DBG_ENABLED()) {
1391                 model_print("Reached read action:\n");
1392                 curr->print();
1393                 model_print("End printing read_from_past\n");
1394         }
1395         return rf_set;
1396 }
1397
1398 /**
1399  * @brief Get an action representing an uninitialized atomic
1400  *
1401  * This function may create a new one or try to retrieve one from the NodeStack
1402  *
1403  * @param curr The current action, which prompts the creation of an UNINIT action
1404  * @return A pointer to the UNINIT ModelAction
1405  */
1406 ModelAction * ModelExecution::get_uninitialized_action(const ModelAction *curr) const
1407 {
1408         Node *node = curr->get_node();
1409         ModelAction *act = node->get_uninit_action();
1410         if (!act) {
1411                 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1412                 node->set_uninit_action(act);
1413         }
1414         act->create_cv(NULL);
1415         return act;
1416 }
1417
1418 static void print_list(const action_list_t *list)
1419 {
1420         action_list_t::const_iterator it;
1421
1422         model_print("------------------------------------------------------------------------------------\n");
1423         model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
1424         model_print("------------------------------------------------------------------------------------\n");
1425
1426         unsigned int hash = 0;
1427
1428         for (it = list->begin();it != list->end();it++) {
1429                 const ModelAction *act = *it;
1430                 if (act->get_seq_number() > 0)
1431                         act->print();
1432                 hash = hash^(hash<<3)^((*it)->hash());
1433         }
1434         model_print("HASH %u\n", hash);
1435         model_print("------------------------------------------------------------------------------------\n");
1436 }
1437
1438 #if SUPPORT_MOD_ORDER_DUMP
1439 void ModelExecution::dumpGraph(char *filename) const
1440 {
1441         char buffer[200];
1442         sprintf(buffer, "%s.dot", filename);
1443         FILE *file = fopen(buffer, "w");
1444         fprintf(file, "digraph %s {\n", filename);
1445         mo_graph->dumpNodes(file);
1446         ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1447
1448         for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1449                 ModelAction *act = *it;
1450                 if (act->is_read()) {
1451                         mo_graph->dot_print_node(file, act);
1452                         mo_graph->dot_print_edge(file,
1453                                                                                                                          act->get_reads_from(),
1454                                                                                                                          act,
1455                                                                                                                          "label=\"rf\", color=red, weight=2");
1456                 }
1457                 if (thread_array[act->get_tid()]) {
1458                         mo_graph->dot_print_edge(file,
1459                                                                                                                          thread_array[id_to_int(act->get_tid())],
1460                                                                                                                          act,
1461                                                                                                                          "label=\"sb\", color=blue, weight=400");
1462                 }
1463
1464                 thread_array[act->get_tid()] = act;
1465         }
1466         fprintf(file, "}\n");
1467         model_free(thread_array);
1468         fclose(file);
1469 }
1470 #endif
1471
1472 /** @brief Prints an execution trace summary. */
1473 void ModelExecution::print_summary() const
1474 {
1475 #if SUPPORT_MOD_ORDER_DUMP
1476         char buffername[100];
1477         sprintf(buffername, "exec%04u", get_execution_number());
1478         mo_graph->dumpGraphToFile(buffername);
1479         sprintf(buffername, "graph%04u", get_execution_number());
1480         dumpGraph(buffername);
1481 #endif
1482
1483         model_print("Execution trace %d:", get_execution_number());
1484         if (isfeasibleprefix()) {
1485                 if (scheduler->all_threads_sleeping())
1486                         model_print(" SLEEP-SET REDUNDANT");
1487                 if (have_bug_reports())
1488                         model_print(" DETECTED BUG(S)");
1489         } else
1490                 print_infeasibility(" INFEASIBLE");
1491         model_print("\n");
1492
1493         print_list(&action_trace);
1494         model_print("\n");
1495
1496 }
1497
1498 /**
1499  * Add a Thread to the system for the first time. Should only be called once
1500  * per thread.
1501  * @param t The Thread to add
1502  */
1503 void ModelExecution::add_thread(Thread *t)
1504 {
1505         unsigned int i = id_to_int(t->get_id());
1506         if (i >= thread_map.size())
1507                 thread_map.resize(i + 1);
1508         thread_map[i] = t;
1509         if (!t->is_model_thread())
1510                 scheduler->add_thread(t);
1511 }
1512
1513 /**
1514  * @brief Get a Thread reference by its ID
1515  * @param tid The Thread's ID
1516  * @return A Thread reference
1517  */
1518 Thread * ModelExecution::get_thread(thread_id_t tid) const
1519 {
1520         unsigned int i = id_to_int(tid);
1521         if (i < thread_map.size())
1522                 return thread_map[i];
1523         return NULL;
1524 }
1525
1526 /**
1527  * @brief Get a reference to the Thread in which a ModelAction was executed
1528  * @param act The ModelAction
1529  * @return A Thread reference
1530  */
1531 Thread * ModelExecution::get_thread(const ModelAction *act) const
1532 {
1533         return get_thread(act->get_tid());
1534 }
1535
1536 /**
1537  * @brief Get a Thread reference by its pthread ID
1538  * @param index The pthread's ID
1539  * @return A Thread reference
1540  */
1541 Thread * ModelExecution::get_pthread(pthread_t pid) {
1542         union {
1543                 pthread_t p;
1544                 uint32_t v;
1545         } x;
1546         x.p = pid;
1547         uint32_t thread_id = x.v;
1548         if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1549         else return NULL;
1550 }
1551
1552 /**
1553  * @brief Check if a Thread is currently enabled
1554  * @param t The Thread to check
1555  * @return True if the Thread is currently enabled
1556  */
1557 bool ModelExecution::is_enabled(Thread *t) const
1558 {
1559         return scheduler->is_enabled(t);
1560 }
1561
1562 /**
1563  * @brief Check if a Thread is currently enabled
1564  * @param tid The ID of the Thread to check
1565  * @return True if the Thread is currently enabled
1566  */
1567 bool ModelExecution::is_enabled(thread_id_t tid) const
1568 {
1569         return scheduler->is_enabled(tid);
1570 }
1571
1572 /**
1573  * @brief Select the next thread to execute based on the curren action
1574  *
1575  * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1576  * actions should be followed by the execution of their child thread. In either
1577  * case, the current action should determine the next thread schedule.
1578  *
1579  * @param curr The current action
1580  * @return The next thread to run, if the current action will determine this
1581  * selection; otherwise NULL
1582  */
1583 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1584 {
1585         /* Do not split atomic RMW */
1586         if (curr->is_rmwr())
1587                 return get_thread(curr);
1588         if (curr->is_write()) {
1589                 std::memory_order order = curr->get_mo();
1590                 switch(order) {
1591                 case std::memory_order_relaxed:
1592                         return get_thread(curr);
1593                 case std::memory_order_release:
1594                         return get_thread(curr);
1595                 default:
1596                         return NULL;
1597                 }
1598         }
1599
1600         /* Follow CREATE with the created thread */
1601         /* which is not needed, because model.cc takes care of this */
1602         if (curr->get_type() == THREAD_CREATE)
1603                 return curr->get_thread_operand();
1604         if (curr->get_type() == PTHREAD_CREATE) {
1605                 return curr->get_thread_operand();
1606         }
1607         return NULL;
1608 }
1609
1610 /**
1611  * Takes the next step in the execution, if possible.
1612  * @param curr The current step to take
1613  * @return Returns the next Thread to run, if any; NULL if this execution
1614  * should terminate
1615  */
1616 Thread * ModelExecution::take_step(ModelAction *curr)
1617 {
1618         Thread *curr_thrd = get_thread(curr);
1619         ASSERT(curr_thrd->get_state() == THREAD_READY);
1620
1621         ASSERT(check_action_enabled(curr));     /* May have side effects? */
1622         curr = check_current_action(curr);
1623         ASSERT(curr);
1624
1625         if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1626                 scheduler->remove_thread(curr_thrd);
1627
1628         return action_select_next_thread(curr);
1629 }
1630
1631 Fuzzer * ModelExecution::getFuzzer() {
1632         return fuzzer;
1633 }