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