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