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