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