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