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