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