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