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