model.cc

   1 #include <stdio.h>
   2 #include <algorithm>
   3 #include <mutex>
   4 #include <new>
   5
   6 #include "model.h"
   7 #include "action.h"
   8 #include "nodestack.h"
   9 #include "schedule.h"
  10 #include "snapshot-interface.h"
  11 #include "common.h"
  12 #include "clockvector.h"
  13 #include "cyclegraph.h"
  14 #include "promise.h"
  15 #include "datarace.h"
  16 #include "threads-model.h"
  17 #include "output.h"
  18
  19 #define INITIAL_THREAD_ID       0
  20
  21 ModelChecker *model;
  22
  23 struct bug_message {
  24         bug_message(const char *str) {
  25                 const char *fmt = "  [BUG] %s\n";
  26                 msg = (char *)snapshot_malloc(strlen(fmt) + strlen(str));
  27                 sprintf(msg, fmt, str);
  28         }
  29         ~bug_message() { if (msg) snapshot_free(msg); }
  30
  31         char *msg;
  32         void print() { model_print("%s", msg); }
  33
  34         SNAPSHOTALLOC
  35 };
  36
  37 /**
  38  * Structure for holding small ModelChecker members that should be snapshotted
  39  */
  40 struct model_snapshot_members {
  41         model_snapshot_members() :
  42                 current_action(NULL),
  43                 /* First thread created will have id INITIAL_THREAD_ID */
  44                 next_thread_id(INITIAL_THREAD_ID),
  45                 used_sequence_numbers(0),
  46                 next_backtrack(NULL),
  47                 bugs(),
  48                 stats(),
  49                 failed_promise(false),
  50                 too_many_reads(false),
  51                 no_valid_reads(false),
  52                 bad_synchronization(false),
  53                 asserted(false)
  54         { }
  55
  56         ~model_snapshot_members() {
  57                 for (unsigned int i = 0; i < bugs.size(); i++)
  58                         delete bugs[i];
  59                 bugs.clear();
  60         }
  61
  62         ModelAction *current_action;
  63         unsigned int next_thread_id;
  64         modelclock_t used_sequence_numbers;
  65         ModelAction *next_backtrack;
  66         std::vector< bug_message *, SnapshotAlloc<bug_message *> > bugs;
  67         struct execution_stats stats;
  68         bool failed_promise;
  69         bool too_many_reads;
  70         bool no_valid_reads;
  71         /** @brief Incorrectly-ordered synchronization was made */
  72         bool bad_synchronization;
  73         bool asserted;
  74
  75         SNAPSHOTALLOC
  76 };
  77
  78 /** @brief Constructor */
  79 ModelChecker::ModelChecker(struct model_params params) :
  80         /* Initialize default scheduler */
  81         params(params),
  82         scheduler(new Scheduler()),
  83         diverge(NULL),
  84         earliest_diverge(NULL),
  85         action_trace(new action_list_t()),
  86         thread_map(new HashTable<int, Thread *, int>()),
  87         obj_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
  88         lock_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
  89         condvar_waiters_map(new HashTable<const void *, action_list_t *, uintptr_t, 4>()),
  90         obj_thrd_map(new HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4 >()),
  91         promises(new std::vector< Promise *, SnapshotAlloc<Promise *> >()),
  92         futurevalues(new std::vector< struct PendingFutureValue, SnapshotAlloc<struct PendingFutureValue> >()),
  93         pending_rel_seqs(new std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >()),
  94         thrd_last_action(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >(1)),
  95         thrd_last_fence_release(new std::vector< ModelAction *, SnapshotAlloc<ModelAction *> >()),
  96         node_stack(new NodeStack()),
  97         priv(new struct model_snapshot_members()),
  98         mo_graph(new CycleGraph())
  99 {
 100         /* Initialize a model-checker thread, for special ModelActions */
 101         model_thread = new Thread(get_next_id());
 102         thread_map->put(id_to_int(model_thread->get_id()), model_thread);
 103 }
 104
 105 /** @brief Destructor */
 106 ModelChecker::~ModelChecker()
 107 {
 108         for (unsigned int i = 0; i < get_num_threads(); i++)
 109                 delete thread_map->get(i);
 110         delete thread_map;
 111
 112         delete obj_thrd_map;
 113         delete obj_map;
 114         delete lock_waiters_map;
 115         delete condvar_waiters_map;
 116         delete action_trace;
 117
 118         for (unsigned int i = 0; i < promises->size(); i++)
 119                 delete (*promises)[i];
 120         delete promises;
 121
 122         delete pending_rel_seqs;
 123
 124         delete thrd_last_action;
 125         delete thrd_last_fence_release;
 126         delete node_stack;
 127         delete scheduler;
 128         delete mo_graph;
 129         delete priv;
 130 }
 131
 132 static action_list_t * get_safe_ptr_action(HashTable<const void *, action_list_t *, uintptr_t, 4> * hash, void * ptr)
 133 {
 134         action_list_t *tmp = hash->get(ptr);
 135         if (tmp == NULL) {
 136                 tmp = new action_list_t();
 137                 hash->put(ptr, tmp);
 138         }
 139         return tmp;
 140 }
 141
 142 static std::vector<action_list_t> * get_safe_ptr_vect_action(HashTable<void *, std::vector<action_list_t> *, uintptr_t, 4> * hash, void * ptr)
 143 {
 144         std::vector<action_list_t> *tmp = hash->get(ptr);
 145         if (tmp == NULL) {
 146                 tmp = new std::vector<action_list_t>();
 147                 hash->put(ptr, tmp);
 148         }
 149         return tmp;
 150 }
 151
 152 /**
 153  * Restores user program to initial state and resets all model-checker data
 154  * structures.
 155  */
 156 void ModelChecker::reset_to_initial_state()
 157 {
 158         DEBUG("+++ Resetting to initial state +++\n");
 159         node_stack->reset_execution();
 160
 161         /* Print all model-checker output before rollback */
 162         fflush(model_out);
 163
 164         snapshot_backtrack_before(0);
 165 }
 166
 167 /** @return a thread ID for a new Thread */
 168 thread_id_t ModelChecker::get_next_id()
 169 {
 170         return priv->next_thread_id++;
 171 }
 172
 173 /** @return the number of user threads created during this execution */
 174 unsigned int ModelChecker::get_num_threads() const
 175 {
 176         return priv->next_thread_id;
 177 }
 178
 179 /**
 180  * Must be called from user-thread context (e.g., through the global
 181  * thread_current() interface)
 182  *
 183  * @return The currently executing Thread.
 184  */
 185 Thread * ModelChecker::get_current_thread() const
 186 {
 187         return scheduler->get_current_thread();
 188 }
 189
 190 /** @return a sequence number for a new ModelAction */
 191 modelclock_t ModelChecker::get_next_seq_num()
 192 {
 193         return ++priv->used_sequence_numbers;
 194 }
 195
 196 Node * ModelChecker::get_curr_node() const
 197 {
 198         return node_stack->get_head();
 199 }
 200
 201 /**
 202  * @brief Choose the next thread to execute.
 203  *
 204  * This function chooses the next thread that should execute. It can force the
 205  * adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
 206  * followed by a THREAD_START, or it can enforce execution replay/backtracking.
 207  * The model-checker may have no preference regarding the next thread (i.e.,
 208  * when exploring a new execution ordering), in which case this will return
 209  * NULL.
 210  * @param curr The current ModelAction. This action might guide the choice of
 211  * next thread.
 212  * @return The next thread to run. If the model-checker has no preference, NULL.
 213  */
 214 Thread * ModelChecker::get_next_thread(ModelAction *curr)
 215 {
 216         thread_id_t tid;
 217
 218         if (curr != NULL) {
 219                 /* Do not split atomic actions. */
 220                 if (curr->is_rmwr())
 221                         return thread_current();
 222                 else if (curr->get_type() == THREAD_CREATE)
 223                         return curr->get_thread_operand();
 224         }
 225
 226         /* Have we completed exploring the preselected path? */
 227         if (diverge == NULL)
 228                 return NULL;
 229
 230         /* Else, we are trying to replay an execution */
 231         ModelAction *next = node_stack->get_next()->get_action();
 232
 233         if (next == diverge) {
 234                 if (earliest_diverge == NULL || *diverge < *earliest_diverge)
 235                         earliest_diverge = diverge;
 236
 237                 Node *nextnode = next->get_node();
 238                 Node *prevnode = nextnode->get_parent();
 239                 scheduler->update_sleep_set(prevnode);
 240
 241                 /* Reached divergence point */
 242                 if (nextnode->increment_misc()) {
 243                         /* The next node will try to satisfy a different misc_index values. */
 244                         tid = next->get_tid();
 245                         node_stack->pop_restofstack(2);
 246                 } else if (nextnode->increment_promise()) {
 247                         /* The next node will try to satisfy a different set of promises. */
 248                         tid = next->get_tid();
 249                         node_stack->pop_restofstack(2);
 250                 } else if (nextnode->increment_read_from()) {
 251                         /* The next node will read from a different value. */
 252                         tid = next->get_tid();
 253                         node_stack->pop_restofstack(2);
 254                 } else if (nextnode->increment_future_value()) {
 255                         /* The next node will try to read from a different future value. */
 256                         tid = next->get_tid();
 257                         node_stack->pop_restofstack(2);
 258                 } else if (nextnode->increment_relseq_break()) {
 259                         /* The next node will try to resolve a release sequence differently */
 260                         tid = next->get_tid();
 261                         node_stack->pop_restofstack(2);
 262                 } else {
 263                         ASSERT(prevnode);
 264                         /* Make a different thread execute for next step */
 265                         scheduler->add_sleep(get_thread(next->get_tid()));
 266                         tid = prevnode->get_next_backtrack();
 267                         /* Make sure the backtracked thread isn't sleeping. */
 268                         node_stack->pop_restofstack(1);
 269                         if (diverge == earliest_diverge) {
 270                                 earliest_diverge = prevnode->get_action();
 271                         }
 272                 }
 273                 /* The correct sleep set is in the parent node. */
 274                 execute_sleep_set();
 275
 276                 DEBUG("*** Divergence point ***\n");
 277
 278                 diverge = NULL;
 279         } else {
 280                 tid = next->get_tid();
 281         }
 282         DEBUG("*** ModelChecker chose next thread = %d ***\n", id_to_int(tid));
 283         ASSERT(tid != THREAD_ID_T_NONE);
 284         return thread_map->get(id_to_int(tid));
 285 }
 286
 287 /**
 288  * We need to know what the next actions of all threads in the sleep
 289  * set will be.  This method computes them and stores the actions at
 290  * the corresponding thread object's pending action.
 291  */
 292
 293 void ModelChecker::execute_sleep_set()
 294 {
 295         for (unsigned int i = 0; i < get_num_threads(); i++) {
 296                 thread_id_t tid = int_to_id(i);
 297                 Thread *thr = get_thread(tid);
 298                 if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
 299                         scheduler->next_thread(thr);
 300                         Thread::swap(&system_context, thr);
 301                         priv->current_action->set_sleep_flag();
 302                         thr->set_pending(priv->current_action);
 303                 }
 304         }
 305 }
 306
 307 void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
 308 {
 309         for (unsigned int i = 0; i < get_num_threads(); i++) {
 310                 Thread *thr = get_thread(int_to_id(i));
 311                 if (scheduler->is_sleep_set(thr)) {
 312                         ModelAction *pending_act = thr->get_pending();
 313                         if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
 314                                 //Remove this thread from sleep set
 315                                 scheduler->remove_sleep(thr);
 316                 }
 317         }
 318 }
 319
 320 /** @brief Alert the model-checker that an incorrectly-ordered
 321  * synchronization was made */
 322 void ModelChecker::set_bad_synchronization()
 323 {
 324         priv->bad_synchronization = true;
 325 }
 326
 327 bool ModelChecker::has_asserted() const
 328 {
 329         return priv->asserted;
 330 }
 331
 332 void ModelChecker::set_assert()
 333 {
 334         priv->asserted = true;
 335 }
 336
 337 /**
 338  * Check if we are in a deadlock. Should only be called at the end of an
 339  * execution, although it should not give false positives in the middle of an
 340  * execution (there should be some ENABLED thread).
 341  *
 342  * @return True if program is in a deadlock; false otherwise
 343  */
 344 bool ModelChecker::is_deadlocked() const
 345 {
 346         bool blocking_threads = false;
 347         for (unsigned int i = 0; i < get_num_threads(); i++) {
 348                 thread_id_t tid = int_to_id(i);
 349                 if (is_enabled(tid))
 350                         return false;
 351                 Thread *t = get_thread(tid);
 352                 if (!t->is_model_thread() && t->get_pending())
 353                         blocking_threads = true;
 354         }
 355         return blocking_threads;
 356 }
 357
 358 /**
 359  * Check if this is a complete execution. That is, have all thread completed
 360  * execution (rather than exiting because sleep sets have forced a redundant
 361  * execution).
 362  *
 363  * @return True if the execution is complete.
 364  */
 365 bool ModelChecker::is_complete_execution() const
 366 {
 367         for (unsigned int i = 0; i < get_num_threads(); i++)
 368                 if (is_enabled(int_to_id(i)))
 369                         return false;
 370         return true;
 371 }
 372
 373 /**
 374  * @brief Assert a bug in the executing program.
 375  *
 376  * Use this function to assert any sort of bug in the user program. If the
 377  * current trace is feasible (actually, a prefix of some feasible execution),
 378  * then this execution will be aborted, printing the appropriate message. If
 379  * the current trace is not yet feasible, the error message will be stashed and
 380  * printed if the execution ever becomes feasible.
 381  *
 382  * @param msg Descriptive message for the bug (do not include newline char)
 383  * @return True if bug is immediately-feasible
 384  */
 385 bool ModelChecker::assert_bug(const char *msg)
 386 {
 387         priv->bugs.push_back(new bug_message(msg));
 388
 389         if (isfeasibleprefix()) {
 390                 set_assert();
 391                 return true;
 392         }
 393         return false;
 394 }
 395
 396 /**
 397  * @brief Assert a bug in the executing program, asserted by a user thread
 398  * @see ModelChecker::assert_bug
 399  * @param msg Descriptive message for the bug (do not include newline char)
 400  */
 401 void ModelChecker::assert_user_bug(const char *msg)
 402 {
 403         /* If feasible bug, bail out now */
 404         if (assert_bug(msg))
 405                 switch_to_master(NULL);
 406 }
 407
 408 /** @return True, if any bugs have been reported for this execution */
 409 bool ModelChecker::have_bug_reports() const
 410 {
 411         return priv->bugs.size() != 0;
 412 }
 413
 414 /** @brief Print bug report listing for this execution (if any bugs exist) */
 415 void ModelChecker::print_bugs() const
 416 {
 417         if (have_bug_reports()) {
 418                 model_print("Bug report: %zu bug%s detected\n",
 419                                 priv->bugs.size(),
 420                                 priv->bugs.size() > 1 ? "s" : "");
 421                 for (unsigned int i = 0; i < priv->bugs.size(); i++)
 422                         priv->bugs[i]->print();
 423         }
 424 }
 425
 426 /**
 427  * @brief Record end-of-execution stats
 428  *
 429  * Must be run when exiting an execution. Records various stats.
 430  * @see struct execution_stats
 431  */
 432 void ModelChecker::record_stats()
 433 {
 434         stats.num_total++;
 435         if (!isfeasibleprefix())
 436                 stats.num_infeasible++;
 437         else if (have_bug_reports())
 438                 stats.num_buggy_executions++;
 439         else if (is_complete_execution())
 440                 stats.num_complete++;
 441         else
 442                 stats.num_redundant++;
 443 }
 444
 445 /** @brief Print execution stats */
 446 void ModelChecker::print_stats() const
 447 {
 448         model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
 449         model_print("Number of redundant executions: %d\n", stats.num_redundant);
 450         model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
 451         model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
 452         model_print("Total executions: %d\n", stats.num_total);
 453         model_print("Total nodes created: %d\n", node_stack->get_total_nodes());
 454 }
 455
 456 /**
 457  * @brief End-of-exeuction print
 458  * @param printbugs Should any existing bugs be printed?
 459  */
 460 void ModelChecker::print_execution(bool printbugs) const
 461 {
 462         print_program_output();
 463
 464         if (DBG_ENABLED() || params.verbose) {
 465                 model_print("Earliest divergence point since last feasible execution:\n");
 466                 if (earliest_diverge)
 467                         earliest_diverge->print();
 468                 else
 469                         model_print("(Not set)\n");
 470
 471                 model_print("\n");
 472                 print_stats();
 473         }
 474
 475         /* Don't print invalid bugs */
 476         if (printbugs)
 477                 print_bugs();
 478
 479         model_print("\n");
 480         print_summary();
 481 }
 482
 483 /**
 484  * Queries the model-checker for more executions to explore and, if one
 485  * exists, resets the model-checker state to execute a new execution.
 486  *
 487  * @return If there are more executions to explore, return true. Otherwise,
 488  * return false.
 489  */
 490 bool ModelChecker::next_execution()
 491 {
 492         DBG();
 493         /* Is this execution a feasible execution that's worth bug-checking? */
 494         bool complete = isfeasibleprefix() && (is_complete_execution() ||
 495                         have_bug_reports());
 496
 497         /* End-of-execution bug checks */
 498         if (complete) {
 499                 if (is_deadlocked())
 500                         assert_bug("Deadlock detected");
 501
 502                 checkDataRaces();
 503         }
 504
 505         record_stats();
 506
 507         /* Output */
 508         if (DBG_ENABLED() || params.verbose || (complete && have_bug_reports()))
 509                 print_execution(complete);
 510         else
 511                 clear_program_output();
 512
 513         if (complete)
 514                 earliest_diverge = NULL;
 515
 516         if ((diverge = get_next_backtrack()) == NULL)
 517                 return false;
 518
 519         if (DBG_ENABLED()) {
 520                 model_print("Next execution will diverge at:\n");
 521                 diverge->print();
 522         }
 523
 524         reset_to_initial_state();
 525         return true;
 526 }
 527
 528 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 529 {
 530         switch (act->get_type()) {
 531         case ATOMIC_FENCE:
 532         case ATOMIC_READ:
 533         case ATOMIC_WRITE:
 534         case ATOMIC_RMW: {
 535                 /* Optimization: relaxed operations don't need backtracking */
 536                 if (act->is_relaxed())
 537                         return NULL;
 538                 /* linear search: from most recent to oldest */
 539                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 540                 action_list_t::reverse_iterator rit;
 541                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 542                         ModelAction *prev = *rit;
 543                         if (prev->could_synchronize_with(act))
 544                                 return prev;
 545                 }
 546                 break;
 547         }
 548         case ATOMIC_LOCK:
 549         case ATOMIC_TRYLOCK: {
 550                 /* linear search: from most recent to oldest */
 551                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 552                 action_list_t::reverse_iterator rit;
 553                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 554                         ModelAction *prev = *rit;
 555                         if (act->is_conflicting_lock(prev))
 556                                 return prev;
 557                 }
 558                 break;
 559         }
 560         case ATOMIC_UNLOCK: {
 561                 /* linear search: from most recent to oldest */
 562                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 563                 action_list_t::reverse_iterator rit;
 564                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 565                         ModelAction *prev = *rit;
 566                         if (!act->same_thread(prev) && prev->is_failed_trylock())
 567                                 return prev;
 568                 }
 569                 break;
 570         }
 571         case ATOMIC_WAIT: {
 572                 /* linear search: from most recent to oldest */
 573                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 574                 action_list_t::reverse_iterator rit;
 575                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 576                         ModelAction *prev = *rit;
 577                         if (!act->same_thread(prev) && prev->is_failed_trylock())
 578                                 return prev;
 579                         if (!act->same_thread(prev) && prev->is_notify())
 580                                 return prev;
 581                 }
 582                 break;
 583         }
 584
 585         case ATOMIC_NOTIFY_ALL:
 586         case ATOMIC_NOTIFY_ONE: {
 587                 /* linear search: from most recent to oldest */
 588                 action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
 589                 action_list_t::reverse_iterator rit;
 590                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 591                         ModelAction *prev = *rit;
 592                         if (!act->same_thread(prev) && prev->is_wait())
 593                                 return prev;
 594                 }
 595                 break;
 596         }
 597         default:
 598                 break;
 599         }
 600         return NULL;
 601 }
 602
 603 /** This method finds backtracking points where we should try to
 604  * reorder the parameter ModelAction against.
 605  *
 606  * @param the ModelAction to find backtracking points for.
 607  */
 608 void ModelChecker::set_backtracking(ModelAction *act)
 609 {
 610         Thread *t = get_thread(act);
 611         ModelAction *prev = get_last_conflict(act);
 612         if (prev == NULL)
 613                 return;
 614
 615         Node *node = prev->get_node()->get_parent();
 616
 617         int low_tid, high_tid;
 618         if (node->enabled_status(t->get_id()) == THREAD_ENABLED) {
 619                 low_tid = id_to_int(act->get_tid());
 620                 high_tid = low_tid + 1;
 621         } else {
 622                 low_tid = 0;
 623                 high_tid = get_num_threads();
 624         }
 625
 626         for (int i = low_tid; i < high_tid; i++) {
 627                 thread_id_t tid = int_to_id(i);
 628
 629                 /* Make sure this thread can be enabled here. */
 630                 if (i >= node->get_num_threads())
 631                         break;
 632
 633                 /* Don't backtrack into a point where the thread is disabled or sleeping. */
 634                 if (node->enabled_status(tid) != THREAD_ENABLED)
 635                         continue;
 636
 637                 /* Check if this has been explored already */
 638                 if (node->has_been_explored(tid))
 639                         continue;
 640
 641                 /* See if fairness allows */
 642                 if (model->params.fairwindow != 0 && !node->has_priority(tid)) {
 643                         bool unfair = false;
 644                         for (int t = 0; t < node->get_num_threads(); t++) {
 645                                 thread_id_t tother = int_to_id(t);
 646                                 if (node->is_enabled(tother) && node->has_priority(tother)) {
 647                                         unfair = true;
 648                                         break;
 649                                 }
 650                         }
 651                         if (unfair)
 652                                 continue;
 653                 }
 654                 /* Cache the latest backtracking point */
 655                 set_latest_backtrack(prev);
 656
 657                 /* If this is a new backtracking point, mark the tree */
 658                 if (!node->set_backtrack(tid))
 659                         continue;
 660                 DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
 661                                         id_to_int(prev->get_tid()),
 662                                         id_to_int(t->get_id()));
 663                 if (DBG_ENABLED()) {
 664                         prev->print();
 665                         act->print();
 666                 }
 667         }
 668 }
 669
 670 /**
 671  * @brief Cache the a backtracking point as the "most recent", if eligible
 672  *
 673  * Note that this does not prepare the NodeStack for this backtracking
 674  * operation, it only caches the action on a per-execution basis
 675  *
 676  * @param act The operation at which we should explore a different next action
 677  * (i.e., backtracking point)
 678  * @return True, if this action is now the most recent backtracking point;
 679  * false otherwise
 680  */
 681 bool ModelChecker::set_latest_backtrack(ModelAction *act)
 682 {
 683         if (!priv->next_backtrack || *act > *priv->next_backtrack) {
 684                 priv->next_backtrack = act;
 685                 return true;
 686         }
 687         return false;
 688 }
 689
 690 /**
 691  * Returns last backtracking point. The model checker will explore a different
 692  * path for this point in the next execution.
 693  * @return The ModelAction at which the next execution should diverge.
 694  */
 695 ModelAction * ModelChecker::get_next_backtrack()
 696 {
 697         ModelAction *next = priv->next_backtrack;
 698         priv->next_backtrack = NULL;
 699         return next;
 700 }
 701
 702 /**
 703  * Processes a read or rmw model action.
 704  * @param curr is the read model action to process.
 705  * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
 706  * @return True if processing this read updates the mo_graph.
 707  */
 708 bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
 709 {
 710         uint64_t value = VALUE_NONE;
 711         bool updated = false;
 712         while (true) {
 713                 const ModelAction *reads_from = curr->get_node()->get_read_from();
 714                 if (reads_from != NULL) {
 715                         mo_graph->startChanges();
 716
 717                         value = reads_from->get_value();
 718                         bool r_status = false;
 719
 720                         if (!second_part_of_rmw) {
 721                                 check_recency(curr, reads_from);
 722                                 r_status = r_modification_order(curr, reads_from);
 723                         }
 724
 725                         if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
 726                                 mo_graph->rollbackChanges();
 727                                 priv->too_many_reads = false;
 728                                 continue;
 729                         }
 730
 731                         read_from(curr, reads_from);
 732                         mo_graph->commitChanges();
 733                         mo_check_promises(curr, true);
 734
 735                         updated |= r_status;
 736                 } else if (!second_part_of_rmw) {
 737                         /* Read from future value */
 738                         struct future_value fv = curr->get_node()->get_future_value();
 739                         Promise *promise = new Promise(curr, fv);
 740                         value = fv.value;
 741                         curr->set_read_from_promise(promise);
 742                         promises->push_back(promise);
 743                         mo_graph->startChanges();
 744                         updated = r_modification_order(curr, promise);
 745                         mo_graph->commitChanges();
 746                 }
 747                 get_thread(curr)->set_return_value(value);
 748                 return updated;
 749         }
 750 }
 751
 752 /**
 753  * Processes a lock, trylock, or unlock model action.  @param curr is
 754  * the read model action to process.
 755  *
 756  * The try lock operation checks whether the lock is taken.  If not,
 757  * it falls to the normal lock operation case.  If so, it returns
 758  * fail.
 759  *
 760  * The lock operation has already been checked that it is enabled, so
 761  * it just grabs the lock and synchronizes with the previous unlock.
 762  *
 763  * The unlock operation has to re-enable all of the threads that are
 764  * waiting on the lock.
 765  *
 766  * @return True if synchronization was updated; false otherwise
 767  */
 768 bool ModelChecker::process_mutex(ModelAction *curr)
 769 {
 770         std::mutex *mutex = NULL;
 771         struct std::mutex_state *state = NULL;
 772
 773         if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
 774                 mutex = (std::mutex *)curr->get_location();
 775                 state = mutex->get_state();
 776         } else if (curr->is_wait()) {
 777                 mutex = (std::mutex *)curr->get_value();
 778                 state = mutex->get_state();
 779         }
 780
 781         switch (curr->get_type()) {
 782         case ATOMIC_TRYLOCK: {
 783                 bool success = !state->islocked;
 784                 curr->set_try_lock(success);
 785                 if (!success) {
 786                         get_thread(curr)->set_return_value(0);
 787                         break;
 788                 }
 789                 get_thread(curr)->set_return_value(1);
 790         }
 791                 //otherwise fall into the lock case
 792         case ATOMIC_LOCK: {
 793                 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
 794                         assert_bug("Lock access before initialization");
 795                 state->islocked = true;
 796                 ModelAction *unlock = get_last_unlock(curr);
 797                 //synchronize with the previous unlock statement
 798                 if (unlock != NULL) {
 799                         curr->synchronize_with(unlock);
 800                         return true;
 801                 }
 802                 break;
 803         }
 804         case ATOMIC_UNLOCK: {
 805                 //unlock the lock
 806                 state->islocked = false;
 807                 //wake up the other threads
 808                 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
 809                 //activate all the waiting threads
 810                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 811                         scheduler->wake(get_thread(*rit));
 812                 }
 813                 waiters->clear();
 814                 break;
 815         }
 816         case ATOMIC_WAIT: {
 817                 //unlock the lock
 818                 state->islocked = false;
 819                 //wake up the other threads
 820                 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
 821                 //activate all the waiting threads
 822                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 823                         scheduler->wake(get_thread(*rit));
 824                 }
 825                 waiters->clear();
 826                 //check whether we should go to sleep or not...simulate spurious failures
 827                 if (curr->get_node()->get_misc() == 0) {
 828                         get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
 829                         //disable us
 830                         scheduler->sleep(get_thread(curr));
 831                 }
 832                 break;
 833         }
 834         case ATOMIC_NOTIFY_ALL: {
 835                 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
 836                 //activate all the waiting threads
 837                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 838                         scheduler->wake(get_thread(*rit));
 839                 }
 840                 waiters->clear();
 841                 break;
 842         }
 843         case ATOMIC_NOTIFY_ONE: {
 844                 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
 845                 int wakeupthread = curr->get_node()->get_misc();
 846                 action_list_t::iterator it = waiters->begin();
 847                 advance(it, wakeupthread);
 848                 scheduler->wake(get_thread(*it));
 849                 waiters->erase(it);
 850                 break;
 851         }
 852
 853         default:
 854                 ASSERT(0);
 855         }
 856         return false;
 857 }
 858
 859 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
 860 {
 861         /* Do more ambitious checks now that mo is more complete */
 862         if (mo_may_allow(writer, reader)) {
 863                 Node *node = reader->get_node();
 864
 865                 /* Find an ancestor thread which exists at the time of the reader */
 866                 Thread *write_thread = get_thread(writer);
 867                 while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
 868                         write_thread = write_thread->get_parent();
 869
 870                 struct future_value fv = {
 871                         writer->get_value(),
 872                         writer->get_seq_number() + params.maxfuturedelay,
 873                         write_thread->get_id(),
 874                 };
 875                 if (node->add_future_value(fv))
 876                         set_latest_backtrack(reader);
 877         }
 878 }
 879
 880 /**
 881  * Process a write ModelAction
 882  * @param curr The ModelAction to process
 883  * @return True if the mo_graph was updated or promises were resolved
 884  */
 885 bool ModelChecker::process_write(ModelAction *curr)
 886 {
 887         bool updated_mod_order = w_modification_order(curr);
 888         bool updated_promises = resolve_promises(curr);
 889
 890         if (promises->size() == 0) {
 891                 for (unsigned int i = 0; i < futurevalues->size(); i++) {
 892                         struct PendingFutureValue pfv = (*futurevalues)[i];
 893                         add_future_value(pfv.writer, pfv.act);
 894                 }
 895                 futurevalues->clear();
 896         }
 897
 898         mo_graph->commitChanges();
 899         mo_check_promises(curr, false);
 900
 901         get_thread(curr)->set_return_value(VALUE_NONE);
 902         return updated_mod_order || updated_promises;
 903 }
 904
 905 /**
 906  * Process a fence ModelAction
 907  * @param curr The ModelAction to process
 908  * @return True if synchronization was updated
 909  */
 910 bool ModelChecker::process_fence(ModelAction *curr)
 911 {
 912         /*
 913          * fence-relaxed: no-op
 914          * fence-release: only log the occurence (not in this function), for
 915          *   use in later synchronization
 916          * fence-acquire (this function): search for hypothetical release
 917          *   sequences
 918          */
 919         bool updated = false;
 920         if (curr->is_acquire()) {
 921                 action_list_t *list = action_trace;
 922                 action_list_t::reverse_iterator rit;
 923                 /* Find X : is_read(X) && X --sb-> curr */
 924                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 925                         ModelAction *act = *rit;
 926                         if (act == curr)
 927                                 continue;
 928                         if (act->get_tid() != curr->get_tid())
 929                                 continue;
 930                         /* Stop at the beginning of the thread */
 931                         if (act->is_thread_start())
 932                                 break;
 933                         /* Stop once we reach a prior fence-acquire */
 934                         if (act->is_fence() && act->is_acquire())
 935                                 break;
 936                         if (!act->is_read())
 937                                 continue;
 938                         /* read-acquire will find its own release sequences */
 939                         if (act->is_acquire())
 940                                 continue;
 941
 942                         /* Establish hypothetical release sequences */
 943                         rel_heads_list_t release_heads;
 944                         get_release_seq_heads(curr, act, &release_heads);
 945                         for (unsigned int i = 0; i < release_heads.size(); i++)
 946                                 if (!curr->synchronize_with(release_heads[i]))
 947                                         set_bad_synchronization();
 948                         if (release_heads.size() != 0)
 949                                 updated = true;
 950                 }
 951         }
 952         return updated;
 953 }
 954
 955 /**
 956  * @brief Process the current action for thread-related activity
 957  *
 958  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
 959  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
 960  * synchronization, etc.  This function is a no-op for non-THREAD actions
 961  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
 962  *
 963  * @param curr The current action
 964  * @return True if synchronization was updated or a thread completed
 965  */
 966 bool ModelChecker::process_thread_action(ModelAction *curr)
 967 {
 968         bool updated = false;
 969
 970         switch (curr->get_type()) {
 971         case THREAD_CREATE: {
 972                 thrd_t *thrd = (thrd_t *)curr->get_location();
 973                 struct thread_params *params = (struct thread_params *)curr->get_value();
 974                 Thread *th = new Thread(thrd, params->func, params->arg);
 975                 add_thread(th);
 976                 th->set_creation(curr);
 977                 /* Promises can be satisfied by children */
 978                 for (unsigned int i = 0; i < promises->size(); i++) {
 979                         Promise *promise = (*promises)[i];
 980                         if (promise->thread_is_available(curr->get_tid()))
 981                                 promise->add_thread(th->get_id());
 982                 }
 983                 break;
 984         }
 985         case THREAD_JOIN: {
 986                 Thread *blocking = curr->get_thread_operand();
 987                 ModelAction *act = get_last_action(blocking->get_id());
 988                 curr->synchronize_with(act);
 989                 updated = true; /* trigger rel-seq checks */
 990                 break;
 991         }
 992         case THREAD_FINISH: {
 993                 Thread *th = get_thread(curr);
 994                 while (!th->wait_list_empty()) {
 995                         ModelAction *act = th->pop_wait_list();
 996                         scheduler->wake(get_thread(act));
 997                 }
 998                 th->complete();
 999                 /* Completed thread can't satisfy promises */
1000                 for (unsigned int i = 0; i < promises->size(); i++) {
1001                         Promise *promise = (*promises)[i];
1002                         if (promise->thread_is_available(th->get_id()))
1003                                 if (promise->eliminate_thread(th->get_id()))
1004                                         priv->failed_promise = true;
1005                 }
1006                 updated = true; /* trigger rel-seq checks */
1007                 break;
1008         }
1009         case THREAD_START: {
1010                 check_promises(curr->get_tid(), NULL, curr->get_cv());
1011                 break;
1012         }
1013         default:
1014                 break;
1015         }
1016
1017         return updated;
1018 }
1019
1020 /**
1021  * @brief Process the current action for release sequence fixup activity
1022  *
1023  * Performs model-checker release sequence fixups for the current action,
1024  * forcing a single pending release sequence to break (with a given, potential
1025  * "loose" write) or to complete (i.e., synchronize). If a pending release
1026  * sequence forms a complete release sequence, then we must perform the fixup
1027  * synchronization, mo_graph additions, etc.
1028  *
1029  * @param curr The current action; must be a release sequence fixup action
1030  * @param work_queue The work queue to which to add work items as they are
1031  * generated
1032  */
1033 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
1034 {
1035         const ModelAction *write = curr->get_node()->get_relseq_break();
1036         struct release_seq *sequence = pending_rel_seqs->back();
1037         pending_rel_seqs->pop_back();
1038         ASSERT(sequence);
1039         ModelAction *acquire = sequence->acquire;
1040         const ModelAction *rf = sequence->rf;
1041         const ModelAction *release = sequence->release;
1042         ASSERT(acquire);
1043         ASSERT(release);
1044         ASSERT(rf);
1045         ASSERT(release->same_thread(rf));
1046
1047         if (write == NULL) {
1048                 /**
1049                  * @todo Forcing a synchronization requires that we set
1050                  * modification order constraints. For instance, we can't allow
1051                  * a fixup sequence in which two separate read-acquire
1052                  * operations read from the same sequence, where the first one
1053                  * synchronizes and the other doesn't. Essentially, we can't
1054                  * allow any writes to insert themselves between 'release' and
1055                  * 'rf'
1056                  */
1057
1058                 /* Must synchronize */
1059                 if (!acquire->synchronize_with(release)) {
1060                         set_bad_synchronization();
1061                         return;
1062                 }
1063                 /* Re-check all pending release sequences */
1064                 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1065                 /* Re-check act for mo_graph edges */
1066                 work_queue->push_back(MOEdgeWorkEntry(acquire));
1067
1068                 /* propagate synchronization to later actions */
1069                 action_list_t::reverse_iterator rit = action_trace->rbegin();
1070                 for (; (*rit) != acquire; rit++) {
1071                         ModelAction *propagate = *rit;
1072                         if (acquire->happens_before(propagate)) {
1073                                 propagate->synchronize_with(acquire);
1074                                 /* Re-check 'propagate' for mo_graph edges */
1075                                 work_queue->push_back(MOEdgeWorkEntry(propagate));
1076                         }
1077                 }
1078         } else {
1079                 /* Break release sequence with new edges:
1080                  *   release --mo--> write --mo--> rf */
1081                 mo_graph->addEdge(release, write);
1082                 mo_graph->addEdge(write, rf);
1083         }
1084
1085         /* See if we have realized a data race */
1086         checkDataRaces();
1087 }
1088
1089 /**
1090  * Initialize the current action by performing one or more of the following
1091  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
1092  * in the NodeStack, manipulating backtracking sets, allocating and
1093  * initializing clock vectors, and computing the promises to fulfill.
1094  *
1095  * @param curr The current action, as passed from the user context; may be
1096  * freed/invalidated after the execution of this function, with a different
1097  * action "returned" its place (pass-by-reference)
1098  * @return True if curr is a newly-explored action; false otherwise
1099  */
1100 bool ModelChecker::initialize_curr_action(ModelAction **curr)
1101 {
1102         ModelAction *newcurr;
1103
1104         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
1105                 newcurr = process_rmw(*curr);
1106                 delete *curr;
1107
1108                 if (newcurr->is_rmw())
1109                         compute_promises(newcurr);
1110
1111                 *curr = newcurr;
1112                 return false;
1113         }
1114
1115         (*curr)->set_seq_number(get_next_seq_num());
1116
1117         newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
1118         if (newcurr) {
1119                 /* First restore type and order in case of RMW operation */
1120                 if ((*curr)->is_rmwr())
1121                         newcurr->copy_typeandorder(*curr);
1122
1123                 ASSERT((*curr)->get_location() == newcurr->get_location());
1124                 newcurr->copy_from_new(*curr);
1125
1126                 /* Discard duplicate ModelAction; use action from NodeStack */
1127                 delete *curr;
1128
1129                 /* Always compute new clock vector */
1130                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1131
1132                 *curr = newcurr;
1133                 return false; /* Action was explored previously */
1134         } else {
1135                 newcurr = *curr;
1136
1137                 /* Always compute new clock vector */
1138                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1139
1140                 /* Assign most recent release fence */
1141                 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
1142
1143                 /*
1144                  * Perform one-time actions when pushing new ModelAction onto
1145                  * NodeStack
1146                  */
1147                 if (newcurr->is_write())
1148                         compute_promises(newcurr);
1149                 else if (newcurr->is_relseq_fixup())
1150                         compute_relseq_breakwrites(newcurr);
1151                 else if (newcurr->is_wait())
1152                         newcurr->get_node()->set_misc_max(2);
1153                 else if (newcurr->is_notify_one()) {
1154                         newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
1155                 }
1156                 return true; /* This was a new ModelAction */
1157         }
1158 }
1159
1160 /**
1161  * @brief Establish reads-from relation between two actions
1162  *
1163  * Perform basic operations involved with establishing a concrete rf relation,
1164  * including setting the ModelAction data and checking for release sequences.
1165  *
1166  * @param act The action that is reading (must be a read)
1167  * @param rf The action from which we are reading (must be a write)
1168  *
1169  * @return True if this read established synchronization
1170  */
1171 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
1172 {
1173         act->set_read_from(rf);
1174         if (rf != NULL && act->is_acquire()) {
1175                 rel_heads_list_t release_heads;
1176                 get_release_seq_heads(act, act, &release_heads);
1177                 int num_heads = release_heads.size();
1178                 for (unsigned int i = 0; i < release_heads.size(); i++)
1179                         if (!act->synchronize_with(release_heads[i])) {
1180                                 set_bad_synchronization();
1181                                 num_heads--;
1182                         }
1183                 return num_heads > 0;
1184         }
1185         return false;
1186 }
1187
1188 /**
1189  * @brief Check whether a model action is enabled.
1190  *
1191  * Checks whether a lock or join operation would be successful (i.e., is the
1192  * lock already locked, or is the joined thread already complete). If not, put
1193  * the action in a waiter list.
1194  *
1195  * @param curr is the ModelAction to check whether it is enabled.
1196  * @return a bool that indicates whether the action is enabled.
1197  */
1198 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1199         if (curr->is_lock()) {
1200                 std::mutex *lock = (std::mutex *)curr->get_location();
1201                 struct std::mutex_state *state = lock->get_state();
1202                 if (state->islocked) {
1203                         //Stick the action in the appropriate waiting queue
1204                         get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1205                         return false;
1206                 }
1207         } else if (curr->get_type() == THREAD_JOIN) {
1208                 Thread *blocking = (Thread *)curr->get_location();
1209                 if (!blocking->is_complete()) {
1210                         blocking->push_wait_list(curr);
1211                         return false;
1212                 }
1213         }
1214
1215         return true;
1216 }
1217
1218 /**
1219  * Stores the ModelAction for the current thread action.  Call this
1220  * immediately before switching from user- to system-context to pass
1221  * data between them.
1222  * @param act The ModelAction created by the user-thread action
1223  */
1224 void ModelChecker::set_current_action(ModelAction *act) {
1225         priv->current_action = act;
1226 }
1227
1228 /**
1229  * This is the heart of the model checker routine. It performs model-checking
1230  * actions corresponding to a given "current action." Among other processes, it
1231  * calculates reads-from relationships, updates synchronization clock vectors,
1232  * forms a memory_order constraints graph, and handles replay/backtrack
1233  * execution when running permutations of previously-observed executions.
1234  *
1235  * @param curr The current action to process
1236  * @return The ModelAction that is actually executed; may be different than
1237  * curr; may be NULL, if the current action is not enabled to run
1238  */
1239 ModelAction * ModelChecker::check_current_action(ModelAction *curr)
1240 {
1241         ASSERT(curr);
1242         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1243
1244         if (!check_action_enabled(curr)) {
1245                 /* Make the execution look like we chose to run this action
1246                  * much later, when a lock/join can succeed */
1247                 get_thread(curr)->set_pending(curr);
1248                 scheduler->sleep(get_thread(curr));
1249                 return NULL;
1250         }
1251
1252         bool newly_explored = initialize_curr_action(&curr);
1253
1254         DBG();
1255         if (DBG_ENABLED())
1256                 curr->print();
1257
1258         wake_up_sleeping_actions(curr);
1259
1260         /* Add the action to lists before any other model-checking tasks */
1261         if (!second_part_of_rmw)
1262                 add_action_to_lists(curr);
1263
1264         /* Build may_read_from set for newly-created actions */
1265         if (newly_explored && curr->is_read())
1266                 build_reads_from_past(curr);
1267
1268         /* Initialize work_queue with the "current action" work */
1269         work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1270         while (!work_queue.empty() && !has_asserted()) {
1271                 WorkQueueEntry work = work_queue.front();
1272                 work_queue.pop_front();
1273
1274                 switch (work.type) {
1275                 case WORK_CHECK_CURR_ACTION: {
1276                         ModelAction *act = work.action;
1277                         bool update = false; /* update this location's release seq's */
1278                         bool update_all = false; /* update all release seq's */
1279
1280                         if (process_thread_action(curr))
1281                                 update_all = true;
1282
1283                         if (act->is_read() && process_read(act, second_part_of_rmw))
1284                                 update = true;
1285
1286                         if (act->is_write() && process_write(act))
1287                                 update = true;
1288
1289                         if (act->is_fence() && process_fence(act))
1290                                 update_all = true;
1291
1292                         if (act->is_mutex_op() && process_mutex(act))
1293                                 update_all = true;
1294
1295                         if (act->is_relseq_fixup())
1296                                 process_relseq_fixup(curr, &work_queue);
1297
1298                         if (update_all)
1299                                 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1300                         else if (update)
1301                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1302                         break;
1303                 }
1304                 case WORK_CHECK_RELEASE_SEQ:
1305                         resolve_release_sequences(work.location, &work_queue);
1306                         break;
1307                 case WORK_CHECK_MO_EDGES: {
1308                         /** @todo Complete verification of work_queue */
1309                         ModelAction *act = work.action;
1310                         bool updated = false;
1311
1312                         if (act->is_read()) {
1313                                 const ModelAction *rf = act->get_reads_from();
1314                                 const Promise *promise = act->get_reads_from_promise();
1315                                 if (rf) {
1316                                         if (r_modification_order(act, rf))
1317                                                 updated = true;
1318                                 } else if (promise) {
1319                                         if (r_modification_order(act, promise))
1320                                                 updated = true;
1321                                 }
1322                         }
1323                         if (act->is_write()) {
1324                                 if (w_modification_order(act))
1325                                         updated = true;
1326                         }
1327                         mo_graph->commitChanges();
1328
1329                         if (updated)
1330                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1331                         break;
1332                 }
1333                 default:
1334                         ASSERT(false);
1335                         break;
1336                 }
1337         }
1338
1339         check_curr_backtracking(curr);
1340         set_backtracking(curr);
1341         return curr;
1342 }
1343
1344 void ModelChecker::check_curr_backtracking(ModelAction *curr)
1345 {
1346         Node *currnode = curr->get_node();
1347         Node *parnode = currnode->get_parent();
1348
1349         if ((parnode && !parnode->backtrack_empty()) ||
1350                          !currnode->misc_empty() ||
1351                          !currnode->read_from_empty() ||
1352                          !currnode->future_value_empty() ||
1353                          !currnode->promise_empty() ||
1354                          !currnode->relseq_break_empty()) {
1355                 set_latest_backtrack(curr);
1356         }
1357 }
1358
1359 bool ModelChecker::promises_expired() const
1360 {
1361         for (unsigned int i = 0; i < promises->size(); i++) {
1362                 Promise *promise = (*promises)[i];
1363                 if (promise->get_expiration() < priv->used_sequence_numbers)
1364                         return true;
1365         }
1366         return false;
1367 }
1368
1369 /**
1370  * This is the strongest feasibility check available.
1371  * @return whether the current trace (partial or complete) must be a prefix of
1372  * a feasible trace.
1373  */
1374 bool ModelChecker::isfeasibleprefix() const
1375 {
1376         return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
1377 }
1378
1379 /**
1380  * Print disagnostic information about an infeasible execution
1381  * @param prefix A string to prefix the output with; if NULL, then a default
1382  * message prefix will be provided
1383  */
1384 void ModelChecker::print_infeasibility(const char *prefix) const
1385 {
1386         char buf[100];
1387         char *ptr = buf;
1388         if (mo_graph->checkForCycles())
1389                 ptr += sprintf(ptr, "[mo cycle]");
1390         if (priv->failed_promise)
1391                 ptr += sprintf(ptr, "[failed promise]");
1392         if (priv->too_many_reads)
1393                 ptr += sprintf(ptr, "[too many reads]");
1394         if (priv->no_valid_reads)
1395                 ptr += sprintf(ptr, "[no valid reads-from]");
1396         if (priv->bad_synchronization)
1397                 ptr += sprintf(ptr, "[bad sw ordering]");
1398         if (promises_expired())
1399                 ptr += sprintf(ptr, "[promise expired]");
1400         if (promises->size() != 0)
1401                 ptr += sprintf(ptr, "[unresolved promise]");
1402         if (ptr != buf)
1403                 model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
1404 }
1405
1406 /**
1407  * Returns whether the current completed trace is feasible, except for pending
1408  * release sequences.
1409  */
1410 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
1411 {
1412         return !is_infeasible() && promises->size() == 0;
1413 }
1414
1415 /**
1416  * Check if the current partial trace is infeasible. Does not check any
1417  * end-of-execution flags, which might rule out the execution. Thus, this is
1418  * useful only for ruling an execution as infeasible.
1419  * @return whether the current partial trace is infeasible.
1420  */
1421 bool ModelChecker::is_infeasible() const
1422 {
1423         return mo_graph->checkForCycles() ||
1424                 priv->no_valid_reads ||
1425                 priv->failed_promise ||
1426                 priv->too_many_reads ||
1427                 priv->bad_synchronization ||
1428                 promises_expired();
1429 }
1430
1431 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1432 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1433         ModelAction *lastread = get_last_action(act->get_tid());
1434         lastread->process_rmw(act);
1435         if (act->is_rmw()) {
1436                 if (lastread->get_reads_from())
1437                         mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1438                 else
1439                         mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread);
1440                 mo_graph->commitChanges();
1441         }
1442         return lastread;
1443 }
1444
1445 /**
1446  * Checks whether a thread has read from the same write for too many times
1447  * without seeing the effects of a later write.
1448  *
1449  * Basic idea:
1450  * 1) there must a different write that we could read from that would satisfy the modification order,
1451  * 2) we must have read from the same value in excess of maxreads times, and
1452  * 3) that other write must have been in the reads_from set for maxreads times.
1453  *
1454  * If so, we decide that the execution is no longer feasible.
1455  */
1456 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
1457 {
1458         if (params.maxreads != 0) {
1459                 if (curr->get_node()->get_read_from_size() <= 1)
1460                         return;
1461                 //Must make sure that execution is currently feasible...  We could
1462                 //accidentally clear by rolling back
1463                 if (is_infeasible())
1464                         return;
1465                 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1466                 int tid = id_to_int(curr->get_tid());
1467
1468                 /* Skip checks */
1469                 if ((int)thrd_lists->size() <= tid)
1470                         return;
1471                 action_list_t *list = &(*thrd_lists)[tid];
1472
1473                 action_list_t::reverse_iterator rit = list->rbegin();
1474                 /* Skip past curr */
1475                 for (; (*rit) != curr; rit++)
1476                         ;
1477                 /* go past curr now */
1478                 rit++;
1479
1480                 action_list_t::reverse_iterator ritcopy = rit;
1481                 //See if we have enough reads from the same value
1482                 int count = 0;
1483                 for (; count < params.maxreads; rit++, count++) {
1484                         if (rit == list->rend())
1485                                 return;
1486                         ModelAction *act = *rit;
1487                         if (!act->is_read())
1488                                 return;
1489
1490                         if (act->get_reads_from() != rf)
1491                                 return;
1492                         if (act->get_node()->get_read_from_size() <= 1)
1493                                 return;
1494                 }
1495                 for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
1496                         /* Get write */
1497                         const ModelAction *write = curr->get_node()->get_read_from_at(i);
1498
1499                         /* Need a different write */
1500                         if (write == rf)
1501                                 continue;
1502
1503                         /* Test to see whether this is a feasible write to read from */
1504                         /** NOTE: all members of read-from set should be
1505                          *  feasible, so we no longer check it here **/
1506
1507                         rit = ritcopy;
1508
1509                         bool feasiblewrite = true;
1510                         //new we need to see if this write works for everyone
1511
1512                         for (int loop = count; loop > 0; loop--, rit++) {
1513                                 ModelAction *act = *rit;
1514                                 bool foundvalue = false;
1515                                 for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
1516                                         if (act->get_node()->get_read_from_at(j) == write) {
1517                                                 foundvalue = true;
1518                                                 break;
1519                                         }
1520                                 }
1521                                 if (!foundvalue) {
1522                                         feasiblewrite = false;
1523                                         break;
1524                                 }
1525                         }
1526                         if (feasiblewrite) {
1527                                 priv->too_many_reads = true;
1528                                 return;
1529                         }
1530                 }
1531         }
1532 }
1533
1534 /**
1535  * Updates the mo_graph with the constraints imposed from the current
1536  * read.
1537  *
1538  * Basic idea is the following: Go through each other thread and find
1539  * the last action that happened before our read.  Two cases:
1540  *
1541  * (1) The action is a write => that write must either occur before
1542  * the write we read from or be the write we read from.
1543  *
1544  * (2) The action is a read => the write that that action read from
1545  * must occur before the write we read from or be the same write.
1546  *
1547  * @param curr The current action. Must be a read.
1548  * @param rf The ModelAction or Promise that curr reads from. Must be a write.
1549  * @return True if modification order edges were added; false otherwise
1550  */
1551 template <typename rf_type>
1552 bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
1553 {
1554         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1555         unsigned int i;
1556         bool added = false;
1557         ASSERT(curr->is_read());
1558
1559         /* Last SC fence in the current thread */
1560         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1561
1562         /* Iterate over all threads */
1563         for (i = 0; i < thrd_lists->size(); i++) {
1564                 /* Last SC fence in thread i */
1565                 ModelAction *last_sc_fence_thread_local = NULL;
1566                 if (int_to_id((int)i) != curr->get_tid())
1567                         last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
1568
1569                 /* Last SC fence in thread i, before last SC fence in current thread */
1570                 ModelAction *last_sc_fence_thread_before = NULL;
1571                 if (last_sc_fence_local)
1572                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1573
1574                 /* Iterate over actions in thread, starting from most recent */
1575                 action_list_t *list = &(*thrd_lists)[i];
1576                 action_list_t::reverse_iterator rit;
1577                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1578                         ModelAction *act = *rit;
1579
1580                         if (act->is_write() && !act->equals(rf) && act != curr) {
1581                                 /* C++, Section 29.3 statement 5 */
1582                                 if (curr->is_seqcst() && last_sc_fence_thread_local &&
1583                                                 *act < *last_sc_fence_thread_local) {
1584                                         added = mo_graph->addEdge(act, rf) || added;
1585                                         break;
1586                                 }
1587                                 /* C++, Section 29.3 statement 4 */
1588                                 else if (act->is_seqcst() && last_sc_fence_local &&
1589                                                 *act < *last_sc_fence_local) {
1590                                         added = mo_graph->addEdge(act, rf) || added;
1591                                         break;
1592                                 }
1593                                 /* C++, Section 29.3 statement 6 */
1594                                 else if (last_sc_fence_thread_before &&
1595                                                 *act < *last_sc_fence_thread_before) {
1596                                         added = mo_graph->addEdge(act, rf) || added;
1597                                         break;
1598                                 }
1599                         }
1600
1601                         /*
1602                          * Include at most one act per-thread that "happens
1603                          * before" curr. Don't consider reflexively.
1604                          */
1605                         if (act->happens_before(curr) && act != curr) {
1606                                 if (act->is_write()) {
1607                                         if (!act->equals(rf)) {
1608                                                 added = mo_graph->addEdge(act, rf) || added;
1609                                         }
1610                                 } else {
1611                                         const ModelAction *prevreadfrom = act->get_reads_from();
1612                                         //if the previous read is unresolved, keep going...
1613                                         if (prevreadfrom == NULL)
1614                                                 continue;
1615
1616                                         if (!prevreadfrom->equals(rf)) {
1617                                                 added = mo_graph->addEdge(prevreadfrom, rf) || added;
1618                                         }
1619                                 }
1620                                 break;
1621                         }
1622                 }
1623         }
1624
1625         /*
1626          * All compatible, thread-exclusive promises must be ordered after any
1627          * concrete loads from the same thread
1628          */
1629         for (unsigned int i = 0; i < promises->size(); i++)
1630                 if ((*promises)[i]->is_compatible_exclusive(curr))
1631                         added = mo_graph->addEdge(rf, (*promises)[i]) || added;
1632
1633         return added;
1634 }
1635
1636 /**
1637  * Updates the mo_graph with the constraints imposed from the current write.
1638  *
1639  * Basic idea is the following: Go through each other thread and find
1640  * the lastest action that happened before our write.  Two cases:
1641  *
1642  * (1) The action is a write => that write must occur before
1643  * the current write
1644  *
1645  * (2) The action is a read => the write that that action read from
1646  * must occur before the current write.
1647  *
1648  * This method also handles two other issues:
1649  *
1650  * (I) Sequential Consistency: Making sure that if the current write is
1651  * seq_cst, that it occurs after the previous seq_cst write.
1652  *
1653  * (II) Sending the write back to non-synchronizing reads.
1654  *
1655  * @param curr The current action. Must be a write.
1656  * @return True if modification order edges were added; false otherwise
1657  */
1658 bool ModelChecker::w_modification_order(ModelAction *curr)
1659 {
1660         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1661         unsigned int i;
1662         bool added = false;
1663         ASSERT(curr->is_write());
1664
1665         if (curr->is_seqcst()) {
1666                 /* We have to at least see the last sequentially consistent write,
1667                          so we are initialized. */
1668                 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
1669                 if (last_seq_cst != NULL) {
1670                         added = mo_graph->addEdge(last_seq_cst, curr) || added;
1671                 }
1672         }
1673
1674         /* Last SC fence in the current thread */
1675         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1676
1677         /* Iterate over all threads */
1678         for (i = 0; i < thrd_lists->size(); i++) {
1679                 /* Last SC fence in thread i, before last SC fence in current thread */
1680                 ModelAction *last_sc_fence_thread_before = NULL;
1681                 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
1682                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1683
1684                 /* Iterate over actions in thread, starting from most recent */
1685                 action_list_t *list = &(*thrd_lists)[i];
1686                 action_list_t::reverse_iterator rit;
1687                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1688                         ModelAction *act = *rit;
1689                         if (act == curr) {
1690                                 /*
1691                                  * 1) If RMW and it actually read from something, then we
1692                                  * already have all relevant edges, so just skip to next
1693                                  * thread.
1694                                  *
1695                                  * 2) If RMW and it didn't read from anything, we should
1696                                  * whatever edge we can get to speed up convergence.
1697                                  *
1698                                  * 3) If normal write, we need to look at earlier actions, so
1699                                  * continue processing list.
1700                                  */
1701                                 if (curr->is_rmw()) {
1702                                         if (curr->get_reads_from() != NULL)
1703                                                 break;
1704                                         else
1705                                                 continue;
1706                                 } else
1707                                         continue;
1708                         }
1709
1710                         /* C++, Section 29.3 statement 7 */
1711                         if (last_sc_fence_thread_before && act->is_write() &&
1712                                         *act < *last_sc_fence_thread_before) {
1713                                 added = mo_graph->addEdge(act, curr) || added;
1714                                 break;
1715                         }
1716
1717                         /*
1718                          * Include at most one act per-thread that "happens
1719                          * before" curr
1720                          */
1721                         if (act->happens_before(curr)) {
1722                                 /*
1723                                  * Note: if act is RMW, just add edge:
1724                                  *   act --mo--> curr
1725                                  * The following edge should be handled elsewhere:
1726                                  *   readfrom(act) --mo--> act
1727                                  */
1728                                 if (act->is_write())
1729                                         added = mo_graph->addEdge(act, curr) || added;
1730                                 else if (act->is_read()) {
1731                                         //if previous read accessed a null, just keep going
1732                                         if (act->get_reads_from() == NULL)
1733                                                 continue;
1734                                         added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
1735                                 }
1736                                 break;
1737                         } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1738                                                      !act->same_thread(curr)) {
1739                                 /* We have an action that:
1740                                    (1) did not happen before us
1741                                    (2) is a read and we are a write
1742                                    (3) cannot synchronize with us
1743                                    (4) is in a different thread
1744                                    =>
1745                                    that read could potentially read from our write.  Note that
1746                                    these checks are overly conservative at this point, we'll
1747                                    do more checks before actually removing the
1748                                    pendingfuturevalue.
1749
1750                                  */
1751                                 if (thin_air_constraint_may_allow(curr, act)) {
1752                                         if (!is_infeasible())
1753                                                 futurevalues->push_back(PendingFutureValue(curr, act));
1754                                         else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
1755                                                 add_future_value(curr, act);
1756                                 }
1757                         }
1758                 }
1759         }
1760
1761         /*
1762          * All compatible, thread-exclusive promises must be ordered after any
1763          * concrete stores to the same thread, or else they can be merged with
1764          * this store later
1765          */
1766         for (unsigned int i = 0; i < promises->size(); i++)
1767                 if ((*promises)[i]->is_compatible_exclusive(curr))
1768                         added = mo_graph->addEdge(curr, (*promises)[i]) || added;
1769
1770         return added;
1771 }
1772
1773 /** Arbitrary reads from the future are not allowed.  Section 29.3
1774  * part 9 places some constraints.  This method checks one result of constraint
1775  * constraint.  Others require compiler support. */
1776 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
1777 {
1778         if (!writer->is_rmw())
1779                 return true;
1780
1781         if (!reader->is_rmw())
1782                 return true;
1783
1784         for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1785                 if (search == reader)
1786                         return false;
1787                 if (search->get_tid() == reader->get_tid() &&
1788                                 search->happens_before(reader))
1789                         break;
1790         }
1791
1792         return true;
1793 }
1794
1795 /**
1796  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1797  * some constraints. This method checks one the following constraint (others
1798  * require compiler support):
1799  *
1800  *   If X --hb-> Y --mo-> Z, then X should not read from Z.
1801  */
1802 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1803 {
1804         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1805         unsigned int i;
1806         /* Iterate over all threads */
1807         for (i = 0; i < thrd_lists->size(); i++) {
1808                 const ModelAction *write_after_read = NULL;
1809
1810                 /* Iterate over actions in thread, starting from most recent */
1811                 action_list_t *list = &(*thrd_lists)[i];
1812                 action_list_t::reverse_iterator rit;
1813                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1814                         ModelAction *act = *rit;
1815
1816                         /* Don't disallow due to act == reader */
1817                         if (!reader->happens_before(act) || reader == act)
1818                                 break;
1819                         else if (act->is_write())
1820                                 write_after_read = act;
1821                         else if (act->is_read() && act->get_reads_from() != NULL)
1822                                 write_after_read = act->get_reads_from();
1823                 }
1824
1825                 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1826                         return false;
1827         }
1828         return true;
1829 }
1830
1831 /**
1832  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1833  * The ModelAction under consideration is expected to be taking part in
1834  * release/acquire synchronization as an object of the "reads from" relation.
1835  * Note that this can only provide release sequence support for RMW chains
1836  * which do not read from the future, as those actions cannot be traced until
1837  * their "promise" is fulfilled. Similarly, we may not even establish the
1838  * presence of a release sequence with certainty, as some modification order
1839  * constraints may be decided further in the future. Thus, this function
1840  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1841  * and a boolean representing certainty.
1842  *
1843  * @param rf The action that might be part of a release sequence. Must be a
1844  * write.
1845  * @param release_heads A pass-by-reference style return parameter. After
1846  * execution of this function, release_heads will contain the heads of all the
1847  * relevant release sequences, if any exists with certainty
1848  * @param pending A pass-by-reference style return parameter which is only used
1849  * when returning false (i.e., uncertain). Returns most information regarding
1850  * an uncertain release sequence, including any write operations that might
1851  * break the sequence.
1852  * @return true, if the ModelChecker is certain that release_heads is complete;
1853  * false otherwise
1854  */
1855 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1856                 rel_heads_list_t *release_heads,
1857                 struct release_seq *pending) const
1858 {
1859         /* Only check for release sequences if there are no cycles */
1860         if (mo_graph->checkForCycles())
1861                 return false;
1862
1863         while (rf) {
1864                 ASSERT(rf->is_write());
1865
1866                 if (rf->is_release())
1867                         release_heads->push_back(rf);
1868                 else if (rf->get_last_fence_release())
1869                         release_heads->push_back(rf->get_last_fence_release());
1870                 if (!rf->is_rmw())
1871                         break; /* End of RMW chain */
1872
1873                 /** @todo Need to be smarter here...  In the linux lock
1874                  * example, this will run to the beginning of the program for
1875                  * every acquire. */
1876                 /** @todo The way to be smarter here is to keep going until 1
1877                  * thread has a release preceded by an acquire and you've seen
1878                  *       both. */
1879
1880                 /* acq_rel RMW is a sufficient stopping condition */
1881                 if (rf->is_acquire() && rf->is_release())
1882                         return true; /* complete */
1883
1884                 rf = rf->get_reads_from();
1885         };
1886         if (!rf) {
1887                 /* read from future: need to settle this later */
1888                 pending->rf = NULL;
1889                 return false; /* incomplete */
1890         }
1891
1892         if (rf->is_release())
1893                 return true; /* complete */
1894
1895         /* else relaxed write
1896          * - check for fence-release in the same thread (29.8, stmt. 3)
1897          * - check modification order for contiguous subsequence
1898          *   -> rf must be same thread as release */
1899
1900         const ModelAction *fence_release = rf->get_last_fence_release();
1901         /* Synchronize with a fence-release unconditionally; we don't need to
1902          * find any more "contiguous subsequence..." for it */
1903         if (fence_release)
1904                 release_heads->push_back(fence_release);
1905
1906         int tid = id_to_int(rf->get_tid());
1907         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
1908         action_list_t *list = &(*thrd_lists)[tid];
1909         action_list_t::const_reverse_iterator rit;
1910
1911         /* Find rf in the thread list */
1912         rit = std::find(list->rbegin(), list->rend(), rf);
1913         ASSERT(rit != list->rend());
1914
1915         /* Find the last {write,fence}-release */
1916         for (; rit != list->rend(); rit++) {
1917                 if (fence_release && *(*rit) < *fence_release)
1918                         break;
1919                 if ((*rit)->is_release())
1920                         break;
1921         }
1922         if (rit == list->rend()) {
1923                 /* No write-release in this thread */
1924                 return true; /* complete */
1925         } else if (fence_release && *(*rit) < *fence_release) {
1926                 /* The fence-release is more recent (and so, "stronger") than
1927                  * the most recent write-release */
1928                 return true; /* complete */
1929         } /* else, need to establish contiguous release sequence */
1930         ModelAction *release = *rit;
1931
1932         ASSERT(rf->same_thread(release));
1933
1934         pending->writes.clear();
1935
1936         bool certain = true;
1937         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1938                 if (id_to_int(rf->get_tid()) == (int)i)
1939                         continue;
1940                 list = &(*thrd_lists)[i];
1941
1942                 /* Can we ensure no future writes from this thread may break
1943                  * the release seq? */
1944                 bool future_ordered = false;
1945
1946                 ModelAction *last = get_last_action(int_to_id(i));
1947                 Thread *th = get_thread(int_to_id(i));
1948                 if ((last && rf->happens_before(last)) ||
1949                                 !is_enabled(th) ||
1950                                 th->is_complete())
1951                         future_ordered = true;
1952
1953                 ASSERT(!th->is_model_thread() || future_ordered);
1954
1955                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1956                         const ModelAction *act = *rit;
1957                         /* Reach synchronization -> this thread is complete */
1958                         if (act->happens_before(release))
1959                                 break;
1960                         if (rf->happens_before(act)) {
1961                                 future_ordered = true;
1962                                 continue;
1963                         }
1964
1965                         /* Only non-RMW writes can break release sequences */
1966                         if (!act->is_write() || act->is_rmw())
1967                                 continue;
1968
1969                         /* Check modification order */
1970                         if (mo_graph->checkReachable(rf, act)) {
1971                                 /* rf --mo--> act */
1972                                 future_ordered = true;
1973                                 continue;
1974                         }
1975                         if (mo_graph->checkReachable(act, release))
1976                                 /* act --mo--> release */
1977                                 break;
1978                         if (mo_graph->checkReachable(release, act) &&
1979                                       mo_graph->checkReachable(act, rf)) {
1980                                 /* release --mo-> act --mo--> rf */
1981                                 return true; /* complete */
1982                         }
1983                         /* act may break release sequence */
1984                         pending->writes.push_back(act);
1985                         certain = false;
1986                 }
1987                 if (!future_ordered)
1988                         certain = false; /* This thread is uncertain */
1989         }
1990
1991         if (certain) {
1992                 release_heads->push_back(release);
1993                 pending->writes.clear();
1994         } else {
1995                 pending->release = release;
1996                 pending->rf = rf;
1997         }
1998         return certain;
1999 }
2000
2001 /**
2002  * An interface for getting the release sequence head(s) with which a
2003  * given ModelAction must synchronize. This function only returns a non-empty
2004  * result when it can locate a release sequence head with certainty. Otherwise,
2005  * it may mark the internal state of the ModelChecker so that it will handle
2006  * the release sequence at a later time, causing @a acquire to update its
2007  * synchronization at some later point in execution.
2008  *
2009  * @param acquire The 'acquire' action that may synchronize with a release
2010  * sequence
2011  * @param read The read action that may read from a release sequence; this may
2012  * be the same as acquire, or else an earlier action in the same thread (i.e.,
2013  * when 'acquire' is a fence-acquire)
2014  * @param release_heads A pass-by-reference return parameter. Will be filled
2015  * with the head(s) of the release sequence(s), if they exists with certainty.
2016  * @see ModelChecker::release_seq_heads
2017  */
2018 void ModelChecker::get_release_seq_heads(ModelAction *acquire,
2019                 ModelAction *read, rel_heads_list_t *release_heads)
2020 {
2021         const ModelAction *rf = read->get_reads_from();
2022         struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
2023         sequence->acquire = acquire;
2024         sequence->read = read;
2025
2026         if (!release_seq_heads(rf, release_heads, sequence)) {
2027                 /* add act to 'lazy checking' list */
2028                 pending_rel_seqs->push_back(sequence);
2029         } else {
2030                 snapshot_free(sequence);
2031         }
2032 }
2033
2034 /**
2035  * Attempt to resolve all stashed operations that might synchronize with a
2036  * release sequence for a given location. This implements the "lazy" portion of
2037  * determining whether or not a release sequence was contiguous, since not all
2038  * modification order information is present at the time an action occurs.
2039  *
2040  * @param location The location/object that should be checked for release
2041  * sequence resolutions. A NULL value means to check all locations.
2042  * @param work_queue The work queue to which to add work items as they are
2043  * generated
2044  * @return True if any updates occurred (new synchronization, new mo_graph
2045  * edges)
2046  */
2047 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
2048 {
2049         bool updated = false;
2050         std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
2051         while (it != pending_rel_seqs->end()) {
2052                 struct release_seq *pending = *it;
2053                 ModelAction *acquire = pending->acquire;
2054                 const ModelAction *read = pending->read;
2055
2056                 /* Only resolve sequences on the given location, if provided */
2057                 if (location && read->get_location() != location) {
2058                         it++;
2059                         continue;
2060                 }
2061
2062                 const ModelAction *rf = read->get_reads_from();
2063                 rel_heads_list_t release_heads;
2064                 bool complete;
2065                 complete = release_seq_heads(rf, &release_heads, pending);
2066                 for (unsigned int i = 0; i < release_heads.size(); i++) {
2067                         if (!acquire->has_synchronized_with(release_heads[i])) {
2068                                 if (acquire->synchronize_with(release_heads[i]))
2069                                         updated = true;
2070                                 else
2071                                         set_bad_synchronization();
2072                         }
2073                 }
2074
2075                 if (updated) {
2076                         /* Re-check all pending release sequences */
2077                         work_queue->push_back(CheckRelSeqWorkEntry(NULL));
2078                         /* Re-check read-acquire for mo_graph edges */
2079                         if (acquire->is_read())
2080                                 work_queue->push_back(MOEdgeWorkEntry(acquire));
2081
2082                         /* propagate synchronization to later actions */
2083                         action_list_t::reverse_iterator rit = action_trace->rbegin();
2084                         for (; (*rit) != acquire; rit++) {
2085                                 ModelAction *propagate = *rit;
2086                                 if (acquire->happens_before(propagate)) {
2087                                         propagate->synchronize_with(acquire);
2088                                         /* Re-check 'propagate' for mo_graph edges */
2089                                         work_queue->push_back(MOEdgeWorkEntry(propagate));
2090                                 }
2091                         }
2092                 }
2093                 if (complete) {
2094                         it = pending_rel_seqs->erase(it);
2095                         snapshot_free(pending);
2096                 } else {
2097                         it++;
2098                 }
2099         }
2100
2101         // If we resolved promises or data races, see if we have realized a data race.
2102         checkDataRaces();
2103
2104         return updated;
2105 }
2106
2107 /**
2108  * Performs various bookkeeping operations for the current ModelAction. For
2109  * instance, adds action to the per-object, per-thread action vector and to the
2110  * action trace list of all thread actions.
2111  *
2112  * @param act is the ModelAction to add.
2113  */
2114 void ModelChecker::add_action_to_lists(ModelAction *act)
2115 {
2116         int tid = id_to_int(act->get_tid());
2117         ModelAction *uninit = NULL;
2118         int uninit_id = -1;
2119         action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
2120         if (list->empty() && act->is_atomic_var()) {
2121                 uninit = new_uninitialized_action(act->get_location());
2122                 uninit_id = id_to_int(uninit->get_tid());
2123                 list->push_back(uninit);
2124         }
2125         list->push_back(act);
2126
2127         action_trace->push_back(act);
2128         if (uninit)
2129                 action_trace->push_front(uninit);
2130
2131         std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
2132         if (tid >= (int)vec->size())
2133                 vec->resize(priv->next_thread_id);
2134         (*vec)[tid].push_back(act);
2135         if (uninit)
2136                 (*vec)[uninit_id].push_front(uninit);
2137
2138         if ((int)thrd_last_action->size() <= tid)
2139                 thrd_last_action->resize(get_num_threads());
2140         (*thrd_last_action)[tid] = act;
2141         if (uninit)
2142                 (*thrd_last_action)[uninit_id] = uninit;
2143
2144         if (act->is_fence() && act->is_release()) {
2145                 if ((int)thrd_last_fence_release->size() <= tid)
2146                         thrd_last_fence_release->resize(get_num_threads());
2147                 (*thrd_last_fence_release)[tid] = act;
2148         }
2149
2150         if (act->is_wait()) {
2151                 void *mutex_loc = (void *) act->get_value();
2152                 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
2153
2154                 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
2155                 if (tid >= (int)vec->size())
2156                         vec->resize(priv->next_thread_id);
2157                 (*vec)[tid].push_back(act);
2158         }
2159 }
2160
2161 /**
2162  * @brief Get the last action performed by a particular Thread
2163  * @param tid The thread ID of the Thread in question
2164  * @return The last action in the thread
2165  */
2166 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
2167 {
2168         int threadid = id_to_int(tid);
2169         if (threadid < (int)thrd_last_action->size())
2170                 return (*thrd_last_action)[id_to_int(tid)];
2171         else
2172                 return NULL;
2173 }
2174
2175 /**
2176  * @brief Get the last fence release performed by a particular Thread
2177  * @param tid The thread ID of the Thread in question
2178  * @return The last fence release in the thread, if one exists; NULL otherwise
2179  */
2180 ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
2181 {
2182         int threadid = id_to_int(tid);
2183         if (threadid < (int)thrd_last_fence_release->size())
2184                 return (*thrd_last_fence_release)[id_to_int(tid)];
2185         else
2186                 return NULL;
2187 }
2188
2189 /**
2190  * Gets the last memory_order_seq_cst write (in the total global sequence)
2191  * performed on a particular object (i.e., memory location), not including the
2192  * current action.
2193  * @param curr The current ModelAction; also denotes the object location to
2194  * check
2195  * @return The last seq_cst write
2196  */
2197 ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
2198 {
2199         void *location = curr->get_location();
2200         action_list_t *list = get_safe_ptr_action(obj_map, location);
2201         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
2202         action_list_t::reverse_iterator rit;
2203         for (rit = list->rbegin(); rit != list->rend(); rit++)
2204                 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
2205                         return *rit;
2206         return NULL;
2207 }
2208
2209 /**
2210  * Gets the last memory_order_seq_cst fence (in the total global sequence)
2211  * performed in a particular thread, prior to a particular fence.
2212  * @param tid The ID of the thread to check
2213  * @param before_fence The fence from which to begin the search; if NULL, then
2214  * search for the most recent fence in the thread.
2215  * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
2216  */
2217 ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
2218 {
2219         /* All fences should have NULL location */
2220         action_list_t *list = get_safe_ptr_action(obj_map, NULL);
2221         action_list_t::reverse_iterator rit = list->rbegin();
2222
2223         if (before_fence) {
2224                 for (; rit != list->rend(); rit++)
2225                         if (*rit == before_fence)
2226                                 break;
2227
2228                 ASSERT(*rit == before_fence);
2229                 rit++;
2230         }
2231
2232         for (; rit != list->rend(); rit++)
2233                 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
2234                         return *rit;
2235         return NULL;
2236 }
2237
2238 /**
2239  * Gets the last unlock operation performed on a particular mutex (i.e., memory
2240  * location). This function identifies the mutex according to the current
2241  * action, which is presumed to perform on the same mutex.
2242  * @param curr The current ModelAction; also denotes the object location to
2243  * check
2244  * @return The last unlock operation
2245  */
2246 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
2247 {
2248         void *location = curr->get_location();
2249         action_list_t *list = get_safe_ptr_action(obj_map, location);
2250         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
2251         action_list_t::reverse_iterator rit;
2252         for (rit = list->rbegin(); rit != list->rend(); rit++)
2253                 if ((*rit)->is_unlock() || (*rit)->is_wait())
2254                         return *rit;
2255         return NULL;
2256 }
2257
2258 ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
2259 {
2260         ModelAction *parent = get_last_action(tid);
2261         if (!parent)
2262                 parent = get_thread(tid)->get_creation();
2263         return parent;
2264 }
2265
2266 /**
2267  * Returns the clock vector for a given thread.
2268  * @param tid The thread whose clock vector we want
2269  * @return Desired clock vector
2270  */
2271 ClockVector * ModelChecker::get_cv(thread_id_t tid) const
2272 {
2273         return get_parent_action(tid)->get_cv();
2274 }
2275
2276 /**
2277  * Resolve a set of Promises with a current write. The set is provided in the
2278  * Node corresponding to @a write.
2279  * @param write The ModelAction that is fulfilling Promises
2280  * @return True if promises were resolved; false otherwise
2281  */
2282 bool ModelChecker::resolve_promises(ModelAction *write)
2283 {
2284         bool haveResolved = false;
2285         std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
2286         promise_list_t mustResolve, resolved;
2287
2288         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
2289                 Promise *promise = (*promises)[promise_index];
2290                 if (write->get_node()->get_promise(i)) {
2291                         ModelAction *read = promise->get_action();
2292                         read_from(read, write);
2293                         //Make sure the promise's value matches the write's value
2294                         ASSERT(promise->is_compatible(write));
2295                         mo_graph->resolvePromise(read, write, &mustResolve);
2296
2297                         resolved.push_back(promise);
2298                         promises->erase(promises->begin() + promise_index);
2299                         actions_to_check.push_back(read);
2300
2301                         haveResolved = true;
2302                 } else
2303                         promise_index++;
2304         }
2305
2306         for (unsigned int i = 0; i < mustResolve.size(); i++) {
2307                 if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
2308                                 == resolved.end())
2309                         priv->failed_promise = true;
2310         }
2311         for (unsigned int i = 0; i < resolved.size(); i++)
2312                 delete resolved[i];
2313         //Check whether reading these writes has made threads unable to
2314         //resolve promises
2315
2316         for (unsigned int i = 0; i < actions_to_check.size(); i++) {
2317                 ModelAction *read = actions_to_check[i];
2318                 mo_check_promises(read, true);
2319         }
2320
2321         return haveResolved;
2322 }
2323
2324 /**
2325  * Compute the set of promises that could potentially be satisfied by this
2326  * action. Note that the set computation actually appears in the Node, not in
2327  * ModelChecker.
2328  * @param curr The ModelAction that may satisfy promises
2329  */
2330 void ModelChecker::compute_promises(ModelAction *curr)
2331 {
2332         for (unsigned int i = 0; i < promises->size(); i++) {
2333                 Promise *promise = (*promises)[i];
2334                 const ModelAction *act = promise->get_action();
2335                 if (!act->happens_before(curr) &&
2336                                 act->is_read() &&
2337                                 !act->could_synchronize_with(curr) &&
2338                                 !act->same_thread(curr) &&
2339                                 act->get_location() == curr->get_location() &&
2340                                 promise->get_value() == curr->get_value()) {
2341                         curr->get_node()->set_promise(i, act->is_rmw());
2342                 }
2343         }
2344 }
2345
2346 /** Checks promises in response to change in ClockVector Threads. */
2347 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2348 {
2349         for (unsigned int i = 0; i < promises->size(); i++) {
2350                 Promise *promise = (*promises)[i];
2351                 const ModelAction *act = promise->get_action();
2352                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2353                                 merge_cv->synchronized_since(act)) {
2354                         if (promise->eliminate_thread(tid)) {
2355                                 //Promise has failed
2356                                 priv->failed_promise = true;
2357                                 return;
2358                         }
2359                 }
2360         }
2361 }
2362
2363 void ModelChecker::check_promises_thread_disabled()
2364 {
2365         for (unsigned int i = 0; i < promises->size(); i++) {
2366                 Promise *promise = (*promises)[i];
2367                 if (promise->has_failed()) {
2368                         priv->failed_promise = true;
2369                         return;
2370                 }
2371         }
2372 }
2373
2374 /**
2375  * @brief Checks promises in response to addition to modification order for
2376  * threads.
2377  *
2378  * We test whether threads are still available for satisfying promises after an
2379  * addition to our modification order constraints. Those that are unavailable
2380  * are "eliminated". Once all threads are eliminated from satisfying a promise,
2381  * that promise has failed.
2382  *
2383  * @param act The ModelAction which updated the modification order
2384  * @param is_read_check Should be true if act is a read and we must check for
2385  * updates to the store from which it read (there is a distinction here for
2386  * RMW's, which are both a load and a store)
2387  */
2388 void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
2389 {
2390         const ModelAction *write = is_read_check ? act->get_reads_from() : act;
2391
2392         for (unsigned int i = 0; i < promises->size(); i++) {
2393                 Promise *promise = (*promises)[i];
2394                 const ModelAction *pread = promise->get_action();
2395
2396                 // Is this promise on the same location?
2397                 if (!pread->same_var(write))
2398                         continue;
2399
2400                 if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
2401                         priv->failed_promise = true;
2402                         return;
2403                 }
2404
2405                 // Don't do any lookups twice for the same thread
2406                 if (!promise->thread_is_available(act->get_tid()))
2407                         continue;
2408
2409                 if (mo_graph->checkReachable(promise, write)) {
2410                         if (mo_graph->checkPromise(write, promise)) {
2411                                 priv->failed_promise = true;
2412                                 return;
2413                         }
2414                 }
2415         }
2416 }
2417
2418 /**
2419  * Compute the set of writes that may break the current pending release
2420  * sequence. This information is extracted from previou release sequence
2421  * calculations.
2422  *
2423  * @param curr The current ModelAction. Must be a release sequence fixup
2424  * action.
2425  */
2426 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2427 {
2428         if (pending_rel_seqs->empty())
2429                 return;
2430
2431         struct release_seq *pending = pending_rel_seqs->back();
2432         for (unsigned int i = 0; i < pending->writes.size(); i++) {
2433                 const ModelAction *write = pending->writes[i];
2434                 curr->get_node()->add_relseq_break(write);
2435         }
2436
2437         /* NULL means don't break the sequence; just synchronize */
2438         curr->get_node()->add_relseq_break(NULL);
2439 }
2440
2441 /**
2442  * Build up an initial set of all past writes that this 'read' action may read
2443  * from. This set is determined by the clock vector's "happens before"
2444  * relationship.
2445  * @param curr is the current ModelAction that we are exploring; it must be a
2446  * 'read' operation.
2447  */
2448 void ModelChecker::build_reads_from_past(ModelAction *curr)
2449 {
2450         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2451         unsigned int i;
2452         ASSERT(curr->is_read());
2453
2454         ModelAction *last_sc_write = NULL;
2455
2456         if (curr->is_seqcst())
2457                 last_sc_write = get_last_seq_cst_write(curr);
2458
2459         /* Iterate over all threads */
2460         for (i = 0; i < thrd_lists->size(); i++) {
2461                 /* Iterate over actions in thread, starting from most recent */
2462                 action_list_t *list = &(*thrd_lists)[i];
2463                 action_list_t::reverse_iterator rit;
2464                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2465                         ModelAction *act = *rit;
2466
2467                         /* Only consider 'write' actions */
2468                         if (!act->is_write() || act == curr)
2469                                 continue;
2470
2471                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2472                         bool allow_read = true;
2473
2474                         if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
2475                                 allow_read = false;
2476                         else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
2477                                 allow_read = false;
2478
2479                         if (allow_read) {
2480                                 /* Only add feasible reads */
2481                                 mo_graph->startChanges();
2482                                 r_modification_order(curr, act);
2483                                 if (!is_infeasible())
2484                                         curr->get_node()->add_read_from(act);
2485                                 mo_graph->rollbackChanges();
2486                         }
2487
2488                         /* Include at most one act per-thread that "happens before" curr */
2489                         if (act->happens_before(curr))
2490                                 break;
2491                 }
2492         }
2493         /* We may find no valid may-read-from only if the execution is doomed */
2494         if (!curr->get_node()->get_read_from_size()) {
2495                 priv->no_valid_reads = true;
2496                 set_assert();
2497         }
2498
2499         if (DBG_ENABLED()) {
2500                 model_print("Reached read action:\n");
2501                 curr->print();
2502                 model_print("Printing may_read_from\n");
2503                 curr->get_node()->print_may_read_from();
2504                 model_print("End printing may_read_from\n");
2505         }
2506 }
2507
2508 bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
2509 {
2510         while (true) {
2511                 /* UNINIT actions don't have a Node, and they never sleep */
2512                 if (write->is_uninitialized())
2513                         return true;
2514                 Node *prevnode = write->get_node()->get_parent();
2515
2516                 bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
2517                 if (write->is_release() && thread_sleep)
2518                         return true;
2519                 if (!write->is_rmw()) {
2520                         return false;
2521                 }
2522                 if (write->get_reads_from() == NULL)
2523                         return true;
2524                 write = write->get_reads_from();
2525         }
2526 }
2527
2528 /**
2529  * @brief Create a new action representing an uninitialized atomic
2530  * @param location The memory location of the atomic object
2531  * @return A pointer to a new ModelAction
2532  */
2533 ModelAction * ModelChecker::new_uninitialized_action(void *location) const
2534 {
2535         ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
2536         act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
2537         act->create_cv(NULL);
2538         return act;
2539 }
2540
2541 static void print_list(action_list_t *list)
2542 {
2543         action_list_t::iterator it;
2544
2545         model_print("---------------------------------------------------------------------\n");
2546
2547         unsigned int hash = 0;
2548
2549         for (it = list->begin(); it != list->end(); it++) {
2550                 (*it)->print();
2551                 hash = hash^(hash<<3)^((*it)->hash());
2552         }
2553         model_print("HASH %u\n", hash);
2554         model_print("---------------------------------------------------------------------\n");
2555 }
2556
2557 #if SUPPORT_MOD_ORDER_DUMP
2558 void ModelChecker::dumpGraph(char *filename) const
2559 {
2560         char buffer[200];
2561         sprintf(buffer, "%s.dot", filename);
2562         FILE *file = fopen(buffer, "w");
2563         fprintf(file, "digraph %s {\n", filename);
2564         mo_graph->dumpNodes(file);
2565         ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
2566
2567         for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2568                 ModelAction *action = *it;
2569                 if (action->is_read()) {
2570                         fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
2571                         if (action->get_reads_from() != NULL)
2572                                 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2573                 }
2574                 if (thread_array[action->get_tid()] != NULL) {
2575                         fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2576                 }
2577
2578                 thread_array[action->get_tid()] = action;
2579         }
2580         fprintf(file, "}\n");
2581         model_free(thread_array);
2582         fclose(file);
2583 }
2584 #endif
2585
2586 /** @brief Prints an execution trace summary. */
2587 void ModelChecker::print_summary() const
2588 {
2589 #if SUPPORT_MOD_ORDER_DUMP
2590         char buffername[100];
2591         sprintf(buffername, "exec%04u", stats.num_total);
2592         mo_graph->dumpGraphToFile(buffername);
2593         sprintf(buffername, "graph%04u", stats.num_total);
2594         dumpGraph(buffername);
2595 #endif
2596
2597         model_print("Execution %d:", stats.num_total);
2598         if (isfeasibleprefix())
2599                 model_print("\n");
2600         else
2601                 print_infeasibility(" INFEASIBLE");
2602         print_list(action_trace);
2603         model_print("\n");
2604 }
2605
2606 /**
2607  * Add a Thread to the system for the first time. Should only be called once
2608  * per thread.
2609  * @param t The Thread to add
2610  */
2611 void ModelChecker::add_thread(Thread *t)
2612 {
2613         thread_map->put(id_to_int(t->get_id()), t);
2614         scheduler->add_thread(t);
2615 }
2616
2617 /**
2618  * Removes a thread from the scheduler.
2619  * @param the thread to remove.
2620  */
2621 void ModelChecker::remove_thread(Thread *t)
2622 {
2623         scheduler->remove_thread(t);
2624 }
2625
2626 /**
2627  * @brief Get a Thread reference by its ID
2628  * @param tid The Thread's ID
2629  * @return A Thread reference
2630  */
2631 Thread * ModelChecker::get_thread(thread_id_t tid) const
2632 {
2633         return thread_map->get(id_to_int(tid));
2634 }
2635
2636 /**
2637  * @brief Get a reference to the Thread in which a ModelAction was executed
2638  * @param act The ModelAction
2639  * @return A Thread reference
2640  */
2641 Thread * ModelChecker::get_thread(const ModelAction *act) const
2642 {
2643         return get_thread(act->get_tid());
2644 }
2645
2646 /**
2647  * @brief Check if a Thread is currently enabled
2648  * @param t The Thread to check
2649  * @return True if the Thread is currently enabled
2650  */
2651 bool ModelChecker::is_enabled(Thread *t) const
2652 {
2653         return scheduler->is_enabled(t);
2654 }
2655
2656 /**
2657  * @brief Check if a Thread is currently enabled
2658  * @param tid The ID of the Thread to check
2659  * @return True if the Thread is currently enabled
2660  */
2661 bool ModelChecker::is_enabled(thread_id_t tid) const
2662 {
2663         return scheduler->is_enabled(tid);
2664 }
2665
2666 /**
2667  * Switch from a user-context to the "master thread" context (a.k.a. system
2668  * context). This switch is made with the intention of exploring a particular
2669  * model-checking action (described by a ModelAction object). Must be called
2670  * from a user-thread context.
2671  *
2672  * @param act The current action that will be explored. May be NULL only if
2673  * trace is exiting via an assertion (see ModelChecker::set_assert and
2674  * ModelChecker::has_asserted).
2675  * @return Return the value returned by the current action
2676  */
2677 uint64_t ModelChecker::switch_to_master(ModelAction *act)
2678 {
2679         DBG();
2680         Thread *old = thread_current();
2681         set_current_action(act);
2682         if (Thread::swap(old, &system_context) < 0) {
2683                 perror("swap threads");
2684                 exit(EXIT_FAILURE);
2685         }
2686         return old->get_return_value();
2687 }
2688
2689 /**
2690  * Takes the next step in the execution, if possible.
2691  * @param curr The current step to take
2692  * @return Returns true (success) if a step was taken and false otherwise.
2693  */
2694 bool ModelChecker::take_step(ModelAction *curr)
2695 {
2696         if (has_asserted())
2697                 return false;
2698
2699         Thread *curr_thrd = get_thread(curr);
2700         ASSERT(curr_thrd->get_state() == THREAD_READY);
2701
2702         curr = check_current_action(curr);
2703
2704         /* Infeasible -> don't take any more steps */
2705         if (is_infeasible())
2706                 return false;
2707         else if (isfeasibleprefix() && have_bug_reports()) {
2708                 set_assert();
2709                 return false;
2710         }
2711
2712         if (params.bound != 0)
2713                 if (priv->used_sequence_numbers > params.bound)
2714                         return false;
2715
2716         if (curr_thrd->is_blocked() || curr_thrd->is_complete())
2717                 scheduler->remove_thread(curr_thrd);
2718
2719         Thread *next_thrd = get_next_thread(curr);
2720         next_thrd = scheduler->next_thread(next_thrd);
2721
2722         DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
2723                         next_thrd ? id_to_int(next_thrd->get_id()) : -1);
2724
2725         /*
2726          * Launch end-of-execution release sequence fixups only when there are:
2727          *
2728          * (1) no more user threads to run (or when execution replay chooses
2729          *     the 'model_thread')
2730          * (2) pending release sequences
2731          * (3) pending assertions (i.e., data races)
2732          * (4) no pending promises
2733          */
2734         if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
2735                         is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
2736                 model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2737                                 pending_rel_seqs->size());
2738                 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2739                                 std::memory_order_seq_cst, NULL, VALUE_NONE,
2740                                 model_thread);
2741                 set_current_action(fixup);
2742                 return true;
2743         }
2744
2745         /* next_thrd == NULL -> don't take any more steps */
2746         if (!next_thrd)
2747                 return false;
2748
2749         if (next_thrd->get_pending() != NULL) {
2750                 /* restart a pending action */
2751                 set_current_action(next_thrd->get_pending());
2752                 next_thrd->set_pending(NULL);
2753                 return true;
2754         }
2755
2756         /* Return false only if swap fails with an error */
2757         return (Thread::swap(&system_context, next_thrd) == 0);
2758 }
2759
2760 /** Wrapper to run the user's main function, with appropriate arguments */
2761 void user_main_wrapper(void *)
2762 {
2763         user_main(model->params.argc, model->params.argv);
2764 }
2765
2766 /** @brief Run ModelChecker for the user program */
2767 void ModelChecker::run()
2768 {
2769         do {
2770                 thrd_t user_thread;
2771                 Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
2772
2773                 add_thread(t);
2774
2775                 /* Run user thread up to its first action */
2776                 scheduler->next_thread(t);
2777                 Thread::swap(&system_context, t);
2778
2779                 /* Wait for all threads to complete */
2780                 while (take_step(priv->current_action));
2781         } while (next_execution());
2782
2783         print_stats();
2784 }