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         thread_map(2),  /* We'll always need at least 2 threads */
  55         pthread_map(0),
  56         pthread_counter(1),
  57         action_trace(),
  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         isfinished(false)
  68 {
  69         /* Initialize a model-checker thread, for special ModelActions */
  70         model_thread = new Thread(get_next_id());
  71         add_thread(model_thread);
  72         fuzzer->register_engine(m->get_history(), this);
  73         scheduler->register_engine(this);
  74 #ifdef TLS
  75         pthread_key_create(&pthreadkey, tlsdestructor);
  76 #endif
  77 }
  78
  79 /** @brief Destructor */
  80 ModelExecution::~ModelExecution()
  81 {
  82         for (unsigned int i = 0;i < get_num_threads();i++)
  83                 delete get_thread(int_to_id(i));
  84
  85         delete mo_graph;
  86         delete priv;
  87 }
  88
  89 int ModelExecution::get_execution_number() const
  90 {
  91         return model->get_execution_number();
  92 }
  93
  94 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
  95 {
  96         action_list_t *tmp = hash->get(ptr);
  97         if (tmp == NULL) {
  98                 tmp = new action_list_t();
  99                 hash->put(ptr, tmp);
 100         }
 101         return tmp;
 102 }
 103
 104 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
 105 {
 106         SnapVector<action_list_t> *tmp = hash->get(ptr);
 107         if (tmp == NULL) {
 108                 tmp = new SnapVector<action_list_t>();
 109                 hash->put(ptr, tmp);
 110         }
 111         return tmp;
 112 }
 113
 114 /** @return a thread ID for a new Thread */
 115 thread_id_t ModelExecution::get_next_id()
 116 {
 117         return priv->next_thread_id++;
 118 }
 119
 120 /** @return the number of user threads created during this execution */
 121 unsigned int ModelExecution::get_num_threads() const
 122 {
 123         return priv->next_thread_id;
 124 }
 125
 126 /** @return a sequence number for a new ModelAction */
 127 modelclock_t ModelExecution::get_next_seq_num()
 128 {
 129         return ++priv->used_sequence_numbers;
 130 }
 131
 132 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
 133 void ModelExecution::restore_last_seq_num()
 134 {
 135         priv->used_sequence_numbers--;
 136 }
 137
 138 /**
 139  * @brief Should the current action wake up a given thread?
 140  *
 141  * @param curr The current action
 142  * @param thread The thread that we might wake up
 143  * @return True, if we should wake up the sleeping thread; false otherwise
 144  */
 145 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
 146 {
 147         const ModelAction *asleep = thread->get_pending();
 148         /* Don't allow partial RMW to wake anyone up */
 149         if (curr->is_rmwr())
 150                 return false;
 151         /* Synchronizing actions may have been backtracked */
 152         if (asleep->could_synchronize_with(curr))
 153                 return true;
 154         /* All acquire/release fences and fence-acquire/store-release */
 155         if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
 156                 return true;
 157         /* Fence-release + store can awake load-acquire on the same location */
 158         if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
 159                 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
 160                 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
 161                         return true;
 162         }
 163         /* The sleep is literally sleeping */
 164         if (asleep->is_sleep()) {
 165                 if (fuzzer->shouldWake(asleep))
 166                         return true;
 167         }
 168
 169         return false;
 170 }
 171
 172 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 173 {
 174         for (unsigned int i = 0;i < get_num_threads();i++) {
 175                 Thread *thr = get_thread(int_to_id(i));
 176                 if (scheduler->is_sleep_set(thr)) {
 177                         if (should_wake_up(curr, thr)) {
 178                                 /* Remove this thread from sleep set */
 179                                 scheduler->remove_sleep(thr);
 180                                 if (thr->get_pending()->is_sleep())
 181                                         thr->set_wakeup_state(true);
 182                         }
 183                 }
 184         }
 185 }
 186
 187 void ModelExecution::assert_bug(const char *msg)
 188 {
 189         priv->bugs.push_back(new bug_message(msg));
 190         set_assert();
 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         uint i = 0;
 294         while (i < rf_set->size()) {
 295                 ModelAction * rf = (*rf_set)[i];
 296                 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
 297                         (*rf_set)[i] = rf_set->back();
 298                         rf_set->pop_back();
 299                 } else
 300                         i++;
 301         }*/
 302
 303         while(true) {
 304                 int index = fuzzer->selectWrite(curr, rf_set);
 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         } else
 724                 ASSERT(rf_set == NULL);
 725
 726         /* Add the action to lists */
 727         if (!second_part_of_rmw)
 728                 add_action_to_lists(curr);
 729
 730         if (curr->is_write())
 731                 add_write_to_lists(curr);
 732
 733         process_thread_action(curr);
 734
 735         if (curr->is_write())
 736                 process_write(curr);
 737
 738         if (curr->is_fence())
 739                 process_fence(curr);
 740
 741         if (curr->is_mutex_op())
 742                 process_mutex(curr);
 743
 744         return curr;
 745 }
 746
 747 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 748 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
 749         ModelAction *lastread = get_last_action(act->get_tid());
 750         lastread->process_rmw(act);
 751         if (act->is_rmw()) {
 752                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
 753         }
 754         return lastread;
 755 }
 756
 757 /**
 758  * @brief Updates the mo_graph with the constraints imposed from the current
 759  * read.
 760  *
 761  * Basic idea is the following: Go through each other thread and find
 762  * the last action that happened before our read.  Two cases:
 763  *
 764  * -# The action is a write: that write must either occur before
 765  * the write we read from or be the write we read from.
 766  * -# The action is a read: the write that that action read from
 767  * must occur before the write we read from or be the same write.
 768  *
 769  * @param curr The current action. Must be a read.
 770  * @param rf The ModelAction or Promise that curr reads from. Must be a write.
 771  * @param check_only If true, then only check whether the current action satisfies
 772  *        read modification order or not, without modifiying priorset and canprune.
 773  *        False by default.
 774  * @return True if modification order edges were added; false otherwise
 775  */
 776
 777 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
 778                                                                                                                                                                         SnapVector<const ModelAction *> * priorset, bool * canprune, bool check_only)
 779 {
 780         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
 781         unsigned int i;
 782         ASSERT(curr->is_read());
 783
 784         /* Last SC fence in the current thread */
 785         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
 786
 787         int tid = curr->get_tid();
 788         ModelAction *prev_same_thread = NULL;
 789         /* Iterate over all threads */
 790         for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
 791                 /* Last SC fence in thread tid */
 792                 ModelAction *last_sc_fence_thread_local = NULL;
 793                 if (i != 0)
 794                         last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
 795
 796                 /* Last SC fence in thread tid, before last SC fence in current thread */
 797                 ModelAction *last_sc_fence_thread_before = NULL;
 798                 if (last_sc_fence_local)
 799                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
 800
 801                 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
 802                 if (prev_same_thread != NULL &&
 803                                 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
 804                                 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
 805                         continue;
 806                 }
 807
 808                 /* Iterate over actions in thread, starting from most recent */
 809                 action_list_t *list = &(*thrd_lists)[tid];
 810                 sllnode<ModelAction *> * rit;
 811                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
 812                         ModelAction *act = rit->getVal();
 813
 814                         /* Skip curr */
 815                         if (act == curr)
 816                                 continue;
 817                         /* Don't want to add reflexive edges on 'rf' */
 818                         if (act->equals(rf)) {
 819                                 if (act->happens_before(curr))
 820                                         break;
 821                                 else
 822                                         continue;
 823                         }
 824
 825                         if (act->is_write()) {
 826                                 /* C++, Section 29.3 statement 5 */
 827                                 if (curr->is_seqcst() && last_sc_fence_thread_local &&
 828                                                 *act < *last_sc_fence_thread_local) {
 829                                         if (mo_graph->checkReachable(rf, act))
 830                                                 return false;
 831                                         if (!check_only)
 832                                                 priorset->push_back(act);
 833                                         break;
 834                                 }
 835                                 /* C++, Section 29.3 statement 4 */
 836                                 else if (act->is_seqcst() && last_sc_fence_local &&
 837                                                                  *act < *last_sc_fence_local) {
 838                                         if (mo_graph->checkReachable(rf, act))
 839                                                 return false;
 840                                         if (!check_only)
 841                                                 priorset->push_back(act);
 842                                         break;
 843                                 }
 844                                 /* C++, Section 29.3 statement 6 */
 845                                 else if (last_sc_fence_thread_before &&
 846                                                                  *act < *last_sc_fence_thread_before) {
 847                                         if (mo_graph->checkReachable(rf, act))
 848                                                 return false;
 849                                         if (!check_only)
 850                                                 priorset->push_back(act);
 851                                         break;
 852                                 }
 853                         }
 854
 855                         /*
 856                          * Include at most one act per-thread that "happens
 857                          * before" curr
 858                          */
 859                         if (act->happens_before(curr)) {
 860                                 if (i==0) {
 861                                         if (last_sc_fence_local == NULL ||
 862                                                         (*last_sc_fence_local < *act)) {
 863                                                 prev_same_thread = act;
 864                                         }
 865                                 }
 866                                 if (act->is_write()) {
 867                                         if (mo_graph->checkReachable(rf, act))
 868                                                 return false;
 869                                         if (!check_only)
 870                                                 priorset->push_back(act);
 871                                 } else {
 872                                         const ModelAction *prevrf = act->get_reads_from();
 873                                         if (!prevrf->equals(rf)) {
 874                                                 if (mo_graph->checkReachable(rf, prevrf))
 875                                                         return false;
 876                                                 if (!check_only)
 877                                                         priorset->push_back(prevrf);
 878                                         } else {
 879                                                 if (act->get_tid() == curr->get_tid()) {
 880                                                         //Can prune curr from obj list
 881                                                         if (!check_only)
 882                                                                 *canprune = true;
 883                                                 }
 884                                         }
 885                                 }
 886                                 break;
 887                         }
 888                 }
 889         }
 890         return true;
 891 }
 892
 893 /**
 894  * Updates the mo_graph with the constraints imposed from the current write.
 895  *
 896  * Basic idea is the following: Go through each other thread and find
 897  * the lastest action that happened before our write.  Two cases:
 898  *
 899  * (1) The action is a write => that write must occur before
 900  * the current write
 901  *
 902  * (2) The action is a read => the write that that action read from
 903  * must occur before the current write.
 904  *
 905  * This method also handles two other issues:
 906  *
 907  * (I) Sequential Consistency: Making sure that if the current write is
 908  * seq_cst, that it occurs after the previous seq_cst write.
 909  *
 910  * (II) Sending the write back to non-synchronizing reads.
 911  *
 912  * @param curr The current action. Must be a write.
 913  * @param send_fv A vector for stashing reads to which we may pass our future
 914  * value. If NULL, then don't record any future values.
 915  * @return True if modification order edges were added; false otherwise
 916  */
 917 void ModelExecution::w_modification_order(ModelAction *curr)
 918 {
 919         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
 920         unsigned int i;
 921         ASSERT(curr->is_write());
 922
 923         SnapList<ModelAction *> edgeset;
 924
 925         if (curr->is_seqcst()) {
 926                 /* We have to at least see the last sequentially consistent write,
 927                          so we are initialized. */
 928                 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
 929                 if (last_seq_cst != NULL) {
 930                         edgeset.push_back(last_seq_cst);
 931                 }
 932                 //update map for next query
 933                 obj_last_sc_map.put(curr->get_location(), curr);
 934         }
 935
 936         /* Last SC fence in the current thread */
 937         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
 938
 939         /* Iterate over all threads */
 940         for (i = 0;i < thrd_lists->size();i++) {
 941                 /* Last SC fence in thread i, before last SC fence in current thread */
 942                 ModelAction *last_sc_fence_thread_before = NULL;
 943                 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
 944                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
 945
 946                 /* Iterate over actions in thread, starting from most recent */
 947                 action_list_t *list = &(*thrd_lists)[i];
 948                 sllnode<ModelAction*>* rit;
 949                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
 950                         ModelAction *act = rit->getVal();
 951                         if (act == curr) {
 952                                 /*
 953                                  * 1) If RMW and it actually read from something, then we
 954                                  * already have all relevant edges, so just skip to next
 955                                  * thread.
 956                                  *
 957                                  * 2) If RMW and it didn't read from anything, we should
 958                                  * whatever edge we can get to speed up convergence.
 959                                  *
 960                                  * 3) If normal write, we need to look at earlier actions, so
 961                                  * continue processing list.
 962                                  */
 963                                 if (curr->is_rmw()) {
 964                                         if (curr->get_reads_from() != NULL)
 965                                                 break;
 966                                         else
 967                                                 continue;
 968                                 } else
 969                                         continue;
 970                         }
 971
 972                         /* C++, Section 29.3 statement 7 */
 973                         if (last_sc_fence_thread_before && act->is_write() &&
 974                                         *act < *last_sc_fence_thread_before) {
 975                                 edgeset.push_back(act);
 976                                 break;
 977                         }
 978
 979                         /*
 980                          * Include at most one act per-thread that "happens
 981                          * before" curr
 982                          */
 983                         if (act->happens_before(curr)) {
 984                                 /*
 985                                  * Note: if act is RMW, just add edge:
 986                                  *   act --mo--> curr
 987                                  * The following edge should be handled elsewhere:
 988                                  *   readfrom(act) --mo--> act
 989                                  */
 990                                 if (act->is_write())
 991                                         edgeset.push_back(act);
 992                                 else if (act->is_read()) {
 993                                         //if previous read accessed a null, just keep going
 994                                         edgeset.push_back(act->get_reads_from());
 995                                 }
 996                                 break;
 997                         }
 998                 }
 999         }
