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