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