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