execution.cc

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