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