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