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