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