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