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