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