execution.cc

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