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