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