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