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