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