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