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