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