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