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