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