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