execution.cc

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