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