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