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