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