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