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