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