execution.cc

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