execution.cc

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