execution.cc

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