execution.cc

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