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