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