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         isfinished(false)
  71 {
  72         /* Initialize a model-checker thread, for special ModelActions */
  73         model_thread = new Thread(get_next_id());
  74         add_thread(model_thread);
  75         scheduler->register_engine(this);
  76 }
  77
  78 /** @brief Destructor */
  79 ModelExecution::~ModelExecution()
  80 {
  81         for (unsigned int i = 0;i < get_num_threads();i++)
  82                 delete get_thread(int_to_id(i));
  83
  84         delete mo_graph;
  85         delete priv;
  86 }
  87
  88 int ModelExecution::get_execution_number() const
  89 {
  90         return model->get_execution_number();
  91 }
  92
  93 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
  94 {
  95         action_list_t *tmp = hash->get(ptr);
  96         if (tmp == NULL) {
  97                 tmp = new action_list_t();
  98                 hash->put(ptr, tmp);
  99         }
 100         return tmp;
 101 }
 102
 103 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
 104 {
 105         SnapVector<action_list_t> *tmp = hash->get(ptr);
 106         if (tmp == NULL) {
 107                 tmp = new SnapVector<action_list_t>();
 108                 hash->put(ptr, tmp);
 109         }
 110         return tmp;
 111 }
 112
 113 /** @return a thread ID for a new Thread */
 114 thread_id_t ModelExecution::get_next_id()
 115 {
 116         return priv->next_thread_id++;
 117 }
 118
 119 /** @return the number of user threads created during this execution */
 120 unsigned int ModelExecution::get_num_threads() const
 121 {
 122         return priv->next_thread_id;
 123 }
 124
 125 /** @return a sequence number for a new ModelAction */
 126 modelclock_t ModelExecution::get_next_seq_num()
 127 {
 128         return ++priv->used_sequence_numbers;
 129 }
 130
 131 /**
 132  * @brief Should the current action wake up a given thread?
 133  *
 134  * @param curr The current action
 135  * @param thread The thread that we might wake up
 136  * @return True, if we should wake up the sleeping thread; false otherwise
 137  */
 138 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
 139 {
 140         const ModelAction *asleep = thread->get_pending();
 141         /* Don't allow partial RMW to wake anyone up */
 142         if (curr->is_rmwr())
 143                 return false;
 144         /* Synchronizing actions may have been backtracked */
 145         if (asleep->could_synchronize_with(curr))
 146                 return true;
 147         /* All acquire/release fences and fence-acquire/store-release */
 148         if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
 149                 return true;
 150         /* Fence-release + store can awake load-acquire on the same location */
 151         if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
 152                 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
 153                 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
 154                         return true;
 155         }
 156         return false;
 157 }
 158
 159 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 160 {
 161         for (unsigned int i = 0;i < get_num_threads();i++) {
 162                 Thread *thr = get_thread(int_to_id(i));
 163                 if (scheduler->is_sleep_set(thr)) {
 164                         if (should_wake_up(curr, thr))
 165                                 /* Remove this thread from sleep set */
 166                                 scheduler->remove_sleep(thr);
 167                 }
 168         }
 169 }
 170
 171 /** @brief Alert the model-checker that an incorrectly-ordered
 172  * synchronization was made */
 173 void ModelExecution::set_bad_synchronization()
 174 {
 175         priv->bad_synchronization = true;
 176 }
 177
 178 bool ModelExecution::assert_bug(const char *msg)
 179 {
 180         priv->bugs.push_back(new bug_message(msg));
 181
 182         if (isfeasibleprefix()) {
 183                 set_assert();
 184                 return true;
 185         }
 186         return false;
 187 }
 188
 189 /** @return True, if any bugs have been reported for this execution */
 190 bool ModelExecution::have_bug_reports() const
 191 {
 192         return priv->bugs.size() != 0;
 193 }
 194
 195 /** @return True, if any fatal bugs have been reported for this execution.
 196  *  Any bug other than a data race is considered a fatal bug. Data races
 197  *  are not considered fatal unless the number of races is exceeds
 198  *  a threshold (temporarily set as 15).
 199  */
 200 bool ModelExecution::have_fatal_bug_reports() const
 201 {
 202         return priv->bugs.size() != 0;
 203 }
 204
 205 SnapVector<bug_message *> * ModelExecution::get_bugs() const
 206 {
 207         return &priv->bugs;
 208 }
 209
 210 /**
 211  * Check whether the current trace has triggered an assertion which should halt
 212  * its execution.
 213  *
 214  * @return True, if the execution should be aborted; false otherwise
 215  */
 216 bool ModelExecution::has_asserted() const
 217 {
 218         return priv->asserted;
 219 }
 220
 221 /**
 222  * Trigger a trace assertion which should cause this execution to be halted.
 223  * This can be due to a detected bug or due to an infeasibility that should
 224  * halt ASAP.
 225  */
 226 void ModelExecution::set_assert()
 227 {
 228         priv->asserted = true;
 229 }
 230
 231 /**
 232  * Check if we are in a deadlock. Should only be called at the end of an
 233  * execution, although it should not give false positives in the middle of an
 234  * execution (there should be some ENABLED thread).
 235  *
 236  * @return True if program is in a deadlock; false otherwise
 237  */
 238 bool ModelExecution::is_deadlocked() const
 239 {
 240         bool blocking_threads = false;
 241         for (unsigned int i = 0;i < get_num_threads();i++) {
 242                 thread_id_t tid = int_to_id(i);
 243                 if (is_enabled(tid))
 244                         return false;
 245                 Thread *t = get_thread(tid);
 246                 if (!t->is_model_thread() && t->get_pending())
 247                         blocking_threads = true;
 248         }
 249         return blocking_threads;
 250 }
 251
 252 /**
 253  * Check if this is a complete execution. That is, have all thread completed
 254  * execution (rather than exiting because sleep sets have forced a redundant
 255  * execution).
 256  *
 257  * @return True if the execution is complete.
 258  */
 259 bool ModelExecution::is_complete_execution() const
 260 {
 261         for (unsigned int i = 0;i < get_num_threads();i++)
 262                 if (is_enabled(int_to_id(i)))
 263                         return false;
 264         return true;
 265 }
 266
 267 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
 268         uint64_t value = *((const uint64_t *) location);
 269         modelclock_t storeclock;
 270         thread_id_t storethread;
 271         getStoreThreadAndClock(location, &storethread, &storeclock);
 272         setAtomicStoreFlag(location);
 273         ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
 274         act->set_seq_number(storeclock);
 275         add_normal_write_to_lists(act);
 276         add_write_to_lists(act);
 277         w_modification_order(act);
 278         return act;
 279 }
 280
 281 /**
 282  * Processes a read model action.
 283  * @param curr is the read model action to process.
 284  * @param rf_set is the set of model actions we can possibly read from
 285  * @return True if processing this read updates the mo_graph.
 286  */
 287 void ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 288 {
 289         SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
 290         bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
 291         if (hasnonatomicstore) {
 292                 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
 293                 rf_set->push_back(nonatomicstore);
 294         }
 295
 296         while(true) {
 297                 int index = fuzzer->selectWrite(curr, rf_set);
 298                 ModelAction *rf = (*rf_set)[index];
 299
 300
 301                 ASSERT(rf);
 302                 bool canprune = false;
 303                 if (r_modification_order(curr, rf, priorset, &canprune)) {
 304                         for(unsigned int i=0;i<priorset->size();i++) {
 305                                 mo_graph->addEdge((*priorset)[i], rf);
 306                         }
 307                         read_from(curr, rf);
 308                         get_thread(curr)->set_return_value(curr->get_return_value());
 309                         delete priorset;
 310                         if (canprune && curr->get_type() == ATOMIC_READ) {
 311                                 int tid = id_to_int(curr->get_tid());
 312                                 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
 313                         }
 314                         return;
 315                 }
 316                 priorset->clear();
 317                 (*rf_set)[index] = rf_set->back();
 318                 rf_set->pop_back();
 319         }
 320 }
 321
 322 /**
 323  * Processes a lock, trylock, or unlock model action.  @param curr is
 324  * the read model action to process.
 325  *
 326  * The try lock operation checks whether the lock is taken.  If not,
 327  * it falls to the normal lock operation case.  If so, it returns
 328  * fail.
 329  *
 330  * The lock operation has already been checked that it is enabled, so
 331  * it just grabs the lock and synchronizes with the previous unlock.
 332  *
 333  * The unlock operation has to re-enable all of the threads that are
 334  * waiting on the lock.
 335  *
 336  * @return True if synchronization was updated; false otherwise
 337  */
 338 bool ModelExecution::process_mutex(ModelAction *curr)
 339 {
 340         cdsc::mutex *mutex = curr->get_mutex();
 341         struct cdsc::mutex_state *state = NULL;
 342
 343         if (mutex)
 344                 state = mutex->get_state();
 345
 346         switch (curr->get_type()) {
 347         case ATOMIC_TRYLOCK: {
 348                 bool success = !state->locked;
 349                 curr->set_try_lock(success);
 350                 if (!success) {
 351                         get_thread(curr)->set_return_value(0);
 352                         break;
 353                 }
 354                 get_thread(curr)->set_return_value(1);
 355         }
 356         //otherwise fall into the lock case
 357         case ATOMIC_LOCK: {
 358                 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
 359                 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
 360                 //      assert_bug("Lock access before initialization");
 361                 state->locked = get_thread(curr);
 362                 ModelAction *unlock = get_last_unlock(curr);
 363                 //synchronize with the previous unlock statement
 364                 if (unlock != NULL) {
 365                         synchronize(unlock, curr);
 366                         return true;
 367                 }
 368                 break;
 369         }
 370         case ATOMIC_WAIT:
 371         case ATOMIC_UNLOCK: {
 372                 //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...
 373
 374                 /* wake up the other threads */
 375                 for (unsigned int i = 0;i < get_num_threads();i++) {
 376                         Thread *t = get_thread(int_to_id(i));
 377                         Thread *curr_thrd = get_thread(curr);
 378                         if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
 379                                 scheduler->wake(t);
 380                 }
 381
 382                 /* unlock the lock - after checking who was waiting on it */
 383                 state->locked = NULL;
 384
 385                 if (!curr->is_wait())
 386                         break;/* The rest is only for ATOMIC_WAIT */
 387
 388                 break;
 389         }
 390         case ATOMIC_NOTIFY_ALL: {
 391                 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
 392                 //activate all the waiting threads
 393                 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
 394                         scheduler->wake(get_thread(rit->getVal()));
 395                 }
 396                 waiters->clear();
 397                 break;
 398         }
 399         case ATOMIC_NOTIFY_ONE: {
 400                 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
 401                 if (waiters->size() != 0) {
 402                         Thread * thread = fuzzer->selectNotify(waiters);
 403                         scheduler->wake(thread);
 404                 }
 405                 break;
 406         }
 407
 408         default:
 409                 ASSERT(0);
 410         }
 411         return false;
 412 }
 413
 414 /**
 415  * Process a write ModelAction
 416  * @param curr The ModelAction to process
 417  * @return True if the mo_graph was updated or promises were resolved
 418  */
 419 void ModelExecution::process_write(ModelAction *curr)
 420 {
 421         w_modification_order(curr);
 422         get_thread(curr)->set_return_value(VALUE_NONE);
 423 }
 424
 425 /**
 426  * Process a fence ModelAction
 427  * @param curr The ModelAction to process
 428  * @return True if synchronization was updated
 429  */
 430 bool ModelExecution::process_fence(ModelAction *curr)
 431 {
 432         /*
 433          * fence-relaxed: no-op
 434          * fence-release: only log the occurence (not in this function), for
 435          *   use in later synchronization
 436          * fence-acquire (this function): search for hypothetical release
 437          *   sequences
 438          * fence-seq-cst: MO constraints formed in {r,w}_modification_order
 439          */
 440         bool updated = false;
 441         if (curr->is_acquire()) {
 442                 action_list_t *list = &action_trace;
 443                 sllnode<ModelAction *> * rit;
 444                 /* Find X : is_read(X) && X --sb-> curr */
 445                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
 446                         ModelAction *act = rit->getVal();
 447                         if (act == curr)
 448                                 continue;
 449                         if (act->get_tid() != curr->get_tid())
 450                                 continue;
 451                         /* Stop at the beginning of the thread */
 452                         if (act->is_thread_start())
 453                                 break;
 454                         /* Stop once we reach a prior fence-acquire */
 455                         if (act->is_fence() && act->is_acquire())
 456                                 break;
 457                         if (!act->is_read())
 458                                 continue;
 459                         /* read-acquire will find its own release sequences */
 460                         if (act->is_acquire())
 461                                 continue;
 462
 463                         /* Establish hypothetical release sequences */
 464                         ClockVector *cv = get_hb_from_write(act->get_reads_from());
 465                         if (cv != NULL && curr->get_cv()->merge(cv))
 466                                 updated = true;
 467                 }
 468         }
 469         return updated;
 470 }
 471
 472 /**
 473  * @brief Process the current action for thread-related activity
 474  *
 475  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
 476  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
 477  * synchronization, etc.  This function is a no-op for non-THREAD actions
 478  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
 479  *
 480  * @param curr The current action
 481  * @return True if synchronization was updated or a thread completed
 482  */
 483 void ModelExecution::process_thread_action(ModelAction *curr)
 484 {
 485         switch (curr->get_type()) {
 486         case THREAD_CREATE: {
 487                 thrd_t *thrd = (thrd_t *)curr->get_location();
 488                 struct thread_params *params = (struct thread_params *)curr->get_value();
 489                 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
 490                 curr->set_thread_operand(th);
 491                 add_thread(th);
 492                 th->set_creation(curr);
 493                 break;
 494         }
 495         case PTHREAD_CREATE: {
 496                 (*(uint32_t *)curr->get_location()) = pthread_counter++;
 497
 498                 struct pthread_params *params = (struct pthread_params *)curr->get_value();
 499                 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
 500                 curr->set_thread_operand(th);
 501                 add_thread(th);
 502                 th->set_creation(curr);
 503
 504                 if ( pthread_map.size() < pthread_counter )
 505                         pthread_map.resize( pthread_counter );
 506                 pthread_map[ pthread_counter-1 ] = th;
 507
 508                 break;
 509         }
 510         case THREAD_JOIN: {
 511                 Thread *blocking = curr->get_thread_operand();
 512                 ModelAction *act = get_last_action(blocking->get_id());
 513                 synchronize(act, curr);
 514                 break;
 515         }
 516         case PTHREAD_JOIN: {
 517                 Thread *blocking = curr->get_thread_operand();
 518                 ModelAction *act = get_last_action(blocking->get_id());
 519                 synchronize(act, curr);
 520                 break;  // WL: to be add (modified)
 521         }
 522
 523         case THREADONLY_FINISH:
 524         case THREAD_FINISH: {
 525                 Thread *th = get_thread(curr);
 526                 if (curr->get_type() == THREAD_FINISH &&
 527                                 th == model->getInitThread()) {
 528                         th->complete();
 529                         setFinished();
 530                         break;
 531                 }
 532
 533                 /* Wake up any joining threads */
 534                 for (unsigned int i = 0;i < get_num_threads();i++) {
 535                         Thread *waiting = get_thread(int_to_id(i));
 536                         if (waiting->waiting_on() == th &&
 537                                         waiting->get_pending()->is_thread_join())
 538                                 scheduler->wake(waiting);
 539                 }
 540                 th->complete();
 541                 break;
 542         }
 543         case THREAD_START: {
 544                 break;
 545         }
 546         default:
 547                 break;
 548         }
 549 }
 550
 551 /**
 552  * Initialize the current action by performing one or more of the following
 553  * actions, as appropriate: merging RMWR and RMWC/RMW actions,
 554  * manipulating backtracking sets, allocating and
 555  * initializing clock vectors, and computing the promises to fulfill.
 556  *
 557  * @param curr The current action, as passed from the user context; may be
 558  * freed/invalidated after the execution of this function, with a different
 559  * action "returned" its place (pass-by-reference)
 560  * @return True if curr is a newly-explored action; false otherwise
 561  */
 562 bool ModelExecution::initialize_curr_action(ModelAction **curr)
 563 {
 564         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
 565                 ModelAction *newcurr = process_rmw(*curr);
 566                 delete *curr;
 567
 568                 *curr = newcurr;
 569                 return false;
 570         } else {
 571                 ModelAction *newcurr = *curr;
 572
 573                 newcurr->set_seq_number(get_next_seq_num());
 574                 /* Always compute new clock vector */
 575                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 576
 577                 /* Assign most recent release fence */
 578                 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
 579
 580                 return true;    /* This was a new ModelAction */
 581         }
 582 }
 583
 584 /**
 585  * @brief Establish reads-from relation between two actions
 586  *
 587  * Perform basic operations involved with establishing a concrete rf relation,
 588  * including setting the ModelAction data and checking for release sequences.
 589  *
 590  * @param act The action that is reading (must be a read)
 591  * @param rf The action from which we are reading (must be a write)
 592  *
 593  * @return True if this read established synchronization
 594  */
 595
 596 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
 597 {
 598         ASSERT(rf);
 599         ASSERT(rf->is_write());
 600
 601         act->set_read_from(rf);
 602         if (act->is_acquire()) {
 603                 ClockVector *cv = get_hb_from_write(rf);
 604                 if (cv == NULL)
 605                         return;
 606                 act->get_cv()->merge(cv);
 607         }
 608 }
 609
 610 /**
 611  * @brief Synchronizes two actions
 612  *
 613  * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
 614  * This function performs the synchronization as well as providing other hooks
 615  * for other checks along with synchronization.
 616  *
 617  * @param first The left-hand side of the synchronizes-with relation
 618  * @param second The right-hand side of the synchronizes-with relation
 619  * @return True if the synchronization was successful (i.e., was consistent
 620  * with the execution order); false otherwise
 621  */
 622 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
 623 {
 624         if (*second < *first) {
 625                 set_bad_synchronization();
 626                 return false;
 627         }
 628         return second->synchronize_with(first);
 629 }
 630
 631 /**
 632  * @brief Check whether a model action is enabled.
 633  *
 634  * Checks whether an operation would be successful (i.e., is a lock already
 635  * locked, or is the joined thread already complete).
 636  *
 637  * For yield-blocking, yields are never enabled.
 638  *
 639  * @param curr is the ModelAction to check whether it is enabled.
 640  * @return a bool that indicates whether the action is enabled.
 641  */
 642 bool ModelExecution::check_action_enabled(ModelAction *curr) {
 643         if (curr->is_lock()) {
 644                 cdsc::mutex *lock = curr->get_mutex();
 645                 struct cdsc::mutex_state *state = lock->get_state();
 646                 if (state->locked)
 647                         return false;
 648         } else if (curr->is_thread_join()) {
 649                 Thread *blocking = curr->get_thread_operand();
 650                 if (!blocking->is_complete()) {
 651                         return false;
 652                 }
 653         }
 654
 655         return true;
 656 }
 657
 658 /**
 659  * This is the heart of the model checker routine. It performs model-checking
 660  * actions corresponding to a given "current action." Among other processes, it
 661  * calculates reads-from relationships, updates synchronization clock vectors,
 662  * forms a memory_order constraints graph, and handles replay/backtrack
 663  * execution when running permutations of previously-observed executions.
 664  *
 665  * @param curr The current action to process
 666  * @return The ModelAction that is actually executed; may be different than
 667  * curr
 668  */
 669 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 670 {
 671         ASSERT(curr);
 672         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
 673         bool newly_explored = initialize_curr_action(&curr);
 674
 675         DBG();
 676
 677         wake_up_sleeping_actions(curr);
 678
 679         /* Add the action to lists before any other model-checking tasks */
 680         if (!second_part_of_rmw && curr->get_type() != NOOP)
 681                 add_action_to_lists(curr);
 682
 683         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 }