execution.cc

   1 #include <stdio.h>
   2 #include <algorithm>
   3 #include <new>
   4 #include <stdarg.h>
   5
   6 #include "model.h"
   7 #include "execution.h"
   8 #include "action.h"
   9 #include "schedule.h"
  10 #include "common.h"
  11 #include "clockvector.h"
  12 #include "cyclegraph.h"
  13 #include "datarace.h"
  14 #include "threads-model.h"
  15 #include "bugmessage.h"
  16 #include "history.h"
  17 #include "fuzzer.h"
  18 #include "newfuzzer.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                 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 asserted;
  45
  46         SNAPSHOTALLOC
  47 };
  48
  49 /** @brief Constructor */
  50 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
  51         model(m),
  52         params(NULL),
  53         scheduler(scheduler),
  54         thread_map(2),  /* We'll always need at least 2 threads */
  55         pthread_map(0),
  56         pthread_counter(2),
  57         action_trace(),
  58         obj_map(),
  59         condvar_waiters_map(),
  60         obj_thrd_map(),
  61         obj_wr_thrd_map(),
  62         obj_last_sc_map(),
  63         mutex_map(),
  64         cond_map(),
  65         thrd_last_action(1),
  66         thrd_last_fence_release(),
  67         priv(new struct model_snapshot_members ()),
  68         mo_graph(new CycleGraph()),
  69 #ifdef NEWFUZZER
  70         fuzzer(new NewFuzzer()),
  71 #else
  72         fuzzer(new Fuzzer()),
  73 #endif
  74         isfinished(false)
  75 {
  76         /* Initialize a model-checker thread, for special ModelActions */
  77         model_thread = new Thread(get_next_id());
  78         add_thread(model_thread);
  79         fuzzer->register_engine(m, this);
  80         scheduler->register_engine(this);
  81 #ifdef TLS
  82         pthread_key_create(&pthreadkey, tlsdestructor);
  83 #endif
  84 }
  85
  86 /** @brief Destructor */
  87 ModelExecution::~ModelExecution()
  88 {
  89         for (unsigned int i = 0;i < get_num_threads();i++)
  90                 delete get_thread(int_to_id(i));
  91
  92         delete mo_graph;
  93         delete priv;
  94 }
  95
  96 int ModelExecution::get_execution_number() const
  97 {
  98         return model->get_execution_number();
  99 }
 100
 101 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 2> * hash, void * ptr)
 102 {
 103         action_list_t *tmp = hash->get(ptr);
 104         if (tmp == NULL) {
 105                 tmp = new action_list_t();
 106                 hash->put(ptr, tmp);
 107         }
 108         return tmp;
 109 }
 110
 111 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 2> * hash, void * ptr)
 112 {
 113         SnapVector<action_list_t> *tmp = hash->get(ptr);
 114         if (tmp == NULL) {
 115                 tmp = new SnapVector<action_list_t>();
 116                 hash->put(ptr, tmp);
 117         }
 118         return tmp;
 119 }
 120
 121 /** @return a thread ID for a new Thread */
 122 thread_id_t ModelExecution::get_next_id()
 123 {
 124         return priv->next_thread_id++;
 125 }
 126
 127 /** @return the number of user threads created during this execution */
 128 unsigned int ModelExecution::get_num_threads() const
 129 {
 130         return priv->next_thread_id;
 131 }
 132
 133 /** @return a sequence number for a new ModelAction */
 134 modelclock_t ModelExecution::get_next_seq_num()
 135 {
 136         return ++priv->used_sequence_numbers;
 137 }
 138
 139 /** @return a sequence number for a new ModelAction */
 140 modelclock_t ModelExecution::get_curr_seq_num()
 141 {
 142         return priv->used_sequence_numbers;
 143 }
 144
 145 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
 146 void ModelExecution::restore_last_seq_num()
 147 {
 148         priv->used_sequence_numbers--;
 149 }
 150
 151 /**
 152  * @brief Should the current action wake up a given thread?
 153  *
 154  * @param curr The current action
 155  * @param thread The thread that we might wake up
 156  * @return True, if we should wake up the sleeping thread; false otherwise
 157  */
 158 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
 159 {
 160         const ModelAction *asleep = thread->get_pending();
 161         /* Don't allow partial RMW to wake anyone up */
 162         if (curr->is_rmwr())
 163                 return false;
 164         /* Synchronizing actions may have been backtracked */
 165         if (asleep->could_synchronize_with(curr))
 166                 return true;
 167         /* All acquire/release fences and fence-acquire/store-release */
 168         if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
 169                 return true;
 170         /* Fence-release + store can awake load-acquire on the same location */
 171         if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
 172                 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
 173                 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
 174                         return true;
 175         }
 176         /* The sleep is literally sleeping */
 177         if (asleep->is_sleep()) {
 178                 if (fuzzer->shouldWake(asleep))
 179                         return true;
 180         }
 181
 182         return false;
 183 }
 184
 185 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 186 {
 187         for (unsigned int i = 0;i < get_num_threads();i++) {
 188                 Thread *thr = get_thread(int_to_id(i));
 189                 if (scheduler->is_sleep_set(thr)) {
 190                         if (should_wake_up(curr, thr)) {
 191                                 /* Remove this thread from sleep set */
 192                                 scheduler->remove_sleep(thr);
 193                                 if (thr->get_pending()->is_sleep())
 194                                         thr->set_wakeup_state(true);
 195                         }
 196                 }
 197         }
 198 }
 199
 200 void ModelExecution::assert_bug(const char *msg)
 201 {
 202         priv->bugs.push_back(new bug_message(msg));
 203         set_assert();
 204 }
 205
 206 /** @return True, if any bugs have been reported for this execution */
 207 bool ModelExecution::have_bug_reports() const
 208 {
 209         return priv->bugs.size() != 0;
 210 }
 211
 212 SnapVector<bug_message *> * ModelExecution::get_bugs() const
 213 {
 214         return &priv->bugs;
 215 }
 216
 217 /**
 218  * Check whether the current trace has triggered an assertion which should halt
 219  * its execution.
 220  *
 221  * @return True, if the execution should be aborted; false otherwise
 222  */
 223 bool ModelExecution::has_asserted() const
 224 {
 225         return priv->asserted;
 226 }
 227
 228 /**
 229  * Trigger a trace assertion which should cause this execution to be halted.
 230  * This can be due to a detected bug or due to an infeasibility that should
 231  * halt ASAP.
 232  */
 233 void ModelExecution::set_assert()
 234 {
 235         priv->asserted = true;
 236 }
 237
 238 /**
 239  * Check if we are in a deadlock. Should only be called at the end of an
 240  * execution, although it should not give false positives in the middle of an
 241  * execution (there should be some ENABLED thread).
 242  *
 243  * @return True if program is in a deadlock; false otherwise
 244  */
 245 bool ModelExecution::is_deadlocked() const
 246 {
 247         bool blocking_threads = false;
 248         for (unsigned int i = 0;i < get_num_threads();i++) {
 249                 thread_id_t tid = int_to_id(i);
 250                 if (is_enabled(tid))
 251                         return false;
 252                 Thread *t = get_thread(tid);
 253                 if (!t->is_model_thread() && t->get_pending())
 254                         blocking_threads = true;
 255         }
 256         return blocking_threads;
 257 }
 258
 259 /**
 260  * Check if this is a complete execution. That is, have all thread completed
 261  * execution (rather than exiting because sleep sets have forced a redundant
 262  * execution).
 263  *
 264  * @return True if the execution is complete.
 265  */
 266 bool ModelExecution::is_complete_execution() const
 267 {
 268         for (unsigned int i = 0;i < get_num_threads();i++)
 269                 if (is_enabled(int_to_id(i)))
 270                         return false;
 271         return true;
 272 }
 273
 274 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
 275         uint64_t value = *((const uint64_t *) location);
 276         modelclock_t storeclock;
 277         thread_id_t storethread;
 278         getStoreThreadAndClock(location, &storethread, &storeclock);
 279         setAtomicStoreFlag(location);
 280         ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
 281         act->set_seq_number(storeclock);
 282         add_normal_write_to_lists(act);
 283         add_write_to_lists(act);
 284         w_modification_order(act);
 285 #ifdef NEWFUZZER
 286         model->get_history()->process_action(act, act->get_tid());
 287 #endif
 288         return act;
 289 }
 290
 291 /**
 292  * Processes a read model action.
 293  * @param curr is the read model action to process.
 294  * @param rf_set is the set of model actions we can possibly read from
 295  * @return True if the read can be pruned from the thread map list.
 296  */
 297 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 298 {
 299         SnapVector<ModelAction *> * priorset = new SnapVector<ModelAction *>();
 300         bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
 301         if (hasnonatomicstore) {
 302                 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
 303                 rf_set->push_back(nonatomicstore);
 304         }
 305
 306         // Remove writes that violate read modification order
 307         /*
 308            uint i = 0;
 309            while (i < rf_set->size()) {
 310                 ModelAction * rf = (*rf_set)[i];
 311                 if (!r_modification_order(curr, rf, NULL, NULL, true)) {
 312                         (*rf_set)[i] = rf_set->back();
 313                         rf_set->pop_back();
 314                 } else
 315                         i++;
 316            }*/
 317
 318         while(true) {
 319                 int index = fuzzer->selectWrite(curr, rf_set);
 320
 321                 ModelAction *rf = (*rf_set)[index];
 322
 323                 ASSERT(rf);
 324                 bool canprune = false;
 325                 if (r_modification_order(curr, rf, priorset, &canprune)) {
 326                         for(unsigned int i=0;i<priorset->size();i++) {
 327                                 mo_graph->addEdge((*priorset)[i], rf);
 328                         }
 329                         read_from(curr, rf);
 330                         get_thread(curr)->set_return_value(curr->get_return_value());
 331                         delete priorset;
 332                         //Update acquire fence clock vector
 333                         ClockVector * hbcv = get_hb_from_write(curr->get_reads_from());
 334                         if (hbcv != NULL)
 335                                 get_thread(curr)->get_acq_fence_cv()->merge(hbcv);
 336                         return canprune && (curr->get_type() == ATOMIC_READ);
 337                 }
 338                 priorset->clear();
 339                 (*rf_set)[index] = rf_set->back();
 340                 rf_set->pop_back();
 341         }
 342 }
 343
 344 /**
 345  * Processes a lock, trylock, or unlock model action.  @param curr is
 346  * the read model action to process.
 347  *
 348  * The try lock operation checks whether the lock is taken.  If not,
 349  * it falls to the normal lock operation case.  If so, it returns
 350  * fail.
 351  *
 352  * The lock operation has already been checked that it is enabled, so
 353  * it just grabs the lock and synchronizes with the previous unlock.
 354  *
 355  * The unlock operation has to re-enable all of the threads that are
 356  * waiting on the lock.
 357  *
 358  * @return True if synchronization was updated; false otherwise
 359  */
 360 bool ModelExecution::process_mutex(ModelAction *curr)
 361 {
 362         cdsc::mutex *mutex = curr->get_mutex();
 363         struct cdsc::mutex_state *state = NULL;
 364
 365         if (mutex)
 366                 state = mutex->get_state();
 367
 368         switch (curr->get_type()) {
 369         case ATOMIC_TRYLOCK: {
 370                 bool success = !state->locked;
 371                 curr->set_try_lock(success);
 372                 if (!success) {
 373                         get_thread(curr)->set_return_value(0);
 374                         break;
 375                 }
 376                 get_thread(curr)->set_return_value(1);
 377         }
 378         //otherwise fall into the lock case
 379         case ATOMIC_LOCK: {
 380                 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
 381                 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
 382                 //      assert_bug("Lock access before initialization");
 383                 state->locked = get_thread(curr);
 384                 ModelAction *unlock = get_last_unlock(curr);
 385                 //synchronize with the previous unlock statement
 386                 if (unlock != NULL) {
 387                         synchronize(unlock, curr);
 388                         return true;
 389                 }
 390                 break;
 391         }
 392         case ATOMIC_WAIT: {
 393                 //TODO: DOESN'T REALLY IMPLEMENT SPURIOUS WAKEUPS CORRECTLY
 394                 if (fuzzer->shouldWait(curr)) {
 395                         /* wake up the other threads */
 396                         for (unsigned int i = 0;i < get_num_threads();i++) {
 397                                 Thread *t = get_thread(int_to_id(i));
 398                                 Thread *curr_thrd = get_thread(curr);
 399                                 if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
 400                                         scheduler->wake(t);
 401                         }
 402
 403                         /* unlock the lock - after checking who was waiting on it */
 404                         state->locked = NULL;
 405
 406                         /* disable this thread */
 407                         get_safe_ptr_action(&condvar_waiters_map, curr->get_location())->addAction(curr);
 408                         scheduler->sleep(get_thread(curr));
 409                 }
 410
 411                 break;
 412         }
 413         case ATOMIC_TIMEDWAIT:
 414         case ATOMIC_UNLOCK: {
 415                 //TODO: FIX WAIT SITUATION...WAITS CAN SPURIOUSLY
 416                 //FAIL...TIMED WAITS SHOULD PROBABLY JUST BE THE SAME
 417                 //AS NORMAL WAITS...THINK ABOUT PROBABILITIES
 418                 //THOUGH....AS IN TIMED WAIT MUST FAIL TO GUARANTEE
 419                 //PROGRESS...NORMAL WAIT MAY FAIL...SO NEED NORMAL
 420                 //WAIT TO WORK CORRECTLY IN THE CASE IT SPURIOUSLY
 421                 //FAILS AND IN THE CASE IT DOESN'T...  TIMED WAITS
 422                 //MUST EVENMTUALLY RELEASE...
 423
 424                 /* wake up the other threads */
 425                 for (unsigned int i = 0;i < get_num_threads();i++) {
 426                         Thread *t = get_thread(int_to_id(i));
 427                         Thread *curr_thrd = get_thread(curr);
 428                         if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
 429                                 scheduler->wake(t);
 430                 }
 431
 432                 /* unlock the lock - after checking who was waiting on it */
 433                 state->locked = NULL;
 434                 break;
 435         }
 436         case ATOMIC_NOTIFY_ALL: {
 437                 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
 438                 //activate all the waiting threads
 439                 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
 440                         scheduler->wake(get_thread(rit->getVal()));
 441                 }
 442                 waiters->clear();
 443                 break;
 444         }
 445         case ATOMIC_NOTIFY_ONE: {
 446                 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
 447                 if (waiters->size() != 0) {
 448                         Thread * thread = fuzzer->selectNotify(waiters);
 449                         scheduler->wake(thread);
 450                 }
 451                 break;
 452         }
 453
 454         default:
 455                 ASSERT(0);
 456         }
 457         return false;
 458 }
 459
 460 /**
 461  * Process a write ModelAction
 462  * @param curr The ModelAction to process
 463  * @return True if the mo_graph was updated or promises were resolved
 464  */
 465 void ModelExecution::process_write(ModelAction *curr)
 466 {
 467         w_modification_order(curr);
 468         get_thread(curr)->set_return_value(VALUE_NONE);
 469 }
 470
 471 /**
 472  * Process a fence ModelAction
 473  * @param curr The ModelAction to process
 474  * @return True if synchronization was updated
 475  */
 476 void ModelExecution::process_fence(ModelAction *curr)
 477 {
 478         /*
 479          * fence-relaxed: no-op
 480          * fence-release: only log the occurence (not in this function), for
 481          *   use in later synchronization
 482          * fence-acquire (this function): search for hypothetical release
 483          *   sequences
 484          * fence-seq-cst: MO constraints formed in {r,w}_modification_order
 485          */
 486         if (curr->is_acquire()) {
 487                 curr->get_cv()->merge(get_thread(curr)->get_acq_fence_cv());
 488         }
 489 }
 490
 491 /**
 492  * @brief Process the current action for thread-related activity
 493  *
 494  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
 495  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
 496  * synchronization, etc.  This function is a no-op for non-THREAD actions
 497  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
 498  *
 499  * @param curr The current action
 500  * @return True if synchronization was updated or a thread completed
 501  */
 502 void ModelExecution::process_thread_action(ModelAction *curr)
 503 {
 504         switch (curr->get_type()) {
 505         case THREAD_CREATE: {
 506                 thrd_t *thrd = (thrd_t *)curr->get_location();
 507                 struct thread_params *params = (struct thread_params *)curr->get_value();
 508                 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
 509                 curr->set_thread_operand(th);
 510                 add_thread(th);
 511                 th->set_creation(curr);
 512                 break;
 513         }
 514         case PTHREAD_CREATE: {
 515                 (*(uint32_t *)curr->get_location()) = pthread_counter++;
 516
 517                 struct pthread_params *params = (struct pthread_params *)curr->get_value();
 518                 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
 519                 curr->set_thread_operand(th);
 520                 add_thread(th);
 521                 th->set_creation(curr);
 522
 523                 if ( pthread_map.size() < pthread_counter )
 524                         pthread_map.resize( pthread_counter );
 525                 pthread_map[ pthread_counter-1 ] = th;
 526
 527                 break;
 528         }
 529         case THREAD_JOIN: {
 530                 Thread *blocking = curr->get_thread_operand();
 531                 ModelAction *act = get_last_action(blocking->get_id());
 532                 synchronize(act, curr);
 533                 break;
 534         }
 535         case PTHREAD_JOIN: {
 536                 Thread *blocking = curr->get_thread_operand();
 537                 ModelAction *act = get_last_action(blocking->get_id());
 538                 synchronize(act, curr);
 539                 break;  // WL: to be add (modified)
 540         }
 541
 542         case THREADONLY_FINISH:
 543         case THREAD_FINISH: {
 544                 Thread *th = get_thread(curr);
 545                 if (curr->get_type() == THREAD_FINISH &&
 546                                 th == model->getInitThread()) {
 547                         th->complete();
 548                         setFinished();
 549                         break;
 550                 }
 551
 552                 /* Wake up any joining threads */
 553                 for (unsigned int i = 0;i < get_num_threads();i++) {
 554                         Thread *waiting = get_thread(int_to_id(i));
 555                         if (waiting->waiting_on() == th &&
 556                                         waiting->get_pending()->is_thread_join())
 557                                 scheduler->wake(waiting);
 558                 }
 559                 th->complete();
 560                 break;
 561         }
 562         case THREAD_START: {
 563                 break;
 564         }
 565         case THREAD_SLEEP: {
 566                 Thread *th = get_thread(curr);
 567                 th->set_pending(curr);
 568                 scheduler->add_sleep(th);
 569                 break;
 570         }
 571         default:
 572                 break;
 573         }
 574 }
 575
 576 /**
 577  * Initialize the current action by performing one or more of the following
 578  * actions, as appropriate: merging RMWR and RMWC/RMW actions,
 579  * manipulating backtracking sets, allocating and
 580  * initializing clock vectors, and computing the promises to fulfill.
 581  *
 582  * @param curr The current action, as passed from the user context; may be
 583  * freed/invalidated after the execution of this function, with a different
 584  * action "returned" its place (pass-by-reference)
 585  * @return True if curr is a newly-explored action; false otherwise
 586  */
 587 bool ModelExecution::initialize_curr_action(ModelAction **curr)
 588 {
 589         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
 590                 ModelAction *newcurr = process_rmw(*curr);
 591                 delete *curr;
 592
 593                 *curr = newcurr;
 594                 return false;
 595         } else {
 596                 ModelAction *newcurr = *curr;
 597
 598                 newcurr->set_seq_number(get_next_seq_num());
 599                 /* Always compute new clock vector */
 600                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 601
 602                 /* Assign most recent release fence */
 603                 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
 604
 605                 return true;    /* This was a new ModelAction */
 606         }
 607 }
 608
 609 /**
 610  * @brief Establish reads-from relation between two actions
 611  *
 612  * Perform basic operations involved with establishing a concrete rf relation,
 613  * including setting the ModelAction data and checking for release sequences.
 614  *
 615  * @param act The action that is reading (must be a read)
 616  * @param rf The action from which we are reading (must be a write)
 617  *
 618  * @return True if this read established synchronization
 619  */
 620
 621 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
 622 {
 623         ASSERT(rf);
 624         ASSERT(rf->is_write());
 625
 626         act->set_read_from(rf);
 627         if (act->is_acquire()) {
 628                 ClockVector *cv = get_hb_from_write(rf);
 629                 if (cv == NULL)
 630                         return;
 631                 act->get_cv()->merge(cv);
 632         }
 633 }
 634
 635 /**
 636  * @brief Synchronizes two actions
 637  *
 638  * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
 639  * This function performs the synchronization as well as providing other hooks
 640  * for other checks along with synchronization.
 641  *
 642  * @param first The left-hand side of the synchronizes-with relation
 643  * @param second The right-hand side of the synchronizes-with relation
 644  * @return True if the synchronization was successful (i.e., was consistent
 645  * with the execution order); false otherwise
 646  */
 647 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
 648 {
 649         if (*second < *first) {
 650                 ASSERT(0);      //This should not happend
 651                 return false;
 652         }
 653         return second->synchronize_with(first);
 654 }
 655
 656 /**
 657  * @brief Check whether a model action is enabled.
 658  *
 659  * Checks whether an operation would be successful (i.e., is a lock already
 660  * locked, or is the joined thread already complete).
 661  *
 662  * For yield-blocking, yields are never enabled.
 663  *
 664  * @param curr is the ModelAction to check whether it is enabled.
 665  * @return a bool that indicates whether the action is enabled.
 666  */
 667 bool ModelExecution::check_action_enabled(ModelAction *curr) {
 668         if (curr->is_lock()) {
 669                 cdsc::mutex *lock = curr->get_mutex();
 670                 struct cdsc::mutex_state *state = lock->get_state();
 671                 if (state->locked)
 672                         return false;
 673         } else if (curr->is_thread_join()) {
 674                 Thread *blocking = curr->get_thread_operand();
 675                 if (!blocking->is_complete()) {
 676                         return false;
 677                 }
 678         } else if (curr->is_sleep()) {
 679                 if (!fuzzer->shouldSleep(curr))
 680                         return false;
 681         }
 682
 683         return true;
 684 }
 685
 686 /**
 687  * This is the heart of the model checker routine. It performs model-checking
 688  * actions corresponding to a given "current action." Among other processes, it
 689  * calculates reads-from relationships, updates synchronization clock vectors,
 690  * forms a memory_order constraints graph, and handles replay/backtrack
 691  * execution when running permutations of previously-observed executions.
 692  *
 693  * @param curr The current action to process
 694  * @return The ModelAction that is actually executed; may be different than
 695  * curr
 696  */
 697 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 698 {
 699         ASSERT(curr);
 700         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
 701         bool newly_explored = initialize_curr_action(&curr);
 702
 703         DBG();
 704
 705         wake_up_sleeping_actions(curr);
 706
 707         SnapVector<ModelAction *> * rf_set = NULL;
 708         /* Build may_read_from set for newly-created actions */
 709         if (newly_explored && curr->is_read())
 710                 rf_set = build_may_read_from(curr);
 711
 712         bool canprune = false;
 713
 714         if (curr->is_read() && !second_part_of_rmw) {
 715                 canprune = process_read(curr, rf_set);
 716                 delete rf_set;
 717         } else
 718                 ASSERT(rf_set == NULL);
 719
 720         /* Add the action to lists */
 721         if (!second_part_of_rmw)
 722                 add_action_to_lists(curr, canprune);
 723
 724         if (curr->is_write())
 725                 add_write_to_lists(curr);
 726
 727         process_thread_action(curr);
 728
 729         if (curr->is_write())
 730                 process_write(curr);
 731
 732         if (curr->is_fence())
 733                 process_fence(curr);
 734
 735         if (curr->is_mutex_op())
 736                 process_mutex(curr);
 737
 738         return curr;
 739 }
 740
 741 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 742 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
 743         ModelAction *lastread = get_last_action(act->get_tid());
 744         lastread->process_rmw(act);
 745         if (act->is_rmw()) {
 746                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
 747         }
 748         return lastread;
 749 }
 750
 751 /**
 752  * @brief Updates the mo_graph with the constraints imposed from the current
 753  * read.
 754  *
 755  * Basic idea is the following: Go through each other thread and find
 756  * the last action that happened before our read.  Two cases:
 757  *
 758  * -# The action is a write: that write must either occur before
 759  * the write we read from or be the write we read from.
 760  * -# The action is a read: the write that that action read from
 761  * must occur before the write we read from or be the same write.
 762  *
 763  * @param curr The current action. Must be a read.
 764  * @param rf The ModelAction or Promise that curr reads from. Must be a write.
 765  * @param check_only If true, then only check whether the current action satisfies
 766  *        read modification order or not, without modifiying priorset and canprune.
 767  *        False by default.
 768  * @return True if modification order edges were added; false otherwise
 769  */
 770
 771 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf,
 772                                                                                                                                                                         SnapVector<ModelAction *> * priorset, bool * canprune, bool check_only)
 773 {
 774         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
 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
 782         /* Need to ensure thrd_lists is big enough because we have not added the curr actions yet.  */
 783         if ((int)thrd_lists->size() <= tid) {
 784                 uint oldsize = thrd_lists->size();
 785                 thrd_lists->resize(priv->next_thread_id);
 786                 for(uint i = oldsize;i < priv->next_thread_id;i++)
 787                         new (&(*thrd_lists)[i]) action_list_t();
 788         }
 789
 790         ModelAction *prev_same_thread = NULL;
 791         /* Iterate over all threads */
 792         for (unsigned int i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
 793                 /* Last SC fence in thread tid */
 794                 ModelAction *last_sc_fence_thread_local = NULL;
 795                 if (i != 0)
 796                         last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
 797
 798                 /* Last SC fence in thread tid, before last SC fence in current thread */
 799                 ModelAction *last_sc_fence_thread_before = NULL;
 800                 if (last_sc_fence_local)
 801                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
 802
 803                 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
 804                 if (prev_same_thread != NULL &&
 805                                 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
 806                                 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
 807                         continue;
 808                 }
 809
 810                 /* Iterate over actions in thread, starting from most recent */
 811                 action_list_t *list = &(*thrd_lists)[tid];
 812                 sllnode<ModelAction *> * rit;
 813                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
 814                         ModelAction *act = rit->getVal();
 815
 816                         /* Skip curr */
 817                         if (act == curr)
 818                                 continue;
 819                         /* Don't want to add reflexive edges on 'rf' */
 820                         if (act->equals(rf)) {
 821                                 if (act->happens_before(curr))
 822                                         break;
 823                                 else
 824                                         continue;
 825                         }
 826
 827                         if (act->is_write()) {
 828                                 /* C++, Section 29.3 statement 5 */
 829                                 if (curr->is_seqcst() && last_sc_fence_thread_local &&
 830                                                 *act < *last_sc_fence_thread_local) {
 831                                         if (mo_graph->checkReachable(rf, act))
 832                                                 return false;
 833                                         if (!check_only)
 834                                                 priorset->push_back(act);
 835                                         break;
 836                                 }
 837                                 /* C++, Section 29.3 statement 4 */
 838                                 else if (act->is_seqcst() && last_sc_fence_local &&
 839                                                                  *act < *last_sc_fence_local) {
 840                                         if (mo_graph->checkReachable(rf, act))
 841                                                 return false;
 842                                         if (!check_only)
 843                                                 priorset->push_back(act);
 844                                         break;
 845                                 }
 846                                 /* C++, Section 29.3 statement 6 */
 847                                 else if (last_sc_fence_thread_before &&
 848                                                                  *act < *last_sc_fence_thread_before) {
 849                                         if (mo_graph->checkReachable(rf, act))
 850                                                 return false;
 851                                         if (!check_only)
 852                                                 priorset->push_back(act);
 853                                         break;
 854                                 }
 855                         }
 856
 857                         /*
 858                          * Include at most one act per-thread that "happens
 859                          * before" curr
 860                          */
 861                         if (act->happens_before(curr)) {
 862                                 if (i==0) {
 863                                         if (last_sc_fence_local == NULL ||
 864                                                         (*last_sc_fence_local < *act)) {
 865                                                 prev_same_thread = act;
 866                                         }
 867                                 }
 868                                 if (act->is_write()) {
 869                                         if (mo_graph->checkReachable(rf, act))
 870                                                 return false;
 871                                         if (!check_only)
 872                                                 priorset->push_back(act);
 873                                 } else {
 874                                         ModelAction *prevrf = act->get_reads_from();
 875                                         if (!prevrf->equals(rf)) {
 876                                                 if (mo_graph->checkReachable(rf, prevrf))
 877                                                         return false;
 878                                                 if (!check_only)
 879                                                         priorset->push_back(prevrf);
 880                                         } else {
 881                                                 if (act->get_tid() == curr->get_tid()) {
 882                                                         //Can prune curr from obj list
 883                                                         if (!check_only)
 884                                                                 *canprune = true;
 885                                                 }
 886                                         }
 887                                 }
 888                                 break;
 889                         }
 890                 }
 891         }
 892         return true;
 893 }
 894
 895 /**
 896  * Updates the mo_graph with the constraints imposed from the current write.
 897  *
 898  * Basic idea is the following: Go through each other thread and find
 899  * the lastest action that happened before our write.  Two cases:
 900  *
 901  * (1) The action is a write => that write must occur before
 902  * the current write
 903  *
 904  * (2) The action is a read => the write that that action read from
 905  * must occur before the current write.
 906  *
 907  * This method also handles two other issues:
 908  *
 909  * (I) Sequential Consistency: Making sure that if the current write is
 910  * seq_cst, that it occurs after the previous seq_cst write.
 911  *
 912  * (II) Sending the write back to non-synchronizing reads.
 913  *
 914  * @param curr The current action. Must be a write.
 915  * @param send_fv A vector for stashing reads to which we may pass our future
 916  * value. If NULL, then don't record any future values.
 917  * @return True if modification order edges were added; false otherwise
 918  */
 919 void ModelExecution::w_modification_order(ModelAction *curr)
 920 {
 921         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
 922         unsigned int i;
 923         ASSERT(curr->is_write());
 924
 925         SnapList<ModelAction *> edgeset;
 926
 927         if (curr->is_seqcst()) {
 928                 /* We have to at least see the last sequentially consistent write,
 929                          so we are initialized. */
 930                 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
 931                 if (last_seq_cst != NULL) {
 932                         edgeset.push_back(last_seq_cst);
 933                 }
 934                 //update map for next query
 935                 obj_last_sc_map.put(curr->get_location(), curr);
 936         }
 937
 938         /* Last SC fence in the current thread */
 939         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
 940
 941         /* Iterate over all threads */
 942         for (i = 0;i < thrd_lists->size();i++) {
 943                 /* Last SC fence in thread i, before last SC fence in current thread */
 944                 ModelAction *last_sc_fence_thread_before = NULL;
 945                 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
 946                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
 947
 948                 /* Iterate over actions in thread, starting from most recent */
 949                 action_list_t *list = &(*thrd_lists)[i];
 950                 sllnode<ModelAction*>* rit;
 951                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
 952                         ModelAction *act = rit->getVal();
 953                         if (act == curr) {
 954                                 /*
 955                                  * 1) If RMW and it actually read from something, then we
 956                                  * already have all relevant edges, so just skip to next
 957                                  * thread.
 958                                  *
 959                                  * 2) If RMW and it didn't read from anything, we should
 960                                  * whatever edge we can get to speed up convergence.
 961                                  *
 962                                  * 3) If normal write, we need to look at earlier actions, so
 963                                  * continue processing list.
 964                                  */
 965                                 if (curr->is_rmw()) {
 966                                         if (curr->get_reads_from() != NULL)
 967                                                 break;
 968                                         else
 969                                                 continue;
 970                                 } else
 971                                         continue;
 972                         }
 973
 974                         /* C++, Section 29.3 statement 7 */
 975                         if (last_sc_fence_thread_before && act->is_write() &&
 976                                         *act < *last_sc_fence_thread_before) {
 977                                 edgeset.push_back(act);
 978                                 break;
 979                         }
 980
 981                         /*
 982                          * Include at most one act per-thread that "happens
 983                          * before" curr
 984                          */
 985                         if (act->happens_before(curr)) {
 986                                 /*
 987                                  * Note: if act is RMW, just add edge:
 988                                  *   act --mo--> curr
 989                                  * The following edge should be handled elsewhere:
 990                                  *   readfrom(act) --mo--> act
 991                                  */
 992                                 if (act->is_write())
 993                                         edgeset.push_back(act);
 994                                 else if (act->is_read()) {
 995                                         //if previous read accessed a null, just keep going
 996                                         edgeset.push_back(act->get_reads_from());
 997                                 }
 998                                 break;
 999                         }
1000                 }
1001         }
1002         mo_graph->addEdges(&edgeset, curr);
1003
1004 }
1005
1006 /**
1007  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1008  * some constraints. This method checks one the following constraint (others
1009  * require compiler support):
1010  *
1011  *   If X --hb-> Y --mo-> Z, then X should not read from Z.
1012  *   If X --hb-> Y, A --rf-> Y, and A --mo-> Z, then X should not read from Z.
1013  */
1014 bool ModelExecution::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1015 {
1016         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(reader->get_location());
1017         unsigned int i;
1018         /* Iterate over all threads */
1019         for (i = 0;i < thrd_lists->size();i++) {
1020                 const ModelAction *write_after_read = NULL;
1021
1022                 /* Iterate over actions in thread, starting from most recent */
1023                 action_list_t *list = &(*thrd_lists)[i];
1024                 sllnode<ModelAction *>* rit;
1025                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1026                         ModelAction *act = rit->getVal();
1027
1028                         /* Don't disallow due to act == reader */
1029                         if (!reader->happens_before(act) || reader == act)
1030                                 break;
1031                         else if (act->is_write())
1032                                 write_after_read = act;
1033                         else if (act->is_read() && act->get_reads_from() != NULL)
1034                                 write_after_read = act->get_reads_from();
1035                 }
1036
1037                 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1038                         return false;
1039         }
1040         return true;
1041 }
1042
1043 /**
1044  * Computes the clock vector that happens before propagates from this write.
1045  *
1046  * @param rf The action that might be part of a release sequence. Must be a
1047  * write.
1048  * @return ClockVector of happens before relation.
1049  */
1050
1051 ClockVector * ModelExecution::get_hb_from_write(ModelAction *rf) const {
1052         SnapVector<ModelAction *> * processset = NULL;
1053         for ( ;rf != NULL;rf = rf->get_reads_from()) {
1054                 ASSERT(rf->is_write());
1055                 if (!rf->is_rmw() || (rf->is_acquire() && rf->is_release()) || rf->get_rfcv() != NULL)
1056                         break;
1057                 if (processset == NULL)
1058                         processset = new SnapVector<ModelAction *>();
1059                 processset->push_back(rf);
1060         }
1061
1062         int i = (processset == NULL) ? 0 : processset->size();
1063
1064         ClockVector * vec = NULL;
1065         while(true) {
1066                 if (rf->get_rfcv() != NULL) {
1067                         vec = rf->get_rfcv();
1068                 } else if (rf->is_acquire() && rf->is_release()) {
1069                         vec = rf->get_cv();
1070                 } else if (rf->is_release() && !rf->is_rmw()) {
1071                         vec = rf->get_cv();
1072                 } else if (rf->is_release()) {
1073                         //have rmw that is release and doesn't have a rfcv
1074                         (vec = new ClockVector(vec, NULL))->merge(rf->get_cv());
1075                         rf->set_rfcv(vec);
1076                 } else {
1077                         //operation that isn't release
1078                         if (rf->get_last_fence_release()) {
1079                                 if (vec == NULL)
1080                                         vec = rf->get_last_fence_release()->get_cv();
1081                                 else
1082                                         (vec=new ClockVector(vec, NULL))->merge(rf->get_last_fence_release()->get_cv());
1083                         }
1084                         rf->set_rfcv(vec);
1085                 }
1086                 i--;
1087                 if (i >= 0) {
1088                         rf = (*processset)[i];
1089                 } else
1090                         break;
1091         }
1092         if (processset != NULL)
1093                 delete processset;
1094         return vec;
1095 }
1096
1097 /**
1098  * Performs various bookkeeping operations for the current ModelAction. For
1099  * instance, adds action to the per-object, per-thread action vector and to the
1100  * action trace list of all thread actions.
1101  *
1102  * @param act is the ModelAction to add.
1103  */
1104 void ModelExecution::add_action_to_lists(ModelAction *act, bool canprune)
1105 {
1106         int tid = id_to_int(act->get_tid());
1107         if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1108                 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1109                 list->addAction(act);
1110         }
1111
1112         // Update action trace, a total order of all actions
1113         action_trace.addAction(act);
1114
1115
1116         // Update obj_thrd_map, a per location, per thread, order of actions
1117         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1118         if ((int)vec->size() <= tid) {
1119                 uint oldsize = vec->size();
1120                 vec->resize(priv->next_thread_id);
1121                 for(uint i = oldsize;i < priv->next_thread_id;i++)
1122                         new (&(*vec)[i]) action_list_t();
1123         }
1124         if (!canprune && (act->is_read() || act->is_write()))
1125                 (*vec)[tid].addAction(act);
1126
1127         // Update thrd_last_action, the last action taken by each thread
1128         if ((int)thrd_last_action.size() <= tid)
1129                 thrd_last_action.resize(get_num_threads());
1130         thrd_last_action[tid] = act;
1131
1132         // Update thrd_last_fence_release, the last release fence taken by each thread
1133         if (act->is_fence() && act->is_release()) {
1134                 if ((int)thrd_last_fence_release.size() <= tid)
1135                         thrd_last_fence_release.resize(get_num_threads());
1136                 thrd_last_fence_release[tid] = act;
1137         }
1138
1139         if (act->is_wait()) {
1140                 void *mutex_loc = (void *) act->get_value();
1141                 get_safe_ptr_action(&obj_map, mutex_loc)->addAction(act);
1142         }
1143 }
1144
1145 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1146         list->addAction(act);
1147 }
1148
1149 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1150         act->create_cv(NULL);
1151         list->addAction(act);
1152 }
1153
1154 /**
1155  * Performs various bookkeeping operations for a normal write.  The
1156  * complication is that we are typically inserting a normal write
1157  * lazily, so we need to insert it into the middle of lists.
1158  *
1159  * @param act is the ModelAction to add.
1160  */
1161
1162 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1163 {
1164         int tid = id_to_int(act->get_tid());
1165         insertIntoActionListAndSetCV(&action_trace, act);
1166
1167         // Update obj_thrd_map, a per location, per thread, order of actions
1168         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1169         if (tid >= (int)vec->size()) {
1170                 uint oldsize =vec->size();
1171                 vec->resize(priv->next_thread_id);
1172                 for(uint i=oldsize;i<priv->next_thread_id;i++)
1173                         new (&(*vec)[i]) action_list_t();
1174         }
1175         insertIntoActionList(&(*vec)[tid],act);
1176
1177         ModelAction * lastact = thrd_last_action[tid];
1178         // Update thrd_last_action, the last action taken by each thrad
1179         if (lastact == NULL || lastact->get_seq_number() == act->get_seq_number())
1180                 thrd_last_action[tid] = act;
1181 }
1182
1183
1184 void ModelExecution::add_write_to_lists(ModelAction *write) {
1185         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, write->get_location());
1186         int tid = id_to_int(write->get_tid());
1187         if (tid >= (int)vec->size()) {
1188                 uint oldsize =vec->size();
1189                 vec->resize(priv->next_thread_id);
1190                 for(uint i=oldsize;i<priv->next_thread_id;i++)
1191                         new (&(*vec)[i]) action_list_t();
1192         }
1193         (*vec)[tid].addAction(write);
1194 }
1195
1196 /**
1197  * @brief Get the last action performed by a particular Thread
1198  * @param tid The thread ID of the Thread in question
1199  * @return The last action in the thread
1200  */
1201 ModelAction * ModelExecution::get_last_action(thread_id_t tid) const
1202 {
1203         int threadid = id_to_int(tid);
1204         if (threadid < (int)thrd_last_action.size())
1205                 return thrd_last_action[id_to_int(tid)];
1206         else
1207                 return NULL;
1208 }
1209
1210 /**
1211  * @brief Get the last fence release performed by a particular Thread
1212  * @param tid The thread ID of the Thread in question
1213  * @return The last fence release in the thread, if one exists; NULL otherwise
1214  */
1215 ModelAction * ModelExecution::get_last_fence_release(thread_id_t tid) const
1216 {
1217         int threadid = id_to_int(tid);
1218         if (threadid < (int)thrd_last_fence_release.size())
1219                 return thrd_last_fence_release[id_to_int(tid)];
1220         else
1221                 return NULL;
1222 }
1223
1224 /**
1225  * Gets the last memory_order_seq_cst write (in the total global sequence)
1226  * performed on a particular object (i.e., memory location), not including the
1227  * current action.
1228  * @param curr The current ModelAction; also denotes the object location to
1229  * check
1230  * @return The last seq_cst write
1231  */
1232 ModelAction * ModelExecution::get_last_seq_cst_write(ModelAction *curr) const
1233 {
1234         void *location = curr->get_location();
1235         return obj_last_sc_map.get(location);
1236 }
1237
1238 /**
1239  * Gets the last memory_order_seq_cst fence (in the total global sequence)
1240  * performed in a particular thread, prior to a particular fence.
1241  * @param tid The ID of the thread to check
1242  * @param before_fence The fence from which to begin the search; if NULL, then
1243  * search for the most recent fence in the thread.
1244  * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
1245  */
1246 ModelAction * ModelExecution::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
1247 {
1248         /* All fences should have location FENCE_LOCATION */
1249         action_list_t *list = obj_map.get(FENCE_LOCATION);
1250
1251         if (!list)
1252                 return NULL;
1253
1254         sllnode<ModelAction*>* rit = list->end();
1255
1256         if (before_fence) {
1257                 for (;rit != NULL;rit=rit->getPrev())
1258                         if (rit->getVal() == before_fence)
1259                                 break;
1260
1261                 ASSERT(rit->getVal() == before_fence);
1262                 rit=rit->getPrev();
1263         }
1264
1265         for (;rit != NULL;rit=rit->getPrev()) {
1266                 ModelAction *act = rit->getVal();
1267                 if (act->is_fence() && (tid == act->get_tid()) && act->is_seqcst())
1268                         return act;
1269         }
1270         return NULL;
1271 }
1272
1273 /**
1274  * Gets the last unlock operation performed on a particular mutex (i.e., memory
1275  * location). This function identifies the mutex according to the current
1276  * action, which is presumed to perform on the same mutex.
1277  * @param curr The current ModelAction; also denotes the object location to
1278  * check
1279  * @return The last unlock operation
1280  */
1281 ModelAction * ModelExecution::get_last_unlock(ModelAction *curr) const
1282 {
1283         void *location = curr->get_location();
1284
1285         action_list_t *list = obj_map.get(location);
1286         if (list == NULL)
1287                 return NULL;
1288
1289         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1290         sllnode<ModelAction*>* rit;
1291         for (rit = list->end();rit != NULL;rit=rit->getPrev())
1292                 if (rit->getVal()->is_unlock() || rit->getVal()->is_wait())
1293                         return rit->getVal();
1294         return NULL;
1295 }
1296
1297 ModelAction * ModelExecution::get_parent_action(thread_id_t tid) const
1298 {
1299         ModelAction *parent = get_last_action(tid);
1300         if (!parent)
1301                 parent = get_thread(tid)->get_creation();
1302         return parent;
1303 }
1304
1305 /**
1306  * Returns the clock vector for a given thread.
1307  * @param tid The thread whose clock vector we want
1308  * @return Desired clock vector
1309  */
1310 ClockVector * ModelExecution::get_cv(thread_id_t tid) const
1311 {
1312         ModelAction *firstaction=get_parent_action(tid);
1313         return firstaction != NULL ? firstaction->get_cv() : NULL;
1314 }
1315
1316 bool valequals(uint64_t val1, uint64_t val2, int size) {
1317         switch(size) {
1318         case 1:
1319                 return ((uint8_t)val1) == ((uint8_t)val2);
1320         case 2:
1321                 return ((uint16_t)val1) == ((uint16_t)val2);
1322         case 4:
1323                 return ((uint32_t)val1) == ((uint32_t)val2);
1324         case 8:
1325                 return val1==val2;
1326         default:
1327                 ASSERT(0);
1328                 return false;
1329         }
1330 }
1331
1332 /**
1333  * Build up an initial set of all past writes that this 'read' action may read
1334  * from, as well as any previously-observed future values that must still be valid.
1335  *
1336  * @param curr is the current ModelAction that we are exploring; it must be a
1337  * 'read' operation.
1338  */
1339 SnapVector<ModelAction *> *  ModelExecution::build_may_read_from(ModelAction *curr)
1340 {
1341         SnapVector<action_list_t> *thrd_lists = obj_wr_thrd_map.get(curr->get_location());
1342         unsigned int i;
1343         ASSERT(curr->is_read());
1344
1345         ModelAction *last_sc_write = NULL;
1346
1347         if (curr->is_seqcst())
1348                 last_sc_write = get_last_seq_cst_write(curr);
1349
1350         SnapVector<ModelAction *> * rf_set = new SnapVector<ModelAction *>();
1351
1352         /* Iterate over all threads */
1353         if (thrd_lists != NULL)
1354                 for (i = 0;i < thrd_lists->size();i++) {
1355                         /* Iterate over actions in thread, starting from most recent */
1356                         action_list_t *list = &(*thrd_lists)[i];
1357                         sllnode<ModelAction *> * rit;
1358                         for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
1359                                 ModelAction *act = rit->getVal();
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 static void print_list(action_list_t *list)
1404 {
1405         sllnode<ModelAction*> *it;
1406
1407         model_print("------------------------------------------------------------------------------------\n");
1408         model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
1409         model_print("------------------------------------------------------------------------------------\n");
1410
1411         unsigned int hash = 0;
1412
1413         for (it = list->begin();it != NULL;it=it->getNext()) {
1414                 const ModelAction *act = it->getVal();
1415                 if (act->get_seq_number() > 0)
1416                         act->print();
1417                 hash = hash^(hash<<3)^(it->getVal()->hash());
1418         }
1419         model_print("HASH %u\n", hash);
1420         model_print("------------------------------------------------------------------------------------\n");
1421 }
1422
1423 #if SUPPORT_MOD_ORDER_DUMP
1424 void ModelExecution::dumpGraph(char *filename)
1425 {
1426         char buffer[200];
1427         sprintf(buffer, "%s.dot", filename);
1428         FILE *file = fopen(buffer, "w");
1429         fprintf(file, "digraph %s {\n", filename);
1430         mo_graph->dumpNodes(file);
1431         ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
1432
1433         for (sllnode<ModelAction*>* it = action_trace.begin();it != NULL;it=it->getNext()) {
1434                 ModelAction *act = it->getVal();
1435                 if (act->is_read()) {
1436                         mo_graph->dot_print_node(file, act);
1437                         mo_graph->dot_print_edge(file,
1438                                                                                                                          act->get_reads_from(),
1439                                                                                                                          act,
1440                                                                                                                          "label=\"rf\", color=red, weight=2");
1441                 }
1442                 if (thread_array[act->get_tid()]) {
1443                         mo_graph->dot_print_edge(file,
1444                                                                                                                          thread_array[id_to_int(act->get_tid())],
1445                                                                                                                          act,
1446                                                                                                                          "label=\"sb\", color=blue, weight=400");
1447                 }
1448
1449                 thread_array[act->get_tid()] = act;
1450         }
1451         fprintf(file, "}\n");
1452         model_free(thread_array);
1453         fclose(file);
1454 }
1455 #endif
1456
1457 /** @brief Prints an execution trace summary. */
1458 void ModelExecution::print_summary()
1459 {
1460 #if SUPPORT_MOD_ORDER_DUMP
1461         char buffername[100];
1462         sprintf(buffername, "exec%04u", get_execution_number());
1463         mo_graph->dumpGraphToFile(buffername);
1464         sprintf(buffername, "graph%04u", get_execution_number());
1465         dumpGraph(buffername);
1466 #endif
1467
1468         model_print("Execution trace %d:", get_execution_number());
1469         if (scheduler->all_threads_sleeping())
1470                 model_print(" SLEEP-SET REDUNDANT");
1471         if (have_bug_reports())
1472                 model_print(" DETECTED BUG(S)");
1473
1474         model_print("\n");
1475
1476         print_list(&action_trace);
1477         model_print("\n");
1478
1479 }
1480
1481 void ModelExecution::print_tail()
1482 {
1483         model_print("Execution trace %d:\n", get_execution_number());
1484
1485         sllnode<ModelAction*> *it;
1486
1487         model_print("------------------------------------------------------------------------------------\n");
1488         model_print("#    t    Action type     MO       Location         Value               Rf  CV\n");
1489         model_print("------------------------------------------------------------------------------------\n");
1490
1491         unsigned int hash = 0;
1492
1493         int length = 25;
1494         int counter = 0;
1495         SnapList<ModelAction *> list;
1496         for (it = action_trace.end();it != NULL;it = it->getPrev()) {
1497                 if (counter > length)
1498                         break;
1499
1500                 ModelAction * act = it->getVal();
1501                 list.push_front(act);
1502                 counter++;
1503         }
1504
1505         for (it = list.begin();it != NULL;it=it->getNext()) {
1506                 const ModelAction *act = it->getVal();
1507                 if (act->get_seq_number() > 0)
1508                         act->print();
1509                 hash = hash^(hash<<3)^(it->getVal()->hash());
1510         }
1511         model_print("HASH %u\n", hash);
1512         model_print("------------------------------------------------------------------------------------\n");
1513 }
1514
1515 /**
1516  * Add a Thread to the system for the first time. Should only be called once
1517  * per thread.
1518  * @param t The Thread to add
1519  */
1520 void ModelExecution::add_thread(Thread *t)
1521 {
1522         unsigned int i = id_to_int(t->get_id());
1523         if (i >= thread_map.size())
1524                 thread_map.resize(i + 1);
1525         thread_map[i] = t;
1526         if (!t->is_model_thread())
1527                 scheduler->add_thread(t);
1528 }
1529
1530 /**
1531  * @brief Get a Thread reference by its ID
1532  * @param tid The Thread's ID
1533  * @return A Thread reference
1534  */
1535 Thread * ModelExecution::get_thread(thread_id_t tid) const
1536 {
1537         unsigned int i = id_to_int(tid);
1538         if (i < thread_map.size())
1539                 return thread_map[i];
1540         return NULL;
1541 }
1542
1543 /**
1544  * @brief Get a reference to the Thread in which a ModelAction was executed
1545  * @param act The ModelAction
1546  * @return A Thread reference
1547  */
1548 Thread * ModelExecution::get_thread(const ModelAction *act) const
1549 {
1550         return get_thread(act->get_tid());
1551 }
1552
1553 /**
1554  * @brief Get a Thread reference by its pthread ID
1555  * @param index The pthread's ID
1556  * @return A Thread reference
1557  */
1558 Thread * ModelExecution::get_pthread(pthread_t pid) {
1559         // pid 1 is reserved for the main thread, pthread ids should start from 2
1560         if (pid == 1)
1561                 return get_thread(pid);
1562
1563         union {
1564                 pthread_t p;
1565                 uint32_t v;
1566         } x;
1567         x.p = pid;
1568         uint32_t thread_id = x.v;
1569
1570         if (thread_id < pthread_counter + 1)
1571                 return pthread_map[thread_id];
1572         else
1573                 return NULL;
1574 }
1575
1576 /**
1577  * @brief Check if a Thread is currently enabled
1578  * @param t The Thread to check
1579  * @return True if the Thread is currently enabled
1580  */
1581 bool ModelExecution::is_enabled(Thread *t) const
1582 {
1583         return scheduler->is_enabled(t);
1584 }
1585
1586 /**
1587  * @brief Check if a Thread is currently enabled
1588  * @param tid The ID of the Thread to check
1589  * @return True if the Thread is currently enabled
1590  */
1591 bool ModelExecution::is_enabled(thread_id_t tid) const
1592 {
1593         return scheduler->is_enabled(tid);
1594 }
1595
1596 /**
1597  * @brief Select the next thread to execute based on the curren action
1598  *
1599  * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1600  * actions should be followed by the execution of their child thread. In either
1601  * case, the current action should determine the next thread schedule.
1602  *
1603  * @param curr The current action
1604  * @return The next thread to run, if the current action will determine this
1605  * selection; otherwise NULL
1606  */
1607 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1608 {
1609         /* Do not split atomic RMW */
1610         if (curr->is_rmwr())
1611                 return get_thread(curr);
1612         /* Follow CREATE with the created thread */
1613         /* which is not needed, because model.cc takes care of this */
1614         if (curr->get_type() == THREAD_CREATE)
1615                 return curr->get_thread_operand();
1616         if (curr->get_type() == PTHREAD_CREATE) {
1617                 return curr->get_thread_operand();
1618         }
1619         return NULL;
1620 }
1621
1622 /**
1623  * Takes the next step in the execution, if possible.
1624  * @param curr The current step to take
1625  * @return Returns the next Thread to run, if any; NULL if this execution
1626  * should terminate
1627  */
1628 Thread * ModelExecution::take_step(ModelAction *curr)
1629 {
1630         Thread *curr_thrd = get_thread(curr);
1631         ASSERT(curr_thrd->get_state() == THREAD_READY);
1632
1633         ASSERT(check_action_enabled(curr));     /* May have side effects? */
1634         curr = check_current_action(curr);
1635         ASSERT(curr);
1636
1637         /* Process this action in ModelHistory for records */
1638 #ifdef NEWFUZZER
1639         model->get_history()->process_action( curr, curr->get_tid() );
1640 #endif
1641         if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1642                 scheduler->remove_thread(curr_thrd);
1643
1644         return action_select_next_thread(curr);
1645 }
1646
1647 /** This method removes references to an Action before we delete it. */
1648
1649 void ModelExecution::removeAction(ModelAction *act) {
1650         {
1651                 action_trace.removeAction(act);
1652         }
1653         {
1654                 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1655                 (*vec)[act->get_tid()].removeAction(act);
1656         }
1657         if ((act->is_fence() && act->is_seqcst()) || act->is_unlock()) {
1658                 action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1659                 list->removeAction(act);
1660         } else if (act->is_wait()) {
1661                 void *mutex_loc = (void *) act->get_value();
1662                 get_safe_ptr_action(&obj_map, mutex_loc)->removeAction(act);
1663         } else if (act->is_free()) {
1664                 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1665                 (*vec)[act->get_tid()].removeAction(act);
1666
1667                 //Clear it from last_sc_map
1668                 if (obj_last_sc_map.get(act->get_location()) == act) {
1669                         obj_last_sc_map.remove(act->get_location());
1670                 }
1671
1672                 //Remove from Cyclegraph
1673                 mo_graph->freeAction(act);
1674         }
1675 }
1676
1677 /** Computes clock vector that all running threads have already synchronized to.  */
1678
1679 ClockVector * ModelExecution::computeMinimalCV() {
1680         ClockVector *cvmin = NULL;
1681         //Thread 0 isn't a real thread, so skip it..
1682         for(unsigned int i = 1;i < thread_map.size();i++) {
1683                 Thread * t = thread_map[i];
1684                 if (t->get_state() == THREAD_COMPLETED)
1685                         continue;
1686                 thread_id_t tid = int_to_id(i);
1687                 ClockVector * cv = get_cv(tid);
1688                 if (cvmin == NULL)
1689                         cvmin = new ClockVector(cv, NULL);
1690                 else
1691                         cvmin->minmerge(cv);
1692         }
1693         return cvmin;
1694 }
1695
1696
1697 /** Sometimes we need to remove an action that is the most recent in the thread.  This happens if it is mo before action in other threads.  In that case we need to create a replacement latest ModelAction */
1698
1699 void ModelExecution::fixupLastAct(ModelAction *act) {
1700         ModelAction *newact = new ModelAction(ATOMIC_NOP, std::memory_order_seq_cst, NULL, VALUE_NONE, get_thread(act->get_tid()));
1701         newact->set_seq_number(get_next_seq_num());
1702         newact->create_cv(act);
1703         newact->set_last_fence_release(act->get_last_fence_release());
1704         add_action_to_lists(newact, false);
1705 }
1706
1707 /** Compute which actions to free.  */
1708
1709 void ModelExecution::collectActions() {
1710         if (priv->used_sequence_numbers < params->traceminsize)
1711                 return;
1712
1713         //Compute minimal clock vector for all live threads
1714         ClockVector *cvmin = computeMinimalCV();
1715         SnapVector<CycleNode *> * queue = new SnapVector<CycleNode *>();
1716         modelclock_t maxtofree = priv->used_sequence_numbers - params->traceminsize;
1717
1718         //Next walk action trace...  When we hit an action, see if it is
1719         //invisible (e.g., earlier than the first before the minimum
1720         //clock for the thread...  if so erase it and all previous
1721         //actions in cyclegraph
1722         sllnode<ModelAction*> * it;
1723         for (it = action_trace.begin();it != NULL;it=it->getNext()) {
1724                 ModelAction *act = it->getVal();
1725                 modelclock_t actseq = act->get_seq_number();
1726
1727                 //See if we are done
1728                 if (actseq > maxtofree)
1729                         break;
1730
1731                 thread_id_t act_tid = act->get_tid();
1732                 modelclock_t tid_clock = cvmin->getClock(act_tid);
1733
1734                 //Free if it is invisible or we have set a flag to remove visible actions.
1735                 if (actseq <= tid_clock || params->removevisible) {
1736                         ModelAction * write;
1737                         if (act->is_write()) {
1738                                 write = act;
1739                         } else if (act->is_read()) {
1740                                 write = act->get_reads_from();
1741                         } else
1742                                 continue;
1743
1744                         //Mark everything earlier in MO graph to be freed
1745                         CycleNode * cn = mo_graph->getNode_noCreate(write);
1746                         if (cn != NULL) {
1747                                 queue->push_back(cn);
1748                                 while(!queue->empty()) {
1749                                         CycleNode * node = queue->back();
1750                                         queue->pop_back();
1751                                         for(unsigned int i=0;i<node->getNumInEdges();i++) {
1752                                                 CycleNode * prevnode = node->getInEdge(i);
1753                                                 ModelAction * prevact = prevnode->getAction();
1754                                                 if (prevact->get_type() != READY_FREE) {
1755                                                         prevact->set_free();
1756                                                         queue->push_back(prevnode);
1757                                                 }
1758                                         }
1759                                 }
1760                         }
1761                 }
1762         }
1763
1764         //We may need to remove read actions in the window we don't delete to preserve correctness.
1765
1766         for (sllnode<ModelAction*> * it2 = action_trace.end();it2 != it;) {
1767                 ModelAction *act = it2->getVal();
1768                 //Do iteration early in case we delete the act
1769                 it2=it2->getPrev();
1770                 bool islastact = false;
1771                 ModelAction *lastact = get_last_action(act->get_tid());
1772                 if (act == lastact) {
1773                         Thread * th = get_thread(act);
1774                         islastact = !th->is_complete();
1775                 }
1776
1777                 if (act->is_read()) {
1778                         if (act->get_reads_from()->is_free()) {
1779                                 if (act->is_rmw()) {
1780                                         //Weaken a RMW from a freed store to a write
1781                                         act->set_type(ATOMIC_WRITE);
1782                                 } else {
1783                                         removeAction(act);
1784                                         if (islastact) {
1785                                                 fixupLastAct(act);
1786                                         }
1787
1788                                         delete act;
1789                                         continue;
1790                                 }
1791                         }
1792                 }
1793                 //If we don't delete the action, we should remove references to release fences
1794
1795                 const ModelAction *rel_fence =act->get_last_fence_release();
1796                 if (rel_fence != NULL) {
1797                         modelclock_t relfenceseq = rel_fence->get_seq_number();
1798                         thread_id_t relfence_tid = rel_fence->get_tid();
1799                         modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1800                         //Remove references to irrelevant release fences
1801                         if (relfenceseq <= tid_clock)
1802                                 act->set_last_fence_release(NULL);
1803                 }
1804         }
1805         //Now we are in the window of old actions that we remove if possible
1806         for (;it != NULL;) {
1807                 ModelAction *act = it->getVal();
1808                 //Do iteration early since we may delete node...
1809                 it=it->getPrev();
1810                 bool islastact = false;
1811                 ModelAction *lastact = get_last_action(act->get_tid());
1812                 if (act == lastact) {
1813                         Thread * th = get_thread(act);
1814                         islastact = !th->is_complete();
1815                 }
1816
1817                 if (act->is_read()) {
1818                         if (act->get_reads_from()->is_free()) {
1819                                 if (act->is_rmw()) {
1820                                         act->set_type(ATOMIC_WRITE);
1821                                 } else {
1822                                         removeAction(act);
1823                                         if (islastact) {
1824                                                 fixupLastAct(act);
1825                                         }
1826                                         delete act;
1827                                         continue;
1828                                 }
1829                         }
1830                 } else if (act->is_free()) {
1831                         removeAction(act);
1832                         if (islastact) {
1833                                 fixupLastAct(act);
1834                         }
1835                         delete act;
1836                         continue;
1837                 } else if (act->is_write()) {
1838                         //Do nothing with write that hasn't been marked to be freed
1839                 } else if (islastact) {
1840                         //Keep the last action for non-read/write actions
1841                 } else if (act->is_fence()) {
1842                         //Note that acquire fences can always be safely
1843                         //removed, but could incur extra overheads in
1844                         //traversals.  Removing them before the cvmin seems
1845                         //like a good compromise.
1846
1847                         //Release fences before the cvmin don't do anything
1848                         //because everyone has already synchronized.
1849
1850                         //Sequentially fences before cvmin are redundant
1851                         //because happens-before will enforce same
1852                         //orderings.
1853
1854                         modelclock_t actseq = act->get_seq_number();
1855                         thread_id_t act_tid = act->get_tid();
1856                         modelclock_t tid_clock = cvmin->getClock(act_tid);
1857                         if (actseq <= tid_clock) {
1858                                 removeAction(act);
1859                                 // Remove reference to act from thrd_last_fence_release
1860                                 int thread_id = id_to_int( act->get_tid() );
1861                                 if (thrd_last_fence_release[thread_id] == act) {
1862                                         thrd_last_fence_release[thread_id] = NULL;
1863                                 }
1864                                 delete act;
1865                                 continue;
1866                         }
1867                 } else {
1868                         //need to deal with lock, annotation, wait, notify, thread create, start, join, yield, finish, nops
1869                         //lock, notify thread create, thread finish, yield, finish are dead as soon as they are in the trace
1870                         //need to keep most recent unlock/wait for each lock
1871                         if(act->is_unlock() || act->is_wait()) {
1872                                 ModelAction * lastlock = get_last_unlock(act);
1873                                 if (lastlock != act) {
1874                                         removeAction(act);
1875                                         delete act;
1876                                         continue;
1877                                 }
1878                         } else if (act->is_create()) {
1879                                 if (act->get_thread_operand()->is_complete()) {
1880                                         removeAction(act);
1881                                         delete act;
1882                                         continue;
1883                                 }
1884                         } else {
1885                                 removeAction(act);
1886                                 delete act;
1887                                 continue;
1888                         }
1889                 }
1890
1891                 //If we don't delete the action, we should remove references to release fences
1892                 const ModelAction *rel_fence =act->get_last_fence_release();
1893                 if (rel_fence != NULL) {
1894                         modelclock_t relfenceseq = rel_fence->get_seq_number();
1895                         thread_id_t relfence_tid = rel_fence->get_tid();
1896                         modelclock_t tid_clock = cvmin->getClock(relfence_tid);
1897                         //Remove references to irrelevant release fences
1898                         if (relfenceseq <= tid_clock)
1899                                 act->set_last_fence_release(NULL);
1900                 }
1901         }
1902
1903         delete cvmin;
1904         delete queue;
1905 }
1906
1907 Fuzzer * ModelExecution::getFuzzer() {
1908         return fuzzer;
1909 }