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                 action_list_t::reverse_iterator rit;
 444                 /* Find X : is_read(X) && X --sb-> curr */
 445                 for (rit = list->rbegin();rit != list->rend();rit++) {
 446                         ModelAction *act = *rit;
 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                 action_list_t::reverse_iterator rit;
 808                 for (rit = list->rbegin();rit != list->rend();rit++) {
 809                         ModelAction *act = *rit;
 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                 action_list_t::reverse_iterator rit;
 940                 for (rit = list->rbegin();rit != list->rend();rit++) {
 941                         ModelAction *act = *rit;
 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                 action_list_t::reverse_iterator rit;
1014                 for (rit = list->rbegin();rit != list->rend();rit++) {
1015                         ModelAction *act = *rit;
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                 (*vec)[uninit_id].push_front(uninit);
1111         }
1112         list->push_back(act);
1113
1114         // Update action trace, a total order of all actions
1115         action_trace.push_back(act);
1116         if (uninit)
1117                 action_trace.push_front(uninit);
1118
1119         // Update obj_thrd_map, a per location, per thread, order of actions
1120         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1121         if (tid >= (int)vec->size()) {
1122           uint oldsize =vec->size();
1123           vec->resize(priv->next_thread_id);
1124           for(uint i=oldsize; i<priv->next_thread_id; i++)
1125             new (&vec[i]) action_list_t();
1126         }
1127         (*vec)[tid].push_back(act);
1128         if (uninit)
1129                 (*vec)[uninit_id].push_front(uninit);
1130
1131         // Update thrd_last_action, the last action taken by each thrad
1132         if ((int)thrd_last_action.size() <= tid)
1133                 thrd_last_action.resize(get_num_threads());
1134         thrd_last_action[tid] = act;
1135         if (uninit)
1136                 thrd_last_action[uninit_id] = uninit;
1137
1138         // Update thrd_last_fence_release, the last release fence taken by each thread
1139         if (act->is_fence() && act->is_release()) {
1140                 if ((int)thrd_last_fence_release.size() <= tid)
1141                         thrd_last_fence_release.resize(get_num_threads());
1142                 thrd_last_fence_release[tid] = act;
1143         }
1144
1145         if (act->is_wait()) {
1146                 void *mutex_loc = (void *) act->get_value();
1147                 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1148
1149                 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1150                 if (tid >= (int)vec->size()) {
1151                   uint oldsize = vec->size();
1152                   vec->resize(priv->next_thread_id);
1153                   for(uint i=oldsize; i<priv->next_thread_id; i++)
1154                     new (&vec[i]) action_list_t();
1155                 }
1156                 (*vec)[tid].push_back(act);
1157         }
1158 }
1159
1160 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1161         action_list_t::reverse_iterator rit = list->rbegin();
1162         modelclock_t next_seq = act->get_seq_number();
1163         if (rit == list->rend() || (*rit)->get_seq_number() == next_seq)
1164                 list->push_back(act);
1165         else {
1166                 for(;rit != list->rend();rit++) {
1167                         if ((*rit)->get_seq_number() == next_seq) {
1168                                 action_list_t::iterator it = rit.base();
1169                                 list->insert(it, act);
1170                                 break;
1171                         }
1172                 }
1173         }
1174 }
1175
1176 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1177         action_list_t::reverse_iterator rit = list->rbegin();
1178         modelclock_t next_seq = act->get_seq_number();
1179         if (rit == list->rend()) {
1180                 act->create_cv(NULL);
1181         } else if ((*rit)->get_seq_number() == next_seq) {
1182                 act->create_cv((*rit));
1183                 list->push_back(act);
1184         } else {
1185                 for(;rit != list->rend();rit++) {
1186                         if ((*rit)->get_seq_number() == next_seq) {
1187                                 act->create_cv((*rit));
1188                                 action_list_t::iterator it = rit.base();
1189                                 list->insert(it, act);
1190                                 break;
1191                         }
1192                 }
1193         }
1194 }
1195
1196 /**
1197  * Performs various bookkeeping operations for a normal write.  The
1198  * complication is that we are typically inserting a normal write
1199  * lazily, so we need to insert it into the middle of lists.
1200  *
1201  * @param act is the ModelAction to add.
1202  */
1203
1204 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1205 {
1206         int tid = id_to_int(act->get_tid());
1207         insertIntoActionListAndSetCV(&action_trace, act);
1208
1209         action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1210         insertIntoActionList(list, act);
1211
1212         // Update obj_thrd_map, a per location, per thread, order of actions
1213         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1214         if (tid >= (int)vec->size()) {
1215           uint oldsize =vec->size();
1216           vec->resize(priv->next_thread_id);
1217           for(uint i=oldsize; i<priv->next_thread_id; i++)
1218             new (&vec[i]) action_list_t();
1219         }
1220         insertIntoActionList(&(*vec)[tid],act);
1221
1222         // Update thrd_last_action, the last action taken by each thrad
1223         if (thrd_last_action[tid]->get_seq_number() == act->get_seq_number())
1224                 thrd_last_action[tid] = act;
1225 }
1226
1227
1228 void ModelExecution::add_write_to_lists(ModelAction *write) {
1229         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1230         int tid = id_to_int(write->get_tid());
1231         if (tid >= (int)vec->size()) {
1232           uint oldsize =vec->size();
1233           vec->resize(priv->next_thread_id);
1234           for(uint i=oldsize; i<priv->next_thread_id; i++)
1235             new (&vec[i]) action_list_t();
1236         }
1237         (*vec)[tid].push_back(write);
1238 }
1239
1240 /**
1241  * @brief Get the last action performed by a particular Thread
1242  * @param tid The thread ID of the Thread in question
1243  * @return The last action in the thread
1244  */
1245 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1246 {
1247         int threadid = id_to_int(tid);
1248         if (threadid < (int)thrd_last_action.size())
1249                 return thrd_last_action[id_to_int(tid)];
1250         else
1251                 return NULL;
1252 }
1253
1254 /**
1255  * @brief Get the last fence release performed by a particular Thread
1256  * @param tid The thread ID of the Thread in question
1257  * @return The last fence release in the thread, if one exists; NULL otherwise
1258  */
1259 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1260 {
1261         int threadid = id_to_int(tid);
1262         if (threadid < (int)thrd_last_fence_release.size())
1263                 return thrd_last_fence_release[id_to_int(tid)];
1264         else
1265                 return NULL;
1266 }
1267
1268 /**
1269  * Gets the last memory_order_seq_cst write (in the total global sequence)
1270  * performed on a particular object (i.e., memory location), not including the
1271  * current action.
1272  * @param curr The current ModelAction; also denotes the object location to
1273  * check
1274  * @return The last seq_cst write
1275  */
1276 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1277 {
1278         void *location = curr->get_location();
1279         return obj_last_sc_map.get(location);
1280 }
1281
1282 /**
1283  * Gets the last memory_order_seq_cst fence (in the total global sequence)
1284  * performed in a particular thread, prior to a particular fence.
1285  * @param tid The ID of the thread to check
1286  * @param before_fence The fence from which to begin the search; if NULL, then
1287  * search for the most recent fence in the thread.
1288  * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1289  */
1290 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1291 {
1292         /* All fences should have location FENCE_LOCATION */
1293         action_list_t *list = obj_map.get(FENCE_LOCATION);
1294
1295         if (!list)
1296                 return NULL;
1297
1298         action_list_t::reverse_iterator rit = list->rbegin();
1299
1300         if (before_fence) {
1301                 for (;rit != list->rend();rit++)
1302                         if (*rit == before_fence)
1303                                 break;
1304
1305                 ASSERT(*rit == before_fence);
1306                 rit++;
1307         }
1308
1309         for (;rit != list->rend();rit++)
1310                 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
1311                         return *rit;
1312         return NULL;
1313 }
1314
1315 /**
1316  * Gets the last unlock operation performed on a particular mutex (i.e., memory
1317  * location). This function identifies the mutex according to the current
1318  * action, which is presumed to perform on the same mutex.
1319  * @param curr The current ModelAction; also denotes the object location to
1320  * check
1321  * @return The last unlock operation
1322  */
1323 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1324 {
1325         void *location = curr->get_location();
1326
1327         action_list_t *list = obj_map.get(location);
1328         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1329         action_list_t::reverse_iterator rit;
1330         for (rit = list->rbegin();rit != list->rend();rit++)
1331                 if ((*rit)->is_unlock() || (*rit)->is_wait())
1332                         return *rit;
1333         return NULL;
1334 }
1335
1336 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1337 {
1338         ModelAction *parent = get_last_action(tid);
1339         if (!parent)
1340                 parent = get_thread(tid)->get_creation();
1341         return parent;
1342 }
1343
1344 /**
1345  * Returns the clock vector for a given thread.
1346  * @param tid The thread whose clock vector we want
1347  * @return Desired clock vector
1348  */
1349 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1350 {
1351         ModelAction *firstaction=get_parent_action(tid);
1352         return firstaction != NULL ? firstaction->get_cv() : NULL;
1353 }
1354
1355 bool valequals(uint64_t val1, uint64_t val2, int size) {
1356         switch(size) {
1357         case 1:
1358                 return ((uint8_t)val1) == ((uint8_t)val2);
1359         case 2:
1360                 return ((uint16_t)val1) == ((uint16_t)val2);
1361         case 4:
1362                 return ((uint32_t)val1) == ((uint32_t)val2);
1363         case 8:
1364                 return val1==val2;
1365         default:
1366                 ASSERT(0);
1367                 return false;
1368         }
1369 }
1370
1371 /**
1372  * Build up an initial set of all past writes that this 'read' action may read
1373  * from, as well as any previously-observed future values that must still be valid.
1374  *
1375  * @param curr is the current ModelAction that we are exploring; it must be a
1376  * 'read' operation.
1377  */
1378 SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
1379 {
1380         SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1381         unsigned int i;
1382         ASSERT(curr->is_read());
1383
1384         ModelAction *last_sc_write = NULL;
1385
1386         if (curr->is_seqcst())
1387                 last_sc_write = get_last_seq_cst_write(curr);
1388
1389         SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1390
1391         /* Iterate over all threads */
1392         for (i = 0;i < thrd_lists->size();i++) {
1393                 /* Iterate over actions in thread, starting from most recent */
1394                 action_list_t *list = &(*thrd_lists)[i];
1395                 action_list_t::reverse_iterator rit;
1396                 for (rit = list->rbegin();rit != list->rend();rit++) {
1397                         ModelAction *act = *rit;
1398
1399                         if (act == curr)
1400                                 continue;
1401
1402                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
1403                         bool allow_read = true;
1404
1405                         if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
1406                                 allow_read = false;
1407
1408                         /* Need to check whether we will have two RMW reading from the same value */
1409                         if (curr->is_rmwr()) {
1410                                 /* It is okay if we have a failing CAS */
1411                                 if (!curr->is_rmwrcas() ||
1412                                                 valequals(curr->get_value(), act->get_value(), curr->getSize())) {
1413                                         //Need to make sure we aren't the second RMW
1414                                         CycleNode * node = mo_graph->getNode_noCreate(act);
1415                                         if (node != NULL && node->getRMW() != NULL) {
1416                                                 //we are the second RMW
1417                                                 allow_read = false;
1418                                         }
1419                                 }
1420                         }
1421
1422                         if (allow_read) {
1423                                 /* Only add feasible reads */
1424                                 rf_set->push_back(act);
1425                         }
1426
1427                         /* Include at most one act per-thread that "happens before" curr */
1428                         if (act->happens_before(curr))
1429                                 break;
1430                 }
1431         }
1432
1433         if (DBG_ENABLED()) {
1434                 model_print("Reached read action:\n");
1435                 curr->print();
1436                 model_print("End printing read_from_past\n");
1437         }
1438         return rf_set;
1439 }
1440
1441 /**
1442  * @brief Get an action representing an uninitialized atomic
1443  *
1444  * This function may create a new one.
1445  *
1446  * @param curr The current action, which prompts the creation of an UNINIT action
1447  * @return A pointer to the UNINIT ModelAction
1448  */
1449 ModelAction * ModelExecution::get_uninitialized_action(ModelAction *curr) const
1450 {
1451         ModelAction *act = curr->get_uninit_action();
1452         if (!act) {
1453                 act = new ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, curr->get_location(), params->uninitvalue, model_thread);
1454                 curr->set_uninit_action(act);
1455         }
1456         act->create_cv(NULL);
1457         return act;
1458 }
1459
1460 static void print_list(const action_list_t *list)
1461 {
1462         action_list_t::const_iterator it;
1463
1464         model_print("------------------------------------------------------------------------------------\n");
1465         model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
1466         model_print("------------------------------------------------------------------------------------\n");
1467
1468         unsigned int hash = 0;
1469
1470         for (it = list->begin();it != list->end();it++) {
1471                 const ModelAction *act = *it;
1472                 if (act->get_seq_number() > 0)
1473                         act->print();
1474                 hash = hash^(hash<<3)^((*it)->hash());
1475         }
1476         model_print("HASH %u\n", hash);
1477         model_print("------------------------------------------------------------------------------------\n");
1478 }
1479
1480 #if SUPPORT_MOD_ORDER_DUMP
1481 void ModelExecution::dumpGraph(char *filename) const
1482 {
1483         char buffer[200];
1484         sprintf(buffer, "%s.dot", filename);
1485         FILE *file = fopen(buffer, "w");
1486         fprintf(file, "digraph %s {\n", filename);
1487         mo_graph->dumpNodes(file);
1488         ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1489
1490         for (action_list_t::const_iterator it = action_trace.begin();it != action_trace.end();it++) {
1491                 ModelAction *act = *it;
1492                 if (act->is_read()) {
1493                         mo_graph->dot_print_node(file, act);
1494                         mo_graph->dot_print_edge(file,
1495                                                                                                                          act->get_reads_from(),
1496                                                                                                                          act,
1497                                                                                                                          "label=\"rf\", color=red, weight=2");
1498                 }
1499                 if (thread_array[act->get_tid()]) {
1500                         mo_graph->dot_print_edge(file,
1501                                                                                                                          thread_array[id_to_int(act->get_tid())],
1502                                                                                                                          act,
1503                                                                                                                          "label=\"sb\", color=blue, weight=400");
1504                 }
1505
1506                 thread_array[act->get_tid()] = act;
1507         }
1508         fprintf(file, "}\n");
1509         model_free(thread_array);
1510         fclose(file);
1511 }
1512 #endif
1513
1514 /** @brief Prints an execution trace summary. */
1515 void ModelExecution::print_summary() const
1516 {
1517 #if SUPPORT_MOD_ORDER_DUMP
1518         char buffername[100];
1519         sprintf(buffername, "exec%04u", get_execution_number());
1520         mo_graph->dumpGraphToFile(buffername);
1521         sprintf(buffername, "graph%04u", get_execution_number());
1522         dumpGraph(buffername);
1523 #endif
1524
1525         model_print("Execution trace %d:", get_execution_number());
1526         if (isfeasibleprefix()) {
1527                 if (scheduler->all_threads_sleeping())
1528                         model_print(" SLEEP-SET REDUNDANT");
1529                 if (have_bug_reports())
1530                         model_print(" DETECTED BUG(S)");
1531         } else
1532                 print_infeasibility(" INFEASIBLE");
1533         model_print("\n");
1534
1535         print_list(&action_trace);
1536         model_print("\n");
1537
1538 }
1539
1540 /**
1541  * Add a Thread to the system for the first time. Should only be called once
1542  * per thread.
1543  * @param t The Thread to add
1544  */
1545 void ModelExecution::add_thread(Thread *t)
1546 {
1547         unsigned int i = id_to_int(t->get_id());
1548         if (i >= thread_map.size())
1549                 thread_map.resize(i + 1);
1550         thread_map[i] = t;
1551         if (!t->is_model_thread())
1552                 scheduler->add_thread(t);
1553 }
1554
1555 /**
1556  * @brief Get a Thread reference by its ID
1557  * @param tid The Thread's ID
1558  * @return A Thread reference
1559  */
1560 Thread * ModelExecution::get_thread(thread_id_t tid) const
1561 {
1562         unsigned int i = id_to_int(tid);
1563         if (i < thread_map.size())
1564                 return thread_map[i];
1565         return NULL;
1566 }
1567
1568 /**
1569  * @brief Get a reference to the Thread in which a ModelAction was executed
1570  * @param act The ModelAction
1571  * @return A Thread reference
1572  */
1573 Thread * ModelExecution::get_thread(const ModelAction *act) const
1574 {
1575         return get_thread(act->get_tid());
1576 }
1577
1578 /**
1579  * @brief Get a Thread reference by its pthread ID
1580  * @param index The pthread's ID
1581  * @return A Thread reference
1582  */
1583 Thread * ModelExecution::get_pthread(pthread_t pid) {
1584         union {
1585                 pthread_t p;
1586                 uint32_t v;
1587         } x;
1588         x.p = pid;
1589         uint32_t thread_id = x.v;
1590         if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1591         else return NULL;
1592 }
1593
1594 /**
1595  * @brief Check if a Thread is currently enabled
1596  * @param t The Thread to check
1597  * @return True if the Thread is currently enabled
1598  */
1599 bool ModelExecution::is_enabled(Thread *t) const
1600 {
1601         return scheduler->is_enabled(t);
1602 }
1603
1604 /**
1605  * @brief Check if a Thread is currently enabled
1606  * @param tid The ID of the Thread to check
1607  * @return True if the Thread is currently enabled
1608  */
1609 bool ModelExecution::is_enabled(thread_id_t tid) const
1610 {
1611         return scheduler->is_enabled(tid);
1612 }
1613
1614 /**
1615  * @brief Select the next thread to execute based on the curren action
1616  *
1617  * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1618  * actions should be followed by the execution of their child thread. In either
1619  * case, the current action should determine the next thread schedule.
1620  *
1621  * @param curr The current action
1622  * @return The next thread to run, if the current action will determine this
1623  * selection; otherwise NULL
1624  */
1625 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1626 {
1627         /* Do not split atomic RMW */
1628         if (curr->is_rmwr())
1629                 return get_thread(curr);
1630         /* Follow CREATE with the created thread */
1631         /* which is not needed, because model.cc takes care of this */
1632         if (curr->get_type() == THREAD_CREATE)
1633                 return curr->get_thread_operand();
1634         if (curr->get_type() == PTHREAD_CREATE) {
1635                 return curr->get_thread_operand();
1636         }
1637         return NULL;
1638 }
1639
1640 /**
1641  * Takes the next step in the execution, if possible.
1642  * @param curr The current step to take
1643  * @return Returns the next Thread to run, if any; NULL if this execution
1644  * should terminate
1645  */
1646 Thread * ModelExecution::take_step(ModelAction *curr)
1647 {
1648         Thread *curr_thrd = get_thread(curr);
1649         ASSERT(curr_thrd->get_state() == THREAD_READY);
1650
1651         ASSERT(check_action_enabled(curr));     /* May have side effects? */
1652         curr = check_current_action(curr);
1653         ASSERT(curr);
1654
1655         /* Process this action in ModelHistory for records*/
1656         model->get_history()->process_action( curr, curr->get_tid() );
1657
1658         if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1659                 scheduler->remove_thread(curr_thrd);
1660
1661         return action_select_next_thread(curr);
1662 }
1663
1664 Fuzzer * ModelExecution::getFuzzer() {
1665         return fuzzer;
1666 }