execution.cc

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