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