execution.cc

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