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