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