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