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