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                 bad_synchronization(false),
  32                 asserted(false)
  33         { }
  34
  35         ~model_snapshot_members() {
  36                 for (unsigned int i = 0;i < bugs.size();i++)
  37                         delete bugs[i];
  38                 bugs.clear();
  39         }
  40
  41         unsigned int next_thread_id;
  42         modelclock_t used_sequence_numbers;
  43         SnapVector<bug_message *> bugs;
  44         /** @brief Incorrectly-ordered synchronization was made */
  45         bool bad_synchronization;
  46         bool asserted;
  47
  48         SNAPSHOTALLOC
  49 };
  50
  51 /** @brief Constructor */
  52 ModelExecution::ModelExecution(ModelChecker *m, Scheduler *scheduler) :
  53         model(m),
  54         params(NULL),
  55         scheduler(scheduler),
  56         action_trace(),
  57         thread_map(2),  /* We'll always need at least 2 threads */
  58         pthread_map(0),
  59         pthread_counter(1),
  60         obj_map(),
  61         condvar_waiters_map(),
  62         obj_thrd_map(),
  63         mutex_map(),
  64         thrd_last_action(1),
  65         thrd_last_fence_release(),
  66         priv(new struct model_snapshot_members ()),
  67         mo_graph(new CycleGraph()),
  68         fuzzer(new NewFuzzer()),
  69         thrd_func_list(),
  70         thrd_func_act_lists(),
  71         isfinished(false)
  72 {
  73         /* Initialize a model-checker thread, for special ModelActions */
  74         model_thread = new Thread(get_next_id());
  75         add_thread(model_thread);
  76         scheduler->register_engine(this);
  77         fuzzer->register_engine(m->get_history(), this);
  78 }
  79
  80 /** @brief Destructor */
  81 ModelExecution::~ModelExecution()
  82 {
  83         for (unsigned int i = 0;i < get_num_threads();i++)
  84                 delete get_thread(int_to_id(i));
  85
  86         delete mo_graph;
  87         delete priv;
  88 }
  89
  90 int ModelExecution::get_execution_number() const
  91 {
  92         return model->get_execution_number();
  93 }
  94
  95 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
  96 {
  97         action_list_t *tmp = hash->get(ptr);
  98         if (tmp == NULL) {
  99                 tmp = new action_list_t();
 100                 hash->put(ptr, tmp);
 101         }
 102         return tmp;
 103 }
 104
 105 static SnapVector<action_list_t> * get_safe_ptr_vect_action(HashTable<const void *, SnapVector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
 106 {
 107         SnapVector<action_list_t> *tmp = hash->get(ptr);
 108         if (tmp == NULL) {
 109                 tmp = new SnapVector<action_list_t>();
 110                 hash->put(ptr, tmp);
 111         }
 112         return tmp;
 113 }
 114
 115 /** @return a thread ID for a new Thread */
 116 thread_id_t ModelExecution::get_next_id()
 117 {
 118         return priv->next_thread_id++;
 119 }
 120
 121 /** @return the number of user threads created during this execution */
 122 unsigned int ModelExecution::get_num_threads() const
 123 {
 124         return priv->next_thread_id;
 125 }
 126
 127 /** @return a sequence number for a new ModelAction */
 128 modelclock_t ModelExecution::get_next_seq_num()
 129 {
 130         return ++priv->used_sequence_numbers;
 131 }
 132
 133 /** Restore the last used sequence number when actions of a thread are postponed by Fuzzer */
 134 void ModelExecution::restore_last_seq_num()
 135 {
 136         priv->used_sequence_numbers--;
 137 }
 138
 139 /**
 140  * @brief Should the current action wake up a given thread?
 141  *
 142  * @param curr The current action
 143  * @param thread The thread that we might wake up
 144  * @return True, if we should wake up the sleeping thread; false otherwise
 145  */
 146 bool ModelExecution::should_wake_up(const ModelAction *curr, const Thread *thread) const
 147 {
 148         const ModelAction *asleep = thread->get_pending();
 149         /* Don't allow partial RMW to wake anyone up */
 150         if (curr->is_rmwr())
 151                 return false;
 152         /* Synchronizing actions may have been backtracked */
 153         if (asleep->could_synchronize_with(curr))
 154                 return true;
 155         /* All acquire/release fences and fence-acquire/store-release */
 156         if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
 157                 return true;
 158         /* Fence-release + store can awake load-acquire on the same location */
 159         if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
 160                 ModelAction *fence_release = get_last_fence_release(curr->get_tid());
 161                 if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
 162                         return true;
 163         }
 164         if (asleep->is_sleep()) {
 165                 if (fuzzer->shouldWake(asleep))
 166                         return true;
 167         }
 168
 169         return false;
 170 }
 171
 172 void ModelExecution::wake_up_sleeping_actions(ModelAction *curr)
 173 {
 174         for (unsigned int i = 0;i < get_num_threads();i++) {
 175                 Thread *thr = get_thread(int_to_id(i));
 176                 if (scheduler->is_sleep_set(thr)) {
 177                         if (should_wake_up(curr, thr))
 178                                 /* Remove this thread from sleep set */
 179                                 scheduler->remove_sleep(thr);
 180                 }
 181         }
 182 }
 183
 184 /** @brief Alert the model-checker that an incorrectly-ordered
 185  * synchronization was made */
 186 void ModelExecution::set_bad_synchronization()
 187 {
 188         priv->bad_synchronization = true;
 189 }
 190
 191 bool ModelExecution::assert_bug(const char *msg)
 192 {
 193         priv->bugs.push_back(new bug_message(msg));
 194
 195         if (isfeasibleprefix()) {
 196                 set_assert();
 197                 return true;
 198         }
 199         return false;
 200 }
 201
 202 /** @return True, if any bugs have been reported for this execution */
 203 bool ModelExecution::have_bug_reports() const
 204 {
 205         return priv->bugs.size() != 0;
 206 }
 207
 208 SnapVector<bug_message *> * ModelExecution::get_bugs() const
 209 {
 210         return &priv->bugs;
 211 }
 212
 213 /**
 214  * Check whether the current trace has triggered an assertion which should halt
 215  * its execution.
 216  *
 217  * @return True, if the execution should be aborted; false otherwise
 218  */
 219 bool ModelExecution::has_asserted() const
 220 {
 221         return priv->asserted;
 222 }
 223
 224 /**
 225  * Trigger a trace assertion which should cause this execution to be halted.
 226  * This can be due to a detected bug or due to an infeasibility that should
 227  * halt ASAP.
 228  */
 229 void ModelExecution::set_assert()
 230 {
 231         priv->asserted = true;
 232 }
 233
 234 /**
 235  * Check if we are in a deadlock. Should only be called at the end of an
 236  * execution, although it should not give false positives in the middle of an
 237  * execution (there should be some ENABLED thread).
 238  *
 239  * @return True if program is in a deadlock; false otherwise
 240  */
 241 bool ModelExecution::is_deadlocked() const
 242 {
 243         bool blocking_threads = false;
 244         for (unsigned int i = 0;i < get_num_threads();i++) {
 245                 thread_id_t tid = int_to_id(i);
 246                 if (is_enabled(tid))
 247                         return false;
 248                 Thread *t = get_thread(tid);
 249                 if (!t->is_model_thread() && t->get_pending())
 250                         blocking_threads = true;
 251         }
 252         return blocking_threads;
 253 }
 254
 255 /**
 256  * Check if this is a complete execution. That is, have all thread completed
 257  * execution (rather than exiting because sleep sets have forced a redundant
 258  * execution).
 259  *
 260  * @return True if the execution is complete.
 261  */
 262 bool ModelExecution::is_complete_execution() const
 263 {
 264         for (unsigned int i = 0;i < get_num_threads();i++)
 265                 if (is_enabled(int_to_id(i)))
 266                         return false;
 267         return true;
 268 }
 269
 270 ModelAction * ModelExecution::convertNonAtomicStore(void * location) {
 271         uint64_t value = *((const uint64_t *) location);
 272         modelclock_t storeclock;
 273         thread_id_t storethread;
 274         getStoreThreadAndClock(location, &storethread, &storeclock);
 275         setAtomicStoreFlag(location);
 276         ModelAction * act = new ModelAction(NONATOMIC_WRITE, memory_order_relaxed, location, value, get_thread(storethread));
 277         act->set_seq_number(storeclock);
 278         add_normal_write_to_lists(act);
 279         add_write_to_lists(act);
 280         w_modification_order(act);
 281         model->get_history()->process_action(act, act->get_tid());
 282         return act;
 283 }
 284
 285 /**
 286  * Processes a read model action.
 287  * @param curr is the read model action to process.
 288  * @param rf_set is the set of model actions we can possibly read from
 289  * @return True if processing this read updates the mo_graph.
 290  */
 291 bool ModelExecution::process_read(ModelAction *curr, SnapVector<ModelAction *> * rf_set)
 292 {
 293         SnapVector<const ModelAction *> * priorset = new SnapVector<const ModelAction *>();
 294         bool hasnonatomicstore = hasNonAtomicStore(curr->get_location());
 295         if (hasnonatomicstore) {
 296                 ModelAction * nonatomicstore = convertNonAtomicStore(curr->get_location());
 297                 rf_set->push_back(nonatomicstore);
 298         }
 299
 300         while(true) {
 301                 int index = fuzzer->selectWrite(curr, rf_set);
 302                 if (index == -1)        // no feasible write exists
 303                         return false;
 304
 305                 ModelAction *rf = (*rf_set)[index];
 306
 307                 ASSERT(rf);
 308                 bool canprune = false;
 309                 if (r_modification_order(curr, rf, priorset, &canprune)) {
 310                         for(unsigned int i=0;i<priorset->size();i++) {
 311                                 mo_graph->addEdge((*priorset)[i], rf);
 312                         }
 313                         read_from(curr, rf);
 314                         get_thread(curr)->set_return_value(curr->get_return_value());
 315                         delete priorset;
 316                         if (canprune && curr->get_type() == ATOMIC_READ) {
 317                                 int tid = id_to_int(curr->get_tid());
 318                                 (*obj_thrd_map.get(curr->get_location()))[tid].pop_back();
 319                         }
 320                         return true;
 321                 }
 322                 priorset->clear();
 323                 (*rf_set)[index] = rf_set->back();
 324                 rf_set->pop_back();
 325         }
 326 }
 327
 328 /**
 329  * Processes a lock, trylock, or unlock model action.  @param curr is
 330  * the read model action to process.
 331  *
 332  * The try lock operation checks whether the lock is taken.  If not,
 333  * it falls to the normal lock operation case.  If so, it returns
 334  * fail.
 335  *
 336  * The lock operation has already been checked that it is enabled, so
 337  * it just grabs the lock and synchronizes with the previous unlock.
 338  *
 339  * The unlock operation has to re-enable all of the threads that are
 340  * waiting on the lock.
 341  *
 342  * @return True if synchronization was updated; false otherwise
 343  */
 344 bool ModelExecution::process_mutex(ModelAction *curr)
 345 {
 346         cdsc::mutex *mutex = curr->get_mutex();
 347         struct cdsc::mutex_state *state = NULL;
 348
 349         if (mutex)
 350                 state = mutex->get_state();
 351
 352         switch (curr->get_type()) {
 353         case ATOMIC_TRYLOCK: {
 354                 bool success = !state->locked;
 355                 curr->set_try_lock(success);
 356                 if (!success) {
 357                         get_thread(curr)->set_return_value(0);
 358                         break;
 359                 }
 360                 get_thread(curr)->set_return_value(1);
 361         }
 362         //otherwise fall into the lock case
 363         case ATOMIC_LOCK: {
 364                 //TODO: FIND SOME BETTER WAY TO CHECK LOCK INITIALIZED OR NOT
 365                 //if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
 366                 //      assert_bug("Lock access before initialization");
 367                 state->locked = get_thread(curr);
 368                 ModelAction *unlock = get_last_unlock(curr);
 369                 //synchronize with the previous unlock statement
 370                 if (unlock != NULL) {
 371                         synchronize(unlock, curr);
 372                         return true;
 373                 }
 374                 break;
 375         }
 376         case ATOMIC_WAIT:
 377         case ATOMIC_UNLOCK: {
 378                 //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...
 379
 380                 /* wake up the other threads */
 381                 for (unsigned int i = 0;i < get_num_threads();i++) {
 382                         Thread *t = get_thread(int_to_id(i));
 383                         Thread *curr_thrd = get_thread(curr);
 384                         if (t->waiting_on() == curr_thrd && t->get_pending()->is_lock())
 385                                 scheduler->wake(t);
 386                 }
 387
 388                 /* unlock the lock - after checking who was waiting on it */
 389                 state->locked = NULL;
 390
 391                 if (!curr->is_wait())
 392                         break;/* The rest is only for ATOMIC_WAIT */
 393
 394                 break;
 395         }
 396         case ATOMIC_NOTIFY_ALL: {
 397                 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
 398                 //activate all the waiting threads
 399                 for (sllnode<ModelAction *> * rit = waiters->begin();rit != NULL;rit=rit->getNext()) {
 400                         scheduler->wake(get_thread(rit->getVal()));
 401                 }
 402                 waiters->clear();
 403                 break;
 404         }
 405         case ATOMIC_NOTIFY_ONE: {
 406                 action_list_t *waiters = get_safe_ptr_action(&condvar_waiters_map, curr->get_location());
 407                 if (waiters->size() != 0) {
 408                         Thread * thread = fuzzer->selectNotify(waiters);
 409                         scheduler->wake(thread);
 410                 }
 411                 break;
 412         }
 413
 414         default:
 415                 ASSERT(0);
 416         }
 417         return false;
 418 }
 419
 420 /**
 421  * Process a write ModelAction
 422  * @param curr The ModelAction to process
 423  * @return True if the mo_graph was updated or promises were resolved
 424  */
 425 void ModelExecution::process_write(ModelAction *curr)
 426 {
 427         w_modification_order(curr);
 428         get_thread(curr)->set_return_value(VALUE_NONE);
 429 }
 430
 431 /**
 432  * Process a fence ModelAction
 433  * @param curr The ModelAction to process
 434  * @return True if synchronization was updated
 435  */
 436 bool ModelExecution::process_fence(ModelAction *curr)
 437 {
 438         /*
 439          * fence-relaxed: no-op
 440          * fence-release: only log the occurence (not in this function), for
 441          *   use in later synchronization
 442          * fence-acquire (this function): search for hypothetical release
 443          *   sequences
 444          * fence-seq-cst: MO constraints formed in {r,w}_modification_order
 445          */
 446         bool updated = false;
 447         if (curr->is_acquire()) {
 448                 action_list_t *list = &action_trace;
 449                 sllnode<ModelAction *> * rit;
 450                 /* Find X : is_read(X) && X --sb-> curr */
 451                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
 452                         ModelAction *act = rit->getVal();
 453                         if (act == curr)
 454                                 continue;
 455                         if (act->get_tid() != curr->get_tid())
 456                                 continue;
 457                         /* Stop at the beginning of the thread */
 458                         if (act->is_thread_start())
 459                                 break;
 460                         /* Stop once we reach a prior fence-acquire */
 461                         if (act->is_fence() && act->is_acquire())
 462                                 break;
 463                         if (!act->is_read())
 464                                 continue;
 465                         /* read-acquire will find its own release sequences */
 466                         if (act->is_acquire())
 467                                 continue;
 468
 469                         /* Establish hypothetical release sequences */
 470                         ClockVector *cv = get_hb_from_write(act->get_reads_from());
 471                         if (cv != NULL && curr->get_cv()->merge(cv))
 472                                 updated = true;
 473                 }
 474         }
 475         return updated;
 476 }
 477
 478 /**
 479  * @brief Process the current action for thread-related activity
 480  *
 481  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
 482  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
 483  * synchronization, etc.  This function is a no-op for non-THREAD actions
 484  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
 485  *
 486  * @param curr The current action
 487  * @return True if synchronization was updated or a thread completed
 488  */
 489 void ModelExecution::process_thread_action(ModelAction *curr)
 490 {
 491         switch (curr->get_type()) {
 492         case THREAD_CREATE: {
 493                 thrd_t *thrd = (thrd_t *)curr->get_location();
 494                 struct thread_params *params = (struct thread_params *)curr->get_value();
 495                 Thread *th = new Thread(get_next_id(), thrd, params->func, params->arg, get_thread(curr));
 496                 curr->set_thread_operand(th);
 497                 add_thread(th);
 498                 th->set_creation(curr);
 499                 break;
 500         }
 501         case PTHREAD_CREATE: {
 502                 (*(uint32_t *)curr->get_location()) = pthread_counter++;
 503
 504                 struct pthread_params *params = (struct pthread_params *)curr->get_value();
 505                 Thread *th = new Thread(get_next_id(), NULL, params->func, params->arg, get_thread(curr));
 506                 curr->set_thread_operand(th);
 507                 add_thread(th);
 508                 th->set_creation(curr);
 509
 510                 if ( pthread_map.size() < pthread_counter )
 511                         pthread_map.resize( pthread_counter );
 512                 pthread_map[ pthread_counter-1 ] = th;
 513
 514                 break;
 515         }
 516         case THREAD_JOIN: {
 517                 Thread *blocking = curr->get_thread_operand();
 518                 ModelAction *act = get_last_action(blocking->get_id());
 519                 synchronize(act, curr);
 520                 break;
 521         }
 522         case PTHREAD_JOIN: {
 523                 Thread *blocking = curr->get_thread_operand();
 524                 ModelAction *act = get_last_action(blocking->get_id());
 525                 synchronize(act, curr);
 526                 break;  // WL: to be add (modified)
 527         }
 528
 529         case THREADONLY_FINISH:
 530         case THREAD_FINISH: {
 531                 Thread *th = get_thread(curr);
 532                 if (curr->get_type() == THREAD_FINISH &&
 533                                 th == model->getInitThread()) {
 534                         th->complete();
 535                         setFinished();
 536                         break;
 537                 }
 538
 539                 /* Wake up any joining threads */
 540                 for (unsigned int i = 0;i < get_num_threads();i++) {
 541                         Thread *waiting = get_thread(int_to_id(i));
 542                         if (waiting->waiting_on() == th &&
 543                                         waiting->get_pending()->is_thread_join())
 544                                 scheduler->wake(waiting);
 545                 }
 546                 th->complete();
 547                 break;
 548         }
 549         case THREAD_START: {
 550                 break;
 551         }
 552         default:
 553                 break;
 554         }
 555 }
 556
 557 /**
 558  * Initialize the current action by performing one or more of the following
 559  * actions, as appropriate: merging RMWR and RMWC/RMW actions,
 560  * manipulating backtracking sets, allocating and
 561  * initializing clock vectors, and computing the promises to fulfill.
 562  *
 563  * @param curr The current action, as passed from the user context; may be
 564  * freed/invalidated after the execution of this function, with a different
 565  * action "returned" its place (pass-by-reference)
 566  * @return True if curr is a newly-explored action; false otherwise
 567  */
 568 bool ModelExecution::initialize_curr_action(ModelAction **curr)
 569 {
 570         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
 571                 ModelAction *newcurr = process_rmw(*curr);
 572                 delete *curr;
 573
 574                 *curr = newcurr;
 575                 return false;
 576         } else {
 577                 ModelAction *newcurr = *curr;
 578
 579                 newcurr->set_seq_number(get_next_seq_num());
 580                 /* Always compute new clock vector */
 581                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 582
 583                 /* Assign most recent release fence */
 584                 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
 585
 586                 return true;    /* This was a new ModelAction */
 587         }
 588 }
 589
 590 /**
 591  * @brief Establish reads-from relation between two actions
 592  *
 593  * Perform basic operations involved with establishing a concrete rf relation,
 594  * including setting the ModelAction data and checking for release sequences.
 595  *
 596  * @param act The action that is reading (must be a read)
 597  * @param rf The action from which we are reading (must be a write)
 598  *
 599  * @return True if this read established synchronization
 600  */
 601
 602 void ModelExecution::read_from(ModelAction *act, ModelAction *rf)
 603 {
 604         ASSERT(rf);
 605         ASSERT(rf->is_write());
 606
 607         act->set_read_from(rf);
 608         if (act->is_acquire()) {
 609                 ClockVector *cv = get_hb_from_write(rf);
 610                 if (cv == NULL)
 611                         return;
 612                 act->get_cv()->merge(cv);
 613         }
 614 }
 615
 616 /**
 617  * @brief Synchronizes two actions
 618  *
 619  * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
 620  * This function performs the synchronization as well as providing other hooks
 621  * for other checks along with synchronization.
 622  *
 623  * @param first The left-hand side of the synchronizes-with relation
 624  * @param second The right-hand side of the synchronizes-with relation
 625  * @return True if the synchronization was successful (i.e., was consistent
 626  * with the execution order); false otherwise
 627  */
 628 bool ModelExecution::synchronize(const ModelAction *first, ModelAction *second)
 629 {
 630         if (*second < *first) {
 631                 set_bad_synchronization();
 632                 return false;
 633         }
 634         return second->synchronize_with(first);
 635 }
 636
 637 /**
 638  * @brief Check whether a model action is enabled.
 639  *
 640  * Checks whether an operation would be successful (i.e., is a lock already
 641  * locked, or is the joined thread already complete).
 642  *
 643  * For yield-blocking, yields are never enabled.
 644  *
 645  * @param curr is the ModelAction to check whether it is enabled.
 646  * @return a bool that indicates whether the action is enabled.
 647  */
 648 bool ModelExecution::check_action_enabled(ModelAction *curr) {
 649         if (curr->is_lock()) {
 650                 cdsc::mutex *lock = curr->get_mutex();
 651                 struct cdsc::mutex_state *state = lock->get_state();
 652                 if (state->locked)
 653                         return false;
 654         } else if (curr->is_thread_join()) {
 655                 Thread *blocking = curr->get_thread_operand();
 656                 if (!blocking->is_complete()) {
 657                         return false;
 658                 }
 659         } else if (curr->is_sleep()) {
 660                 if (!fuzzer->shouldSleep(curr))
 661                         return false;
 662         }
 663
 664         return true;
 665 }
 666
 667 /**
 668  * This is the heart of the model checker routine. It performs model-checking
 669  * actions corresponding to a given "current action." Among other processes, it
 670  * calculates reads-from relationships, updates synchronization clock vectors,
 671  * forms a memory_order constraints graph, and handles replay/backtrack
 672  * execution when running permutations of previously-observed executions.
 673  *
 674  * @param curr The current action to process
 675  * @return The ModelAction that is actually executed; may be different than
 676  * curr
 677  */
 678 ModelAction * ModelExecution::check_current_action(ModelAction *curr)
 679 {
 680         ASSERT(curr);
 681         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
 682         bool newly_explored = initialize_curr_action(&curr);
 683
 684         DBG();
 685
 686         wake_up_sleeping_actions(curr);
 687
 688         /* Add uninitialized actions to lists */
 689         if (!second_part_of_rmw && curr->get_type() != NOOP)
 690                 add_uninit_action_to_lists(curr);
 691
 692         SnapVector<ModelAction *> * rf_set = NULL;
 693         /* Build may_read_from set for newly-created actions */
 694         if (newly_explored && curr->is_read())
 695                 rf_set = build_may_read_from(curr);
 696
 697         if (curr->is_read() && !second_part_of_rmw) {
 698                 bool success = process_read(curr, rf_set);
 699                 delete rf_set;
 700                 if (!success)
 701                         return curr;    // Do not add action to lists
 702         } else
 703                 ASSERT(rf_set == NULL);
 704
 705         /* Add the action to lists */
 706         if (!second_part_of_rmw && curr->get_type() != NOOP)
 707                 add_action_to_lists(curr);
 708
 709         if (curr->is_write())
 710                 add_write_to_lists(curr);
 711
 712         process_thread_action(curr);
 713
 714         if (curr->is_write())
 715                 process_write(curr);
 716
 717         if (curr->is_fence())
 718                 process_fence(curr);
 719
 720         if (curr->is_mutex_op())
 721                 process_mutex(curr);
 722
 723         return curr;
 724 }
 725
 726 /**
 727  * This is the strongest feasibility check available.
 728  * @return whether the current trace (partial or complete) must be a prefix of
 729  * a feasible trace.
 730  */
 731 bool ModelExecution::isfeasibleprefix() const
 732 {
 733         return !is_infeasible();
 734 }
 735
 736 /**
 737  * Print disagnostic information about an infeasible execution
 738  * @param prefix A string to prefix the output with; if NULL, then a default
 739  * message prefix will be provided
 740  */
 741 void ModelExecution::print_infeasibility(const char *prefix) const
 742 {
 743         char buf[100];
 744         char *ptr = buf;
 745         if (priv->bad_synchronization)
 746                 ptr += sprintf(ptr, "[bad sw ordering]");
 747         if (ptr != buf)
 748                 model_print("%s: %s", prefix ? prefix : "Infeasible", buf);
 749 }
 750
 751 /**
 752  * Check if the current partial trace is infeasible. Does not check any
 753  * end-of-execution flags, which might rule out the execution. Thus, this is
 754  * useful only for ruling an execution as infeasible.
 755  * @return whether the current partial trace is infeasible.
 756  */
 757 bool ModelExecution::is_infeasible() const
 758 {
 759         return priv->bad_synchronization;
 760 }
 761
 762 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 763 ModelAction * ModelExecution::process_rmw(ModelAction *act) {
 764         ModelAction *lastread = get_last_action(act->get_tid());
 765         lastread->process_rmw(act);
 766         if (act->is_rmw()) {
 767                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
 768         }
 769         return lastread;
 770 }
 771
 772 /**
 773  * @brief Updates the mo_graph with the constraints imposed from the current
 774  * read.
 775  *
 776  * Basic idea is the following: Go through each other thread and find
 777  * the last action that happened before our read.  Two cases:
 778  *
 779  * -# The action is a write: that write must either occur before
 780  * the write we read from or be the write we read from.
 781  * -# The action is a read: the write that that action read from
 782  * must occur before the write we read from or be the same write.
 783  *
 784  * @param curr The current action. Must be a read.
 785  * @param rf The ModelAction or Promise that curr reads from. Must be a write.
 786  * @return True if modification order edges were added; false otherwise
 787  */
 788
 789 bool ModelExecution::r_modification_order(ModelAction *curr, const ModelAction *rf, SnapVector<const ModelAction *> * priorset, bool * canprune)
 790 {
 791         SnapVector<action_list_t> *thrd_lists = obj_thrd_map.get(curr->get_location());
 792         unsigned int i;
 793         ASSERT(curr->is_read());
 794
 795         /* Last SC fence in the current thread */
 796         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
 797
 798         int tid = curr->get_tid();
 799         ModelAction *prev_same_thread = NULL;
 800         /* Iterate over all threads */
 801         for (i = 0;i < thrd_lists->size();i++, tid = (((unsigned int)(tid+1)) == thrd_lists->size()) ? 0 : tid + 1) {
 802                 /* Last SC fence in thread tid */
 803                 ModelAction *last_sc_fence_thread_local = NULL;
 804                 if (i != 0)
 805                         last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(tid), NULL);
 806
 807                 /* Last SC fence in thread tid, before last SC fence in current thread */
 808                 ModelAction *last_sc_fence_thread_before = NULL;
 809                 if (last_sc_fence_local)
 810                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(tid), last_sc_fence_local);
 811
 812                 //Only need to iterate if either hb has changed for thread in question or SC fence after last operation...
 813                 if (prev_same_thread != NULL &&
 814                                 (prev_same_thread->get_cv()->getClock(tid) == curr->get_cv()->getClock(tid)) &&
 815                                 (last_sc_fence_thread_local == NULL || *last_sc_fence_thread_local < *prev_same_thread)) {
 816                         continue;
 817                 }
 818
 819                 /* Iterate over actions in thread, starting from most recent */
 820                 action_list_t *list = &(*thrd_lists)[tid];
 821                 sllnode<ModelAction *> * rit;
 822                 for (rit = list->end();rit != NULL;rit=rit->getPrev()) {
 823                         ModelAction *act = rit->getVal();
 824
 825                         /* Skip curr */
 826                         if (act == curr)
 827                                 continue;
 828                         /* Don't want to add reflexive edges on 'rf' */
 829                         if (act->equals(rf)) {
 830                                 if (act->happens_before(curr))
 831                                         break;
 832                                 else
 833                                         continue;
 834                         }
 835
 836                         if (act->is_write()) {
 837                                 /* C++, Section 29.3 statement 5 */
 838                                 if (curr->is_seqcst() && last_sc_fence_thread_local &&
 839                                                 *act < *last_sc_fence_thread_local) {
 840                                         if (mo_graph->checkReachable(rf, act))
 841                                                 return false;
 842                                         priorset->push_back(act);
 843                                         break;
 844                                 }
 845                                 /* C++, Section 29.3 statement 4 */
 846                                 else if (act->is_seqcst() && last_sc_fence_local &&
 847                                                                  *act < *last_sc_fence_local) {
 848                                         if (mo_graph->checkReachable(rf, act))
 849                                                 return false;
 850                                         priorset->push_back(act);
 851                                         break;
 852                                 }
 853                                 /* C++, Section 29.3 statement 6 */
 854                                 else if (last_sc_fence_thread_before &&
 855                                                                  *act < *last_sc_fence_thread_before) {
 856                                         if (mo_graph->checkReachable(rf, act))
 857                                                 return false;
 858                                         priorset->push_back(act);
 859                                         break;
 860                                 }
 861                         }
 862
 863                         /*
 864                          * Include at most one act per-thread that "happens
 865                          * before" curr
 866                          */
 867                         if (act->happens_before(curr)) {
 868                                 if (i==0) {
 869                                         if (last_sc_fence_local == NULL ||
 870                                                         (*last_sc_fence_local < *act)) {
 871                                                 prev_same_thread = act;
 872                                         }
 873                                 }
 874                                 if (act->is_write()) {
 875                                         if (mo_graph->checkReachable(rf, act))
 876                                                 return false;
 877                                         priorset->push_back(act);
 878                                 } else {
 879                                         const ModelAction *prevrf = act->get_reads_from();
 880                                         if (!prevrf->equals(rf)) {
 881                                                 if (mo_graph->checkReachable(rf, prevrf))
 882                                                         return false;
 883                                                 priorset->push_back(prevrf);
 884                                         } else {
 885                                                 if (act->get_tid() == curr->get_tid()) {
 886                                                         //Can prune curr from obj list
 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         action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1115         if (list->empty() && act->is_atomic_var()) {
1116                 uninit = get_uninitialized_action(act);
1117                 uninit_id = id_to_int(uninit->get_tid());
1118                 list->push_front(uninit);
1119                 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_wr_thrd_map, act->get_location());
1120                 if ((int)vec->size() <= uninit_id) {
1121                         int oldsize = (int) vec->size();
1122                         vec->resize(uninit_id + 1);
1123                         for(int i = oldsize; i < uninit_id + 1; i++) {
1124                                 new (&(*vec)[i]) action_list_t();
1125                         }
1126                 }
1127                 (*vec)[uninit_id].push_front(uninit);
1128         }
1129
1130         // Update action trace, a total order of all actions
1131         if (uninit)
1132                 action_trace.push_front(uninit);
1133
1134         // Update obj_thrd_map, a per location, per thread, order of actions
1135         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1136         if ((int)vec->size() <= tid) {
1137                 uint oldsize = vec->size();
1138                 vec->resize(priv->next_thread_id);
1139                 for(uint i = oldsize; i < priv->next_thread_id; i++)
1140                         new (&(*vec)[i]) action_list_t();
1141         }
1142         if (uninit)
1143                 (*vec)[uninit_id].push_front(uninit);
1144
1145         // Update thrd_last_action, the last action taken by each thrad
1146         if ((int)thrd_last_action.size() <= tid)
1147                 thrd_last_action.resize(get_num_threads());
1148         if (uninit)
1149                 thrd_last_action[uninit_id] = uninit;
1150 }
1151
1152
1153 /**
1154  * Performs various bookkeeping operations for the current ModelAction. For
1155  * instance, adds action to the per-object, per-thread action vector and to the
1156  * action trace list of all thread actions.
1157  *
1158  * @param act is the ModelAction to add.
1159  */
1160 void ModelExecution::add_action_to_lists(ModelAction *act)
1161 {
1162         int tid = id_to_int(act->get_tid());
1163         action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1164         list->push_back(act);
1165
1166         // Update action trace, a total order of all actions
1167         action_trace.push_back(act);
1168
1169         // Update obj_thrd_map, a per location, per thread, order of actions
1170         SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, act->get_location());
1171         if ((int)vec->size() <= tid) {
1172                 uint oldsize = vec->size();
1173                 vec->resize(priv->next_thread_id);
1174                 for(uint i = oldsize; i < priv->next_thread_id; i++)
1175                         new (&(*vec)[i]) action_list_t();
1176         }
1177         (*vec)[tid].push_back(act);
1178
1179         // Update thrd_last_action, the last action taken by each thrad
1180         if ((int)thrd_last_action.size() <= tid)
1181                 thrd_last_action.resize(get_num_threads());
1182         thrd_last_action[tid] = act;
1183
1184         // Update thrd_last_fence_release, the last release fence taken by each thread
1185         if (act->is_fence() && act->is_release()) {
1186                 if ((int)thrd_last_fence_release.size() <= tid)
1187                         thrd_last_fence_release.resize(get_num_threads());
1188                 thrd_last_fence_release[tid] = act;
1189         }
1190
1191         if (act->is_wait()) {
1192                 void *mutex_loc = (void *) act->get_value();
1193                 get_safe_ptr_action(&obj_map, mutex_loc)->push_back(act);
1194
1195                 SnapVector<action_list_t> *vec = get_safe_ptr_vect_action(&obj_thrd_map, mutex_loc);
1196                 if ((int)vec->size() <= tid) {
1197                         uint oldsize = vec->size();
1198                         vec->resize(priv->next_thread_id);
1199                         for(uint i = oldsize; i < priv->next_thread_id; i++)
1200                                 new (&(*vec)[i]) action_list_t();
1201                 }
1202                 (*vec)[tid].push_back(act);
1203         }
1204 }
1205
1206 void insertIntoActionList(action_list_t *list, ModelAction *act) {
1207         sllnode<ModelAction*> * rit = list->end();
1208         modelclock_t next_seq = act->get_seq_number();
1209         if (rit == NULL || (rit->getVal()->get_seq_number() == next_seq))
1210                 list->push_back(act);
1211         else {
1212                 for(;rit != NULL;rit=rit->getPrev()) {
1213                         if (rit->getVal()->get_seq_number() == next_seq) {
1214                                 list->insertAfter(rit, act);
1215                                 break;
1216                         }
1217                 }
1218         }
1219 }
1220
1221 void insertIntoActionListAndSetCV(action_list_t *list, ModelAction *act) {
1222         sllnode<ModelAction*> * rit = list->end();
1223         modelclock_t next_seq = act->get_seq_number();
1224         if (rit == NULL) {
1225                 act->create_cv(NULL);
1226         } else if (rit->getVal()->get_seq_number() == next_seq) {
1227                 act->create_cv(rit->getVal());
1228                 list->push_back(act);
1229         } else {
1230                 for(;rit != NULL;rit=rit->getPrev()) {
1231                         if (rit->getVal()->get_seq_number() == next_seq) {
1232                                 act->create_cv(rit->getVal());
1233                                 list->insertAfter(rit, act);
1234                                 break;
1235                         }
1236                 }
1237         }
1238 }
1239
1240 /**
1241  * Performs various bookkeeping operations for a normal write.  The
1242  * complication is that we are typically inserting a normal write
1243  * lazily, so we need to insert it into the middle of lists.
1244  *
1245  * @param act is the ModelAction to add.
1246  */
1247
1248 void ModelExecution::add_normal_write_to_lists(ModelAction *act)
1249 {
1250         int tid = id_to_int(act->get_tid());
1251         insertIntoActionListAndSetCV(&action_trace, act);
1252
1253         action_list_t *list = get_safe_ptr_action(&obj_map, act->get_location());
1254         insertIntoActionList(list, 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         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         (*vec)[tid].push_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 (isfeasibleprefix()) {
1573                 if (scheduler->all_threads_sleeping())
1574                         model_print(" SLEEP-SET REDUNDANT");
1575                 if (have_bug_reports())
1576                         model_print(" DETECTED BUG(S)");
1577         } else
1578                 print_infeasibility(" INFEASIBLE");
1579         model_print("\n");
1580
1581         print_list(&action_trace);
1582         model_print("\n");
1583
1584 }
1585
1586 /**
1587  * Add a Thread to the system for the first time. Should only be called once
1588  * per thread.
1589  * @param t The Thread to add
1590  */
1591 void ModelExecution::add_thread(Thread *t)
1592 {
1593         unsigned int i = id_to_int(t->get_id());
1594         if (i >= thread_map.size())
1595                 thread_map.resize(i + 1);
1596         thread_map[i] = t;
1597         if (!t->is_model_thread())
1598                 scheduler->add_thread(t);
1599 }
1600
1601 /**
1602  * @brief Get a Thread reference by its ID
1603  * @param tid The Thread's ID
1604  * @return A Thread reference
1605  */
1606 Thread * ModelExecution::get_thread(thread_id_t tid) const
1607 {
1608         unsigned int i = id_to_int(tid);
1609         if (i < thread_map.size())
1610                 return thread_map[i];
1611         return NULL;
1612 }
1613
1614 /**
1615  * @brief Get a reference to the Thread in which a ModelAction was executed
1616  * @param act The ModelAction
1617  * @return A Thread reference
1618  */
1619 Thread * ModelExecution::get_thread(const ModelAction *act) const
1620 {
1621         return get_thread(act->get_tid());
1622 }
1623
1624 /**
1625  * @brief Get a Thread reference by its pthread ID
1626  * @param index The pthread's ID
1627  * @return A Thread reference
1628  */
1629 Thread * ModelExecution::get_pthread(pthread_t pid) {
1630         union {
1631                 pthread_t p;
1632                 uint32_t v;
1633         } x;
1634         x.p = pid;
1635         uint32_t thread_id = x.v;
1636         if (thread_id < pthread_counter + 1) return pthread_map[thread_id];
1637         else return NULL;
1638 }
1639
1640 /**
1641  * @brief Check if a Thread is currently enabled
1642  * @param t The Thread to check
1643  * @return True if the Thread is currently enabled
1644  */
1645 bool ModelExecution::is_enabled(Thread *t) const
1646 {
1647         return scheduler->is_enabled(t);
1648 }
1649
1650 /**
1651  * @brief Check if a Thread is currently enabled
1652  * @param tid The ID of the Thread to check
1653  * @return True if the Thread is currently enabled
1654  */
1655 bool ModelExecution::is_enabled(thread_id_t tid) const
1656 {
1657         return scheduler->is_enabled(tid);
1658 }
1659
1660 /**
1661  * @brief Select the next thread to execute based on the curren action
1662  *
1663  * RMW actions occur in two parts, and we cannot split them. And THREAD_CREATE
1664  * actions should be followed by the execution of their child thread. In either
1665  * case, the current action should determine the next thread schedule.
1666  *
1667  * @param curr The current action
1668  * @return The next thread to run, if the current action will determine this
1669  * selection; otherwise NULL
1670  */
1671 Thread * ModelExecution::action_select_next_thread(const ModelAction *curr) const
1672 {
1673         /* Do not split atomic RMW */
1674         if (curr->is_rmwr() && !paused_by_fuzzer(curr))
1675                 return get_thread(curr);
1676         /* Follow CREATE with the created thread */
1677         /* which is not needed, because model.cc takes care of this */
1678         if (curr->get_type() == THREAD_CREATE)
1679                 return curr->get_thread_operand();
1680         if (curr->get_type() == PTHREAD_CREATE) {
1681                 return curr->get_thread_operand();
1682         }
1683         return NULL;
1684 }
1685
1686 /** @param act A read atomic action */
1687 bool ModelExecution::paused_by_fuzzer(const ModelAction * act) const
1688 {
1689         ASSERT(act->is_read());
1690
1691         // Actions paused by fuzzer have their sequence number reset to 0
1692         return act->get_seq_number() == 0;
1693 }
1694
1695 /**
1696  * Takes the next step in the execution, if possible.
1697  * @param curr The current step to take
1698  * @return Returns the next Thread to run, if any; NULL if this execution
1699  * should terminate
1700  */
1701 Thread * ModelExecution::take_step(ModelAction *curr)
1702 {
1703         Thread *curr_thrd = get_thread(curr);
1704         ASSERT(curr_thrd->get_state() == THREAD_READY);
1705
1706         ASSERT(check_action_enabled(curr));     /* May have side effects? */
1707         curr = check_current_action(curr);
1708         ASSERT(curr);
1709
1710         /* Process this action in ModelHistory for records */
1711         model->get_history()->process_action( curr, curr->get_tid() );
1712
1713         if (curr_thrd->is_blocked() || curr_thrd->is_complete())
1714                 scheduler->remove_thread(curr_thrd);
1715
1716         return action_select_next_thread(curr);
1717 }
1718
1719 Fuzzer * ModelExecution::getFuzzer() {
1720         return fuzzer;
1721 }