execution.cc

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