1000         mo_graph->addEdges(&edgeset, curr);
1001
1002 }
1003
1004 /**
1005  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1006  * some constraints. This method checks one the following constraint (others
1007  * require compiler support):
1008  *
1009  *   If X --hb-> Y --mo-> Z, then X should not read from Z.
1010  *   If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1011  */
1012 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1013 {
1014         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1015         unsigned int i;
1016         /* Iterate over all threads */
1017         for (i = 0;i < thrd_lists->size();i++) {
1018                 const ModelAction *write_after_read = NULL;
1019
1020                 /* Iterate over actions in thread, starting from most recent */
1021                 action_list_t *list = &(*thrd_lists)[i];
1022                 sllnode<ModelAction *>* rit;
1023                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1024                         ModelAction *act = rit->getVal();
1025
1026                         /* Don't disallow due to act == reader */
1027                         if (!reader->happens_before(act) || reader == act)
1028                                 break;
1029                         else if (act->is_write())
1030                                 write_after_read = act;
1031                         else if (act->is_read() && act->get_reads_from() != NULL)
1032                                 write_after_read = act->get_reads_from();
1033                 }
1034
1035                 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1036                         return false;
1037         }
1038         return true;
1039 }
1040
1041 /**
1042  * Computes the clock vector that happens before propagates from this write.
1043  *
1044  * @param rf The action that might be part of a release sequence. Must be a
1045  * write.
1046  * @return ClockVector of happens before relation.
1047  */
1048
1049 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1050         SnapVector<ModelAction *> * processset = NULL;
1051         for ( ;rf != NULL;rf = rf->get_reads_from()) {
1052                 ASSERT(rf->is_write());
1053                 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1054                         break;
1055                 if (processset == NULL)
1056                         processset = new SnapVector<ModelAction *>();
1057                 processset->push_back(rf);
1058         }
1059
1060         int i = (processset == NULL) ? 0 : processset->size();
1061
1062         ClockVector * vec = NULL;
1063         while(true) {
1064                 if (rf->get_rfcv() != NULL) {
1065                         vec = rf->get_rfcv();
1066                 } else if (rf->is_acquire() && rf->is_release()) {
1067                         vec = rf->get_cv();
1068                 } else if (rf->is_release() && !rf->is_rmw()) {
1069                         vec = rf->get_cv();
1070                 } else if (rf->is_release()) {
1071                         //have rmw that is release and doesn't have a rfcv
1072                         (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1073                         rf->set_rfcv(vec);
1074                 } else {
1075                         //operation that isn't release
1076                         if (rf->get_last_fence_release()) {
1077                                 if (vec == NULL)
1078                                         vec = rf->get_last_fence_release()->get_cv();
1079                                 else
1080                                         (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1081                         }
1082                         rf->set_rfcv(vec);
1083                 }
1084                 i--;
1085                 if (i >= 0) {
1086                         rf = (*processset)[i];
1087                 } else
1088                         break;
1089         }
1090         if (processset != NULL)
1091                 delete processset;
1092         return vec;
1093 }
1094
1095 /**
1096  * Performs various bookkeeping operations for the current ModelAction when it is
1097  * the first atomic action occurred at its memory location.
1098  *
1099  * For instance, adds uninitialized action to the per-object, per-thread action vector
1100  * and to the action trace list of all thread actions.
1101  *
1102  * @param act is the ModelAction to process.
1103  */
1104 void ModelExecution::add_uninit_action_to_lists(ModelAction *act)
1105 {
1106         int tid = id_to_int(act->get_tid());
1107         ModelAction *uninit = NULL;
1108         int uninit_id = -1;
1109         SnapVector<action_list_t> *objvec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1110         if (objvec->empty() && act->is_atomic_var()) {
1111                 uninit = get_uninitialized_action(act);
1112                 uninit_id = id_to_int(uninit->get_tid());
1113                 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1114                 if ((int)vec->size() <= uninit_id) {
1115                         int oldsize = (int) vec->size();
1116                         vec->resize(uninit_id + 1);
1117                         for(int i = oldsize;i < uninit_id + 1;i++) {
1118                                 new (&(*vec)[i]) action_list_t();
1119                         }
1120                 }
1121                 (*vec)[uninit_id].push_front(uninit);
1122         }
1123
1124         // Update action trace, a total order of all actions
1125         if (uninit)
1126                 action_trace.push_front(uninit);
1127
1128         // Update obj_thrd_map, a per location, per thread, order of actions
1129         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1130         if ((int)vec->size() <= tid) {
1131                 uint oldsize = vec->size();
1132                 vec->resize(priv->next_thread_id);
1133                 for(uint i = oldsize;i < priv->next_thread_id;i++)
1134                         new (&(*vec)[i]) action_list_t();
1135         }
1136         if (uninit)
1137                 (*vec)[uninit_id].push_front(uninit);
1138
1139         // Update thrd_last_action, the last action taken by each thrad
1140         if ((int)thrd_last_action.size() <= tid)
1141                 thrd_last_action.resize(get_num_threads());
1142         if (uninit)
1143                 thrd_last_action[uninit_id] = uninit;
1144 }
1145
1146
1147 /**
1148  * Performs various bookkeeping operations for the current ModelAction. For
1149  * instance, adds action to the per-object, per-thread action vector and to the
1150  * action trace list of all thread actions.
1151  *
1152  * @param act is the ModelAction to add.
1153  */
1154 void ModelExecution::add_action_to_lists(ModelAction *act)
1155 {
1156         int tid = id_to_int(act->get_tid());
1157         if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1158           action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1159           list->push_back(act);
1160         }
1161
1162         // Update action trace, a total order of all actions
1163         action_trace.push_back(act);
1164
1165         // Update obj_thrd_map, a per location, per thread, order of actions
1166         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1167         if ((int)vec->size() <= tid) {
1168                 uint oldsize = vec->size();
1169                 vec->resize(priv->next_thread_id);
1170                 for(uint i = oldsize;i < priv->next_thread_id;i++)
1171                         new (&(*vec)[i]) action_list_t();
1172         }
1173         (*vec)[tid].push_back(act);
1174
1175         // Update thrd_last_action, the last action taken by each thrad
1176         if ((int)thrd_last_action.size() <= tid)
1177                 thrd_last_action.resize(get_num_threads());
1178         thrd_last_action[tid] = act;
1179
1180         // Update thrd_last_fence_release, the last release fence taken by each thread
1181         if (act->is_fence() && act->is_release()) {
1182                 if ((int)thrd_last_fence_release.size() <= tid)
1183                         thrd_last_fence_release.resize(get_num_threads());
1184                 thrd_last_fence_release[tid] = act;
1185         }
1186
1187         if (act->is_wait()) {
1188                 void *mutex_loc = (void *) act->get_value();
1189                 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1190
1191                 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1192                 if ((int)vec->size() <= tid) {
1193                         uint oldsize = vec->size();
1194                         vec->resize(priv->next_thread_id);
1195                         for(uint i = oldsize;i < priv->next_thread_id;i++)
1196                                 new (&(*vec)[i]) action_list_t();
1197                 }
1198                 (*vec)[tid].push_back(act);
1199         }
1200 }
1201
1202 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1203         sllnode<ModelAction*> * rit = list->end();
1204         modelclock_t next_seq = act->get_seq_number();
1205         if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1206                 list->push_back(act);
1207         else {
1208                 for(;rit != NULL;rit=rit->getPrev()) {
1209                         if (rit->getVal()->get_seq_number() == next_seq) {
1210                                 list->insertAfter(rit, act);
1211                                 break;
1212                         }
1213                 }
1214         }
1215 }
1216
1217 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1218         sllnode<ModelAction*> * rit = list->end();
1219         modelclock_t next_seq = act->get_seq_number();
1220         if (rit == NULL) {
1221                 act->create_cv(NULL);
1222         } else if (rit->getVal()->get_seq_number() == next_seq) {
1223                 act->create_cv(rit->getVal());
1224                 list->push_back(act);
1225         } else {
1226                 for(;rit != NULL;rit=rit->getPrev()) {
1227                         if (rit->getVal()->get_seq_number() == next_seq) {
1228                                 act->create_cv(rit->getVal());
1229                                 list->insertAfter(rit, act);
1230                                 break;
1231                         }
1232                 }
1233         }
1234 }
1235
1236 /**
1237  * Performs various bookkeeping operations for a normal write.  The
1238  * complication is that we are typically inserting a normal write
1239  * lazily, so we need to insert it into the middle of lists.
1240  *
1241  * @param act is the ModelAction to add.
1242  */
1243
1244 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1245 {
1246         int tid = id_to_int(act->get_tid());
1247         insertIntoActionListAndSetCV(&action_trace, act);
1248
1249         // Update obj_thrd_map, a per location, per thread, order of actions
1250         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1251         if (tid >= (int)vec->size()) {
1252                 uint oldsize =vec->size();
1253                 vec->resize(priv->next_thread_id);
1254                 for(uint i=oldsize;i<priv->next_thread_id;i++)
1255                         new (&(*vec)[i]) action_list_t();
1256         }
1257         insertIntoActionList(&(*vec)[tid],act);
1258
1259         // Update thrd_last_action, the last action taken by each thrad
1260         if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1261                 thrd_last_action[tid] = act;
1262 }
1263
1264
1265 void ModelExecution::add_write_to_lists(ModelAction *write) {
1266         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1267         int tid = id_to_int(write->get_tid());
1268         if (tid >= (int)vec->size()) {
1269                 uint oldsize =vec->size();
1270                 vec->resize(priv->next_thread_id);
1271                 for(uint i=oldsize;i<priv->next_thread_id;i++)
1272                         new (&(*vec)[i]) action_list_t();
1273         }
1274         (*vec)[tid].push_back(write);
1275 }
1276
1277 /**
1278  * @brief Get the last action performed by a particular Thread
1279  * @param tid The thread ID of the Thread in question
1280  * @return The last action in the thread
1281  */
1282 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1283 {
1284         int threadid = id_to_int(tid);
1285         if (threadid < (int)thrd_last_action.size())
1286                 return thrd_last_action[id_to_int(tid)];
1287         else
1288                 return NULL;
1289 }
1290
1291 /**
1292  * @brief Get the last fence release performed by a particular Thread
1293  * @param tid The thread ID of the Thread in question
1294  * @return The last fence release in the thread, if one exists; NULL otherwise
1295  */
1296 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1297 {
1298         int threadid = id_to_int(tid);
1299         if (threadid < (int)thrd_last_fence_release.size())
1300                 return thrd_last_fence_release[id_to_int(tid)];
1301         else
1302                 return NULL;
1303 }
1304
1305 /**
1306  * Gets the last memory_order_seq_cst write (in the total global sequence)
1307  * performed on a particular object (i.e., memory location), not including the
1308  * current action.
1309  * @param curr The current ModelAction; also denotes the object location to
1310  * check
1311  * @return The last seq_cst write
1312  */
1313 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1314 {
1315         void *location = curr->get_location();
1316         return obj_last_sc_map.get(location);
1317 }
1318
1319 /**
1320  * Gets the last memory_order_seq_cst fence (in the total global sequence)
1321  * performed in a particular thread, prior to a particular fence.
1322  * @param tid The ID of the thread to check
1323  * @param before_fence The fence from which to begin the search; if NULL, then
1324  * search for the most recent fence in the thread.
1325  * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1326  */
1327 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1328 {
1329         /* All fences should have location FENCE_LOCATION */
1330         action_list_t *list = obj_map.get(FENCE_LOCATION);
1331
1332         if (!list)
1333                 return NULL;
1334
1335         sllnode<ModelAction*>* rit = list->end();
1336
1337         if (before_fence) {
1338                 for (;rit != NULL;rit=rit->getPrev())
1339                         if (rit->getVal() == before_fence)
1340                                 break;
1341
1342                 ASSERT(rit->getVal() == before_fence);
1343                 rit=rit->getPrev();
1344         }
1345
1346         for (;rit != NULL;rit=rit->getPrev()) {
1347                 ModelAction *act = rit->getVal();
1348                 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1349                         return act;
1350         }
1351         return NULL;
1352 }
1353
1354 /**
1355  * Gets the last unlock operation performed on a particular mutex (i.e., memory
1356  * location). This function identifies the mutex according to the current
1357  * action, which is presumed to perform on the same mutex.
1358  * @param curr The current ModelAction; also denotes the object location to
1359  * check
1360  * @return The last unlock operation
1361  */
1362 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1363 {
1364         void *location = curr->get_location();
1365
1366         action_list_t *list = obj_map.get(location);
1367         if (list == NULL)
1368                 return NULL;
1369
1370         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1371         sllnode<ModelAction*>* rit;
1372         for (rit = list->end();rit != NULL;rit=rit->getPrev())
1373                 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1374                         return rit->getVal();
1375         return NULL;
1376 }
1377
1378 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1379 {
1380         ModelAction *parent = get_last_action(tid);
1381         if (!parent)
1382                 parent = get_thread(tid)->get_creation();
1383         return parent;
1384 }
1385
1386 /**
1387  * Returns the clock vector for a given thread.
1388  * @param tid The thread whose clock vector we want
1389  * @return Desired clock vector
1390  */
1391 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1392 {
1393         ModelAction *firstaction=get_parent_action(tid);
1394         return firstaction != NULL ? firstaction->get_cv() : NULL;
1395 }
1396
1397 bool valequals(uint64_t val1, uint64_t val2, int size) {
1398         switch(size) {
1399         case 1:
1400                 return ((uint8_t)val1) == ((uint8_t)val2);
1401         case 2:
1402                 return ((uint16_t)val1) == ((uint16_t)val2);
1403         case 4:
1404                 return ((uint32_t)val1) == ((uint32_t)val2);
1405         case 8:
1406                 return val1==val2;
1407         default:
1408                 ASSERT(0);
1409                 return false;
1410         }
1411 }
1412
1413 /**
1414  * Build up an initial set of all past writes that this 'read' action may read
1415  * from, as well as any previously-observed future values that must still be valid.
1416  *
1417  * @param curr is the current ModelAction that we are exploring; it must be a
1418  * 'read' operation.
1419  */
1420 SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
1421 {
1422         SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1423         unsigned int i;
1424         ASSERT(curr->is_read());
1425
1426         ModelAction *last_sc_write = NULL;
1427
1428         if (curr->is_seqcst())
1429                 last_sc_write = get_last_seq_cst_write(curr);
1430
1431         SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1432
1433         /* Iterate over all threads */
1434         for (i = 0;i < thrd_lists->size();i++) {
1435                 /* Iterate over actions in thread, starting from most recent */
1436                 action_list_t *list = &(*thrd_lists)[i];
1437                 sllnode<ModelAction *> * rit;
1438                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1439                         ModelAction *act = rit->getVal();
1440
1441                         if (act == curr)
1442                                 continue;
1443
1444                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1445                         bool allow_read = true;
1446
1447                         if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1448                                 allow_read = false;
1449
1450                         /* Need to check whether we will have two RMW reading from the same value */
1451                         if (curr->is_rmwr()) {
1452                                 /* It is okay if we have a failing CAS */
1453                                 if (!curr->is_rmwrcas() ||
1454                                                 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1455                                         //Need to make sure we aren't the second RMW
1456                                         CycleNode * node = mo_graph->getNode_noCreate(act);
1457                                         if (node != NULL && node->getRMW() != NULL) {
1458                                                 //we are the second RMW
1459                                                 allow_read = false;
1460                                         }
1461                                 }
1462                         }
1463
1464                         if (allow_read) {
1465                                 /* Only add feasible reads */
1466                                 rf_set->push_back(act);
1467                         }
1468
1469                         /* Include at most one act per-thread that "happens before" curr */
1470                         if (act->happens_before(curr))
1471                                 break;
1472                 }
1473         }
1474
1475         if (DBG_ENABLED()) {
1476                 model_print("Reached read action:\n");
1477                 curr->print();
1478                 model_print("End printing read_from_past\n");
1479         }
1480         return rf_set;
1481 }
1482
1483 /**
1484  * @brief Get an action representing an uninitialized atomic
1485  *
1486  * This function may create a new one.
1487  *
1488  * @param curr The current action, which prompts the creation of an UNINIT action
1489  * @return A pointer to the UNINIT ModelAction
1490  */
1491 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1492 {
1493         ModelAction *act = curr->get_uninit_action();
1494         if (!act) {
1495                 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1496                 curr->set_uninit_action(act);
1497         }
1498         act->create_cv(NULL);
1499         return act;
1500 }
1501
1502 static void print_list(action_list_t *list)
1503 {
1504         sllnode<ModelAction*> *it;
1505
1506         model_print("------------------------------------------------------------------------------------\n");
1507         model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
1508         model_print("------------------------------------------------------------------------------------\n");
1509
1510         unsigned int hash = 0;
1511
1512         for (it = list->begin();it != NULL;it=it->getNext()) {
1513                 const ModelAction *act = it->getVal();
1514                 if (act->get_seq_number() > 0)
1515                         act->print();
1516                 hash = hash^(hash<<3)^(it->getVal()->hash());
1517         }
1518         model_print("HASH %u\n", hash);
1519         model_print("------------------------------------------------------------------------------------\n");
1520 }
1521
1522 #if SUPPORT_MOD_ORDER_DUMP
1523 void ModelExecution::dumpGraph(char *filename)
1524 {
1525         char buffer[200];
1526         sprintf(buffer, "%s.dot", filename);
1527         FILE *file = fopen(buffer, "w");
1528         fprintf(file, "digraph %s {\n", filename);
1529         mo_graph->dumpNodes(file);
1530         ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1531
1532         for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1533                 ModelAction *act = it->getVal();
1534                 if (act->is_read()) {
1535                         mo_graph->dot_print_node(file, act);
1536                         mo_graph->dot_print_edge(file,
1537                                                                                                                          act->get_reads_from(),
1538                                                                                                                          act,
1539                                                                                                                          "label=\"rf\", color=red, weight=2");
1540                 }
1541                 if (thread_array[act->get_tid()]) {
1542                         mo_graph->dot_print_edge(file,
1543                                                                                                                          thread_array[id_to_int(act->get_tid())],
1544                                                                                                                          act,
1545                                                                                                                          "label=\"sb\", color=blue, weight=400");
1546                 }
1547
1548                 thread_array[act->get_tid()] = act;
1549         }
1550         fprintf(file, "}\n");
1551         model_free(thread_array);
1552         fclose(file);
1553 }
1554 #endif
1555
1556 /** @brief Prints an execution trace summary. */
1557 void ModelExecution::print_summary()
1558 {
1559 #if SUPPORT_MOD_ORDER_DUMP
1560         char buffername[100];
1561         sprintf(buffername, "exec%04u", get_execution_number());
1562         mo_graph->dumpGraphToFile(buffername);
1563         sprintf(buffername, "graph%04u", get_execution_number());
1564         dumpGraph(buffername);
1565 #endif
1566
1567         model_print("Execution trace %d:", get_execution_number());
1568         if (scheduler->all_threads_sleeping())
1569                 model_print(" SLEEP-SET REDUNDANT");
1570         if (have_bug_reports())
1571                 model_print(" DETECTED BUG(S)");
1572
1573         model_print("\n");
1574
1575         print_list(&action_trace);
1576         model_print("\n");
1577
1578 }
1579
1580 /**
1581  * Add a Thread to the system for the first time. Should only be called once
1582  * per thread.
1583  * @param t The Thread to add
1584  */
1585 void ModelExecution::add_thread(Thread *t)
1586 {
1587         unsigned int i = id_to_int(t->get_id());
1588         if (i >= thread_map.size())
1589                 thread_map.resize(i + 1);
1590         thread_map[i] = t;
1591         if (!t->is_model_thread())
1592                 scheduler->add_thread(t);
1593 }
1594
1595 /**
1596  * @brief Get a Thread reference by its ID
1597  * @param tid The Thread's ID
1598  * @return A Thread reference
1599  */
1600 Thread * ModelExecution::get_thread(thread_id_t tid) const
1601 {
1602         unsigned int i = id_to_int(tid);
1603         if (i < thread_map.size())
1604                 return thread_map[i];
1605         return NULL;
1606 }
1607
1608 /**
1609  * @brief Get a reference to the Thread in which a ModelAction was executed
1610  * @param act The ModelAction
1611  * @return A Thread reference
1612  */
1613 Thread * ModelExecution::get_thread(const ModelAction *act) const
1614 {
1615         return get_thread(act->get_tid());
1616 }
1617
1618 /**
1619  * @brief Get a Thread reference by its pthread ID
1620  * @param index The pthread's ID
1621  * @return A Thread reference
1622  */
1623 Thread * ModelExecution::get_pthread(pthread_t pid) {
1624         union {
1625                 pthread_t p;
1626                 uint32_t v;
1627         } x;
1628         x.p = pid;
1629         uint32_t thread_id = x.v;
1630         if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1631         else return NULL;
1632 }
1633
1634 /**
1635  * @brief Check if a Thread is currently enabled
1636  * @param t The Thread to check
1637  * @return True if the Thread is currently enabled
1638  */
1639 bool ModelExecution::is_enabled(Thread *t) const
1640 {
1641         return scheduler->is_enabled(t);
1642 }
1643
1644 /**
1645  * @brief Check if a Thread is currently enabled
1646  * @param tid The ID of the Thread to check
1647  * @return True if the Thread is currently enabled
1648  */
1649 bool ModelExecution::is_enabled(thread_id_t tid) const
1650 {
1651         return scheduler->is_enabled(tid);
1652 }
1653
1654 /**
1655  * @brief Select the next thread to execute based on the curren action
1656  *
1657  * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1658  * actions should be followed by the execution of their child thread. In either
1659  * case, the current action should determine the next thread schedule.
1660  *
1661  * @param curr The current action
1662  * @return The next thread to run, if the current action will determine this
1663  * selection; otherwise NULL
1664  */
1665 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1666 {
1667         /* Do not split atomic RMW */
1668         if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1669                 return get_thread(curr);
1670         /* Follow CREATE with the created thread */
1671         /* which is not needed, because model.cc takes care of this */
1672         if (curr->get_type() == THREAD_CREATE)
1673                 return curr->get_thread_operand();
1674         if (curr->get_type() == PTHREAD_CREATE) {
1675                 return curr->get_thread_operand();
1676         }
1677         return NULL;
1678 }
1679
1680 /** @param act A read atomic action */
1681 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1682 {
1683         ASSERT(act->is_read());
1684
1685         // Actions paused by fuzzer have their sequence number reset to 0
1686         return act->get_seq_number() == 0;
1687 }
1688
1689 /**
1690  * Takes the next step in the execution, if possible.
1691  * @param curr The current step to take
1692  * @return Returns the next Thread to run, if any; NULL if this execution
1693  * should terminate
1694  */
1695 Thread * ModelExecution::take_step(ModelAction *curr)
1696 {
1697         Thread *curr_thrd = get_thread(curr);
1698         ASSERT(curr_thrd->get_state() == THREAD_READY);
1699
1700         ASSERT(check_action_enabled(curr));     /* May have side effects? */
1701         curr = check_current_action(curr);
1702         ASSERT(curr);
1703
1704         /* Process this action in ModelHistory for records */
1705         model->get_history()->process_action( curr, curr->get_tid() );
1706
1707         if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1708                 scheduler->remove_thread(curr_thrd);
1709
1710         return action_select_next_thread(curr);
1711 }
1712
1713 Fuzzer * ModelExecution::getFuzzer() {
1714         return fuzzer;
1715 }