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
 725                         if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
 726                                 mo_graph->rollbackChanges();
 727                                 priv->too_many_reads = false;
 728                                 continue;
 729                         }
 730
 731                         read_from(curr, reads_from);
 732                         mo_graph->commitChanges();
 733                         mo_check_promises(curr->get_tid(), reads_from, NULL);
 734
 735                         updated |= r_status;
 736                 } else if (!second_part_of_rmw) {
 737                         /* Read from future value */
 738                         struct future_value fv = curr->get_node()->get_future_value();
 739                         value = fv.value;
 740                         curr->set_value(fv.value);
 741                         curr->set_read_from(NULL);
 742                         promises->push_back(new Promise(curr, fv));
 743                 }
 744                 get_thread(curr)->set_return_value(value);
 745                 return updated;
 746         }
 747 }
 748
 749 /**
 750  * Processes a lock, trylock, or unlock model action.  @param curr is
 751  * the read model action to process.
 752  *
 753  * The try lock operation checks whether the lock is taken.  If not,
 754  * it falls to the normal lock operation case.  If so, it returns
 755  * fail.
 756  *
 757  * The lock operation has already been checked that it is enabled, so
 758  * it just grabs the lock and synchronizes with the previous unlock.
 759  *
 760  * The unlock operation has to re-enable all of the threads that are
 761  * waiting on the lock.
 762  *
 763  * @return True if synchronization was updated; false otherwise
 764  */
 765 bool ModelChecker::process_mutex(ModelAction *curr)
 766 {
 767         std::mutex *mutex = NULL;
 768         struct std::mutex_state *state = NULL;
 769
 770         if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
 771                 mutex = (std::mutex *)curr->get_location();
 772                 state = mutex->get_state();
 773         } else if (curr->is_wait()) {
 774                 mutex = (std::mutex *)curr->get_value();
 775                 state = mutex->get_state();
 776         }
 777
 778         switch (curr->get_type()) {
 779         case ATOMIC_TRYLOCK: {
 780                 bool success = !state->islocked;
 781                 curr->set_try_lock(success);
 782                 if (!success) {
 783                         get_thread(curr)->set_return_value(0);
 784                         break;
 785                 }
 786                 get_thread(curr)->set_return_value(1);
 787         }
 788                 //otherwise fall into the lock case
 789         case ATOMIC_LOCK: {
 790                 if (curr->get_cv()->getClock(state->alloc_tid) <= state->alloc_clock)
 791                         assert_bug("Lock access before initialization");
 792                 state->islocked = true;
 793                 ModelAction *unlock = get_last_unlock(curr);
 794                 //synchronize with the previous unlock statement
 795                 if (unlock != NULL) {
 796                         curr->synchronize_with(unlock);
 797                         return true;
 798                 }
 799                 break;
 800         }
 801         case ATOMIC_UNLOCK: {
 802                 //unlock the lock
 803                 state->islocked = false;
 804                 //wake up the other threads
 805                 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, curr->get_location());
 806                 //activate all the waiting threads
 807                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 808                         scheduler->wake(get_thread(*rit));
 809                 }
 810                 waiters->clear();
 811                 break;
 812         }
 813         case ATOMIC_WAIT: {
 814                 //unlock the lock
 815                 state->islocked = false;
 816                 //wake up the other threads
 817                 action_list_t *waiters = get_safe_ptr_action(lock_waiters_map, (void *) curr->get_value());
 818                 //activate all the waiting threads
 819                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 820                         scheduler->wake(get_thread(*rit));
 821                 }
 822                 waiters->clear();
 823                 //check whether we should go to sleep or not...simulate spurious failures
 824                 if (curr->get_node()->get_misc() == 0) {
 825                         get_safe_ptr_action(condvar_waiters_map, curr->get_location())->push_back(curr);
 826                         //disable us
 827                         scheduler->sleep(get_thread(curr));
 828                 }
 829                 break;
 830         }
 831         case ATOMIC_NOTIFY_ALL: {
 832                 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
 833                 //activate all the waiting threads
 834                 for (action_list_t::iterator rit = waiters->begin(); rit != waiters->end(); rit++) {
 835                         scheduler->wake(get_thread(*rit));
 836                 }
 837                 waiters->clear();
 838                 break;
 839         }
 840         case ATOMIC_NOTIFY_ONE: {
 841                 action_list_t *waiters = get_safe_ptr_action(condvar_waiters_map, curr->get_location());
 842                 int wakeupthread = curr->get_node()->get_misc();
 843                 action_list_t::iterator it = waiters->begin();
 844                 advance(it, wakeupthread);
 845                 scheduler->wake(get_thread(*it));
 846                 waiters->erase(it);
 847                 break;
 848         }
 849
 850         default:
 851                 ASSERT(0);
 852         }
 853         return false;
 854 }
 855
 856 void ModelChecker::add_future_value(const ModelAction *writer, ModelAction *reader)
 857 {
 858         /* Do more ambitious checks now that mo is more complete */
 859         if (mo_may_allow(writer, reader)) {
 860                 Node *node = reader->get_node();
 861
 862                 /* Find an ancestor thread which exists at the time of the reader */
 863                 Thread *write_thread = get_thread(writer);
 864                 while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
 865                         write_thread = write_thread->get_parent();
 866
 867                 struct future_value fv = {
 868                         writer->get_value(),
 869                         writer->get_seq_number() + params.maxfuturedelay,
 870                         write_thread->get_id(),
 871                 };
 872                 if (node->add_future_value(fv))
 873                         set_latest_backtrack(reader);
 874         }
 875 }
 876
 877 /**
 878  * Process a write ModelAction
 879  * @param curr The ModelAction to process
 880  * @return True if the mo_graph was updated or promises were resolved
 881  */
 882 bool ModelChecker::process_write(ModelAction *curr)
 883 {
 884         bool updated_mod_order = w_modification_order(curr);
 885         bool updated_promises = resolve_promises(curr);
 886
 887         if (promises->size() == 0) {
 888                 for (unsigned int i = 0; i < futurevalues->size(); i++) {
 889                         struct PendingFutureValue pfv = (*futurevalues)[i];
 890                         add_future_value(pfv.writer, pfv.act);
 891                 }
 892                 futurevalues->clear();
 893         }
 894
 895         mo_graph->commitChanges();
 896         mo_check_promises(curr->get_tid(), curr, NULL);
 897
 898         get_thread(curr)->set_return_value(VALUE_NONE);
 899         return updated_mod_order || updated_promises;
 900 }
 901
 902 /**
 903  * Process a fence ModelAction
 904  * @param curr The ModelAction to process
 905  * @return True if synchronization was updated
 906  */
 907 bool ModelChecker::process_fence(ModelAction *curr)
 908 {
 909         /*
 910          * fence-relaxed: no-op
 911          * fence-release: only log the occurence (not in this function), for
 912          *   use in later synchronization
 913          * fence-acquire (this function): search for hypothetical release
 914          *   sequences
 915          */
 916         bool updated = false;
 917         if (curr->is_acquire()) {
 918                 action_list_t *list = action_trace;
 919                 action_list_t::reverse_iterator rit;
 920                 /* Find X : is_read(X) && X --sb-> curr */
 921                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 922                         ModelAction *act = *rit;
 923                         if (act == curr)
 924                                 continue;
 925                         if (act->get_tid() != curr->get_tid())
 926                                 continue;
 927                         /* Stop at the beginning of the thread */
 928                         if (act->is_thread_start())
 929                                 break;
 930                         /* Stop once we reach a prior fence-acquire */
 931                         if (act->is_fence() && act->is_acquire())
 932                                 break;
 933                         if (!act->is_read())
 934                                 continue;
 935                         /* read-acquire will find its own release sequences */
 936                         if (act->is_acquire())
 937                                 continue;
 938
 939                         /* Establish hypothetical release sequences */
 940                         rel_heads_list_t release_heads;
 941                         get_release_seq_heads(curr, act, &release_heads);
 942                         for (unsigned int i = 0; i < release_heads.size(); i++)
 943                                 if (!curr->synchronize_with(release_heads[i]))
 944                                         set_bad_synchronization();
 945                         if (release_heads.size() != 0)
 946                                 updated = true;
 947                 }
 948         }
 949         return updated;
 950 }
 951
 952 /**
 953  * @brief Process the current action for thread-related activity
 954  *
 955  * Performs current-action processing for a THREAD_* ModelAction. Proccesses
 956  * may include setting Thread status, completing THREAD_FINISH/THREAD_JOIN
 957  * synchronization, etc.  This function is a no-op for non-THREAD actions
 958  * (e.g., ATOMIC_{READ,WRITE,RMW,LOCK}, etc.)
 959  *
 960  * @param curr The current action
 961  * @return True if synchronization was updated or a thread completed
 962  */
 963 bool ModelChecker::process_thread_action(ModelAction *curr)
 964 {
 965         bool updated = false;
 966
 967         switch (curr->get_type()) {
 968         case THREAD_CREATE: {
 969                 Thread *th = curr->get_thread_operand();
 970                 th->set_creation(curr);
 971                 /* Promises can be satisfied by children */
 972                 for (unsigned int i = 0; i < promises->size(); i++) {
 973                         Promise *promise = (*promises)[i];
 974                         if (promise->thread_is_available(curr->get_tid()))
 975                                 promise->add_thread(th->get_id());
 976                 }
 977                 break;
 978         }
 979         case THREAD_JOIN: {
 980                 Thread *blocking = curr->get_thread_operand();
 981                 ModelAction *act = get_last_action(blocking->get_id());
 982                 curr->synchronize_with(act);
 983                 updated = true; /* trigger rel-seq checks */
 984                 break;
 985         }
 986         case THREAD_FINISH: {
 987                 Thread *th = get_thread(curr);
 988                 while (!th->wait_list_empty()) {
 989                         ModelAction *act = th->pop_wait_list();
 990                         scheduler->wake(get_thread(act));
 991                 }
 992                 th->complete();
 993                 /* Completed thread can't satisfy promises */
 994                 for (unsigned int i = 0; i < promises->size(); i++) {
 995                         Promise *promise = (*promises)[i];
 996                         if (promise->thread_is_available(th->get_id()))
 997                                 if (promise->eliminate_thread(th->get_id()))
 998                                         priv->failed_promise = true;
 999                 }
1000                 updated = true; /* trigger rel-seq checks */
1001                 break;
1002         }
1003         case THREAD_START: {
1004                 check_promises(curr->get_tid(), NULL, curr->get_cv());
1005                 break;
1006         }
1007         default:
1008                 break;
1009         }
1010
1011         return updated;
1012 }
1013
1014 /**
1015  * @brief Process the current action for release sequence fixup activity
1016  *
1017  * Performs model-checker release sequence fixups for the current action,
1018  * forcing a single pending release sequence to break (with a given, potential
1019  * "loose" write) or to complete (i.e., synchronize). If a pending release
1020  * sequence forms a complete release sequence, then we must perform the fixup
1021  * synchronization, mo_graph additions, etc.
1022  *
1023  * @param curr The current action; must be a release sequence fixup action
1024  * @param work_queue The work queue to which to add work items as they are
1025  * generated
1026  */
1027 void ModelChecker::process_relseq_fixup(ModelAction *curr, work_queue_t *work_queue)
1028 {
1029         const ModelAction *write = curr->get_node()->get_relseq_break();
1030         struct release_seq *sequence = pending_rel_seqs->back();
1031         pending_rel_seqs->pop_back();
1032         ASSERT(sequence);
1033         ModelAction *acquire = sequence->acquire;
1034         const ModelAction *rf = sequence->rf;
1035         const ModelAction *release = sequence->release;
1036         ASSERT(acquire);
1037         ASSERT(release);
1038         ASSERT(rf);
1039         ASSERT(release->same_thread(rf));
1040
1041         if (write == NULL) {
1042                 /**
1043                  * @todo Forcing a synchronization requires that we set
1044                  * modification order constraints. For instance, we can't allow
1045                  * a fixup sequence in which two separate read-acquire
1046                  * operations read from the same sequence, where the first one
1047                  * synchronizes and the other doesn't. Essentially, we can't
1048                  * allow any writes to insert themselves between 'release' and
1049                  * 'rf'
1050                  */
1051
1052                 /* Must synchronize */
1053                 if (!acquire->synchronize_with(release)) {
1054                         set_bad_synchronization();
1055                         return;
1056                 }
1057                 /* Re-check all pending release sequences */
1058                 work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1059                 /* Re-check act for mo_graph edges */
1060                 work_queue->push_back(MOEdgeWorkEntry(acquire));
1061
1062                 /* propagate synchronization to later actions */
1063                 action_list_t::reverse_iterator rit = action_trace->rbegin();
1064                 for (; (*rit) != acquire; rit++) {
1065                         ModelAction *propagate = *rit;
1066                         if (acquire->happens_before(propagate)) {
1067                                 propagate->synchronize_with(acquire);
1068                                 /* Re-check 'propagate' for mo_graph edges */
1069                                 work_queue->push_back(MOEdgeWorkEntry(propagate));
1070                         }
1071                 }
1072         } else {
1073                 /* Break release sequence with new edges:
1074                  *   release --mo--> write --mo--> rf */
1075                 mo_graph->addEdge(release, write);
1076                 mo_graph->addEdge(write, rf);
1077         }
1078
1079         /* See if we have realized a data race */
1080         checkDataRaces();
1081 }
1082
1083 /**
1084  * Initialize the current action by performing one or more of the following
1085  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
1086  * in the NodeStack, manipulating backtracking sets, allocating and
1087  * initializing clock vectors, and computing the promises to fulfill.
1088  *
1089  * @param curr The current action, as passed from the user context; may be
1090  * freed/invalidated after the execution of this function, with a different
1091  * action "returned" its place (pass-by-reference)
1092  * @return True if curr is a newly-explored action; false otherwise
1093  */
1094 bool ModelChecker::initialize_curr_action(ModelAction **curr)
1095 {
1096         ModelAction *newcurr;
1097
1098         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
1099                 newcurr = process_rmw(*curr);
1100                 delete *curr;
1101
1102                 if (newcurr->is_rmw())
1103                         compute_promises(newcurr);
1104
1105                 *curr = newcurr;
1106                 return false;
1107         }
1108
1109         (*curr)->set_seq_number(get_next_seq_num());
1110
1111         newcurr = node_stack->explore_action(*curr, scheduler->get_enabled_array());
1112         if (newcurr) {
1113                 /* First restore type and order in case of RMW operation */
1114                 if ((*curr)->is_rmwr())
1115                         newcurr->copy_typeandorder(*curr);
1116
1117                 ASSERT((*curr)->get_location() == newcurr->get_location());
1118                 newcurr->copy_from_new(*curr);
1119
1120                 /* Discard duplicate ModelAction; use action from NodeStack */
1121                 delete *curr;
1122
1123                 /* Always compute new clock vector */
1124                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1125
1126                 *curr = newcurr;
1127                 return false; /* Action was explored previously */
1128         } else {
1129                 newcurr = *curr;
1130
1131                 /* Always compute new clock vector */
1132                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
1133
1134                 /* Assign most recent release fence */
1135                 newcurr->set_last_fence_release(get_last_fence_release(newcurr->get_tid()));
1136
1137                 /*
1138                  * Perform one-time actions when pushing new ModelAction onto
1139                  * NodeStack
1140                  */
1141                 if (newcurr->is_write())
1142                         compute_promises(newcurr);
1143                 else if (newcurr->is_relseq_fixup())
1144                         compute_relseq_breakwrites(newcurr);
1145                 else if (newcurr->is_wait())
1146                         newcurr->get_node()->set_misc_max(2);
1147                 else if (newcurr->is_notify_one()) {
1148                         newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
1149                 }
1150                 return true; /* This was a new ModelAction */
1151         }
1152 }
1153
1154 /**
1155  * @brief Establish reads-from relation between two actions
1156  *
1157  * Perform basic operations involved with establishing a concrete rf relation,
1158  * including setting the ModelAction data and checking for release sequences.
1159  *
1160  * @param act The action that is reading (must be a read)
1161  * @param rf The action from which we are reading (must be a write)
1162  *
1163  * @return True if this read established synchronization
1164  */
1165 bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
1166 {
1167         act->set_read_from(rf);
1168         if (rf != NULL && act->is_acquire()) {
1169                 rel_heads_list_t release_heads;
1170                 get_release_seq_heads(act, act, &release_heads);
1171                 int num_heads = release_heads.size();
1172                 for (unsigned int i = 0; i < release_heads.size(); i++)
1173                         if (!act->synchronize_with(release_heads[i])) {
1174                                 set_bad_synchronization();
1175                                 num_heads--;
1176                         }
1177                 return num_heads > 0;
1178         }
1179         return false;
1180 }
1181
1182 /**
1183  * @brief Check whether a model action is enabled.
1184  *
1185  * Checks whether a lock or join operation would be successful (i.e., is the
1186  * lock already locked, or is the joined thread already complete). If not, put
1187  * the action in a waiter list.
1188  *
1189  * @param curr is the ModelAction to check whether it is enabled.
1190  * @return a bool that indicates whether the action is enabled.
1191  */
1192 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1193         if (curr->is_lock()) {
1194                 std::mutex *lock = (std::mutex *)curr->get_location();
1195                 struct std::mutex_state *state = lock->get_state();
1196                 if (state->islocked) {
1197                         //Stick the action in the appropriate waiting queue
1198                         get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1199                         return false;
1200                 }
1201         } else if (curr->get_type() == THREAD_JOIN) {
1202                 Thread *blocking = (Thread *)curr->get_location();
1203                 if (!blocking->is_complete()) {
1204                         blocking->push_wait_list(curr);
1205                         return false;
1206                 }
1207         }
1208
1209         return true;
1210 }
1211
1212 /**
1213  * Stores the ModelAction for the current thread action.  Call this
1214  * immediately before switching from user- to system-context to pass
1215  * data between them.
1216  * @param act The ModelAction created by the user-thread action
1217  */
1218 void ModelChecker::set_current_action(ModelAction *act) {
1219         priv->current_action = act;
1220 }
1221
1222 /**
1223  * This is the heart of the model checker routine. It performs model-checking
1224  * actions corresponding to a given "current action." Among other processes, it
1225  * calculates reads-from relationships, updates synchronization clock vectors,
1226  * forms a memory_order constraints graph, and handles replay/backtrack
1227  * execution when running permutations of previously-observed executions.
1228  *
1229  * @param curr The current action to process
1230  * @return The ModelAction that is actually executed; may be different than
1231  * curr; may be NULL, if the current action is not enabled to run
1232  */
1233 ModelAction * ModelChecker::check_current_action(ModelAction *curr)
1234 {
1235         ASSERT(curr);
1236         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1237
1238         if (!check_action_enabled(curr)) {
1239                 /* Make the execution look like we chose to run this action
1240                  * much later, when a lock/join can succeed */
1241                 get_thread(curr)->set_pending(curr);
1242                 scheduler->sleep(get_thread(curr));
1243                 return NULL;
1244         }
1245
1246         bool newly_explored = initialize_curr_action(&curr);
1247
1248         DBG();
1249         if (DBG_ENABLED())
1250                 curr->print();
1251
1252         wake_up_sleeping_actions(curr);
1253
1254         /* Add the action to lists before any other model-checking tasks */
1255         if (!second_part_of_rmw)
1256                 add_action_to_lists(curr);
1257
1258         /* Build may_read_from set for newly-created actions */
1259         if (newly_explored && curr->is_read())
1260                 build_reads_from_past(curr);
1261
1262         /* Initialize work_queue with the "current action" work */
1263         work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1264         while (!work_queue.empty() && !has_asserted()) {
1265                 WorkQueueEntry work = work_queue.front();
1266                 work_queue.pop_front();
1267
1268                 switch (work.type) {
1269                 case WORK_CHECK_CURR_ACTION: {
1270                         ModelAction *act = work.action;
1271                         bool update = false; /* update this location's release seq's */
1272                         bool update_all = false; /* update all release seq's */
1273
1274                         if (process_thread_action(curr))
1275                                 update_all = true;
1276
1277                         if (act->is_read() && process_read(act, second_part_of_rmw))
1278                                 update = true;
1279
1280                         if (act->is_write() && process_write(act))
1281                                 update = true;
1282
1283                         if (act->is_fence() && process_fence(act))
1284                                 update_all = true;
1285
1286                         if (act->is_mutex_op() && process_mutex(act))
1287                                 update_all = true;
1288
1289                         if (act->is_relseq_fixup())
1290                                 process_relseq_fixup(curr, &work_queue);
1291
1292                         if (update_all)
1293                                 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1294                         else if (update)
1295                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1296                         break;
1297                 }
1298                 case WORK_CHECK_RELEASE_SEQ:
1299                         resolve_release_sequences(work.location, &work_queue);
1300                         break;
1301                 case WORK_CHECK_MO_EDGES: {
1302                         /** @todo Complete verification of work_queue */
1303                         ModelAction *act = work.action;
1304                         bool updated = false;
1305
1306                         if (act->is_read()) {
1307                                 const ModelAction *rf = act->get_reads_from();
1308                                 if (rf != NULL && r_modification_order(act, rf))
1309                                         updated = true;
1310                         }
1311                         if (act->is_write()) {
1312                                 if (w_modification_order(act))
1313                                         updated = true;
1314                         }
1315                         mo_graph->commitChanges();
1316
1317                         if (updated)
1318                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1319                         break;
1320                 }
1321                 default:
1322                         ASSERT(false);
1323                         break;
1324                 }
1325         }
1326
1327         check_curr_backtracking(curr);
1328         set_backtracking(curr);
1329         return curr;
1330 }
1331
1332 void ModelChecker::check_curr_backtracking(ModelAction *curr)
1333 {
1334         Node *currnode = curr->get_node();
1335         Node *parnode = currnode->get_parent();
1336
1337         if ((parnode && !parnode->backtrack_empty()) ||
1338                          !currnode->misc_empty() ||
1339                          !currnode->read_from_empty() ||
1340                          !currnode->future_value_empty() ||
1341                          !currnode->promise_empty() ||
1342                          !currnode->relseq_break_empty()) {
1343                 set_latest_backtrack(curr);
1344         }
1345 }
1346
1347 bool ModelChecker::promises_expired() const
1348 {
1349         for (unsigned int i = 0; i < promises->size(); i++) {
1350                 Promise *promise = (*promises)[i];
1351                 if (promise->get_expiration() < priv->used_sequence_numbers)
1352                         return true;
1353         }
1354         return false;
1355 }
1356
1357 /**
1358  * This is the strongest feasibility check available.
1359  * @return whether the current trace (partial or complete) must be a prefix of
1360  * a feasible trace.
1361  */
1362 bool ModelChecker::isfeasibleprefix() const
1363 {
1364         return pending_rel_seqs->size() == 0 && is_feasible_prefix_ignore_relseq();
1365 }
1366
1367 /**
1368  * Print disagnostic information about an infeasible execution
1369  * @param prefix A string to prefix the output with; if NULL, then a default
1370  * message prefix will be provided
1371  */
1372 void ModelChecker::print_infeasibility(const char *prefix) const
1373 {
1374         char buf[100];
1375         char *ptr = buf;
1376         if (mo_graph->checkForRMWViolation())
1377                 ptr += sprintf(ptr, "[RMW atomicity]");
1378         if (mo_graph->checkForCycles())
1379                 ptr += sprintf(ptr, "[mo cycle]");
1380         if (priv->failed_promise)
1381                 ptr += sprintf(ptr, "[failed promise]");
1382         if (priv->too_many_reads)
1383                 ptr += sprintf(ptr, "[too many reads]");
1384         if (priv->bad_synchronization)
1385                 ptr += sprintf(ptr, "[bad sw ordering]");
1386         if (promises_expired())
1387                 ptr += sprintf(ptr, "[promise expired]");
1388         if (promises->size() != 0)
1389                 ptr += sprintf(ptr, "[unresolved promise]");
1390         if (ptr != buf)
1391                 model_print("%s: %s\n", prefix ? prefix : "Infeasible", buf);
1392 }
1393
1394 /**
1395  * Returns whether the current completed trace is feasible, except for pending
1396  * release sequences.
1397  */
1398 bool ModelChecker::is_feasible_prefix_ignore_relseq() const
1399 {
1400         return !is_infeasible() && promises->size() == 0;
1401 }
1402
1403 /**
1404  * Check if the current partial trace is infeasible. Does not check any
1405  * end-of-execution flags, which might rule out the execution. Thus, this is
1406  * useful only for ruling an execution as infeasible.
1407  * @return whether the current partial trace is infeasible.
1408  */
1409 bool ModelChecker::is_infeasible() const
1410 {
1411         return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
1412 }
1413
1414 /**
1415  * Check If the current partial trace is infeasible, while ignoring
1416  * infeasibility related to 2 RMW's reading from the same store. It does not
1417  * check end-of-execution feasibility.
1418  * @see ModelChecker::is_infeasible
1419  * @return whether the current partial trace is infeasible, ignoring multiple
1420  * RMWs reading from the same store.
1421  * */
1422 bool ModelChecker::is_infeasible_ignoreRMW() const
1423 {
1424         return mo_graph->checkForCycles() || priv->failed_promise ||
1425                 priv->too_many_reads || priv->bad_synchronization ||
1426                 promises_expired();
1427 }
1428
1429 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1430 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1431         ModelAction *lastread = get_last_action(act->get_tid());
1432         lastread->process_rmw(act);
1433         if (act->is_rmw() && lastread->get_reads_from() != NULL) {
1434                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1435                 mo_graph->commitChanges();
1436         }
1437         return lastread;
1438 }
1439
1440 /**
1441  * Checks whether a thread has read from the same write for too many times
1442  * without seeing the effects of a later write.
1443  *
1444  * Basic idea:
1445  * 1) there must a different write that we could read from that would satisfy the modification order,
1446  * 2) we must have read from the same value in excess of maxreads times, and
1447  * 3) that other write must have been in the reads_from set for maxreads times.
1448  *
1449  * If so, we decide that the execution is no longer feasible.
1450  */
1451 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
1452 {
1453         if (params.maxreads != 0) {
1454                 if (curr->get_node()->get_read_from_size() <= 1)
1455                         return;
1456                 //Must make sure that execution is currently feasible...  We could
1457                 //accidentally clear by rolling back
1458                 if (is_infeasible())
1459                         return;
1460                 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1461                 int tid = id_to_int(curr->get_tid());
1462
1463                 /* Skip checks */
1464                 if ((int)thrd_lists->size() <= tid)
1465                         return;
1466                 action_list_t *list = &(*thrd_lists)[tid];
1467
1468                 action_list_t::reverse_iterator rit = list->rbegin();
1469                 /* Skip past curr */
1470                 for (; (*rit) != curr; rit++)
1471                         ;
1472                 /* go past curr now */
1473                 rit++;
1474
1475                 action_list_t::reverse_iterator ritcopy = rit;
1476                 //See if we have enough reads from the same value
1477                 int count = 0;
1478                 for (; count < params.maxreads; rit++, count++) {
1479                         if (rit == list->rend())
1480                                 return;
1481                         ModelAction *act = *rit;
1482                         if (!act->is_read())
1483                                 return;
1484
1485                         if (act->get_reads_from() != rf)
1486                                 return;
1487                         if (act->get_node()->get_read_from_size() <= 1)
1488                                 return;
1489                 }
1490                 for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
1491                         /* Get write */
1492                         const ModelAction *write = curr->get_node()->get_read_from_at(i);
1493
1494                         /* Need a different write */
1495                         if (write == rf)
1496                                 continue;
1497
1498                         /* Test to see whether this is a feasible write to read from */
1499                         mo_graph->startChanges();
1500                         r_modification_order(curr, write);
1501                         bool feasiblereadfrom = !is_infeasible();
1502                         mo_graph->rollbackChanges();
1503
1504                         if (!feasiblereadfrom)
1505                                 continue;
1506                         rit = ritcopy;
1507
1508                         bool feasiblewrite = true;
1509                         //new we need to see if this write works for everyone
1510
1511                         for (int loop = count; loop > 0; loop--, rit++) {
1512                                 ModelAction *act = *rit;
1513                                 bool foundvalue = false;
1514                                 for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
1515                                         if (act->get_node()->get_read_from_at(j) == write) {
1516                                                 foundvalue = true;
1517                                                 break;
1518                                         }
1519                                 }
1520                                 if (!foundvalue) {
1521                                         feasiblewrite = false;
1522                                         break;
1523                                 }
1524                         }
1525                         if (feasiblewrite) {
1526                                 priv->too_many_reads = true;
1527                                 return;
1528                         }
1529                 }
1530         }
1531 }
1532
1533 /**
1534  * Updates the mo_graph with the constraints imposed from the current
1535  * read.
1536  *
1537  * Basic idea is the following: Go through each other thread and find
1538  * the lastest action that happened before our read.  Two cases:
1539  *
1540  * (1) The action is a write => that write must either occur before
1541  * the write we read from or be the write we read from.
1542  *
1543  * (2) The action is a read => the write that that action read from
1544  * must occur before the write we read from or be the same write.
1545  *
1546  * @param curr The current action. Must be a read.
1547  * @param rf The action that curr reads from. Must be a write.
1548  * @return True if modification order edges were added; false otherwise
1549  */
1550 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
1551 {
1552         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1553         unsigned int i;
1554         bool added = false;
1555         ASSERT(curr->is_read());
1556
1557         /* Last SC fence in the current thread */
1558         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1559
1560         /* Iterate over all threads */
1561         for (i = 0; i < thrd_lists->size(); i++) {
1562                 /* Last SC fence in thread i */
1563                 ModelAction *last_sc_fence_thread_local = NULL;
1564                 if (int_to_id((int)i) != curr->get_tid())
1565                         last_sc_fence_thread_local = get_last_seq_cst_fence(int_to_id(i), NULL);
1566
1567                 /* Last SC fence in thread i, before last SC fence in current thread */
1568                 ModelAction *last_sc_fence_thread_before = NULL;
1569                 if (last_sc_fence_local)
1570                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1571
1572                 /* Iterate over actions in thread, starting from most recent */
1573                 action_list_t *list = &(*thrd_lists)[i];
1574                 action_list_t::reverse_iterator rit;
1575                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1576                         ModelAction *act = *rit;
1577
1578                         if (act->is_write() && act != rf && act != curr) {
1579                                 /* C++, Section 29.3 statement 5 */
1580                                 if (curr->is_seqcst() && last_sc_fence_thread_local &&
1581                                                 *act < *last_sc_fence_thread_local) {
1582                                         mo_graph->addEdge(act, rf);
1583                                         added = true;
1584                                         break;
1585                                 }
1586                                 /* C++, Section 29.3 statement 4 */
1587                                 else if (act->is_seqcst() && last_sc_fence_local &&
1588                                                 *act < *last_sc_fence_local) {
1589                                         mo_graph->addEdge(act, rf);
1590                                         added = true;
1591                                         break;
1592                                 }
1593                                 /* C++, Section 29.3 statement 6 */
1594                                 else if (last_sc_fence_thread_before &&
1595                                                 *act < *last_sc_fence_thread_before) {
1596                                         mo_graph->addEdge(act, rf);
1597                                         added = true;
1598                                         break;
1599                                 }
1600                         }
1601
1602                         /*
1603                          * Include at most one act per-thread that "happens
1604                          * before" curr. Don't consider reflexively.
1605                          */
1606                         if (act->happens_before(curr) && act != curr) {
1607                                 if (act->is_write()) {
1608                                         if (rf != act) {
1609                                                 mo_graph->addEdge(act, rf);
1610                                                 added = true;
1611                                         }
1612                                 } else {
1613                                         const ModelAction *prevreadfrom = act->get_reads_from();
1614                                         //if the previous read is unresolved, keep going...
1615                                         if (prevreadfrom == NULL)
1616                                                 continue;
1617
1618                                         if (rf != prevreadfrom) {
1619                                                 mo_graph->addEdge(prevreadfrom, rf);
1620                                                 added = true;
1621                                         }
1622                                 }
1623                                 break;
1624                         }
1625                 }
1626         }
1627
1628         return added;
1629 }
1630
1631 /** This method fixes up the modification order when we resolve a
1632  *  promises.  The basic problem is that actions that occur after the
1633  *  read curr could not property add items to the modification order
1634  *  for our read.
1635  *
1636  *  So for each thread, we find the earliest item that happens after
1637  *  the read curr.  This is the item we have to fix up with additional
1638  *  constraints.  If that action is write, we add a MO edge between
1639  *  the Action rf and that action.  If the action is a read, we add a
1640  *  MO edge between the Action rf, and whatever the read accessed.
1641  *
1642  * @param curr is the read ModelAction that we are fixing up MO edges for.
1643  * @param rf is the write ModelAction that curr reads from.
1644  *
1645  */
1646 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1647 {
1648         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1649         unsigned int i;
1650         ASSERT(curr->is_read());
1651
1652         /* Iterate over all threads */
1653         for (i = 0; i < thrd_lists->size(); i++) {
1654                 /* Iterate over actions in thread, starting from most recent */
1655                 action_list_t *list = &(*thrd_lists)[i];
1656                 action_list_t::reverse_iterator rit;
1657                 ModelAction *lastact = NULL;
1658
1659                 /* Find last action that happens after curr that is either not curr or a rmw */
1660                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1661                         ModelAction *act = *rit;
1662                         if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1663                                 lastact = act;
1664                         } else
1665                                 break;
1666                 }
1667
1668                         /* Include at most one act per-thread that "happens before" curr */
1669                 if (lastact != NULL) {
1670                         if (lastact == curr) {
1671                                 //Case 1: The resolved read is a RMW, and we need to make sure
1672                                 //that the write portion of the RMW mod order after rf
1673
1674                                 mo_graph->addEdge(rf, lastact);
1675                         } else if (lastact->is_read()) {
1676                                 //Case 2: The resolved read is a normal read and the next
1677                                 //operation is a read, and we need to make sure the value read
1678                                 //is mod ordered after rf
1679
1680                                 const ModelAction *postreadfrom = lastact->get_reads_from();
1681                                 if (postreadfrom != NULL && rf != postreadfrom)
1682                                         mo_graph->addEdge(rf, postreadfrom);
1683                         } else {
1684                                 //Case 3: The resolved read is a normal read and the next
1685                                 //operation is a write, and we need to make sure that the
1686                                 //write is mod ordered after rf
1687                                 if (lastact != rf)
1688                                         mo_graph->addEdge(rf, lastact);
1689                         }
1690                         break;
1691                 }
1692         }
1693 }
1694
1695 /**
1696  * Updates the mo_graph with the constraints imposed from the current write.
1697  *
1698  * Basic idea is the following: Go through each other thread and find
1699  * the lastest action that happened before our write.  Two cases:
1700  *
1701  * (1) The action is a write => that write must occur before
1702  * the current write
1703  *
1704  * (2) The action is a read => the write that that action read from
1705  * must occur before the current write.
1706  *
1707  * This method also handles two other issues:
1708  *
1709  * (I) Sequential Consistency: Making sure that if the current write is
1710  * seq_cst, that it occurs after the previous seq_cst write.
1711  *
1712  * (II) Sending the write back to non-synchronizing reads.
1713  *
1714  * @param curr The current action. Must be a write.
1715  * @return True if modification order edges were added; false otherwise
1716  */
1717 bool ModelChecker::w_modification_order(ModelAction *curr)
1718 {
1719         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1720         unsigned int i;
1721         bool added = false;
1722         ASSERT(curr->is_write());
1723
1724         if (curr->is_seqcst()) {
1725                 /* We have to at least see the last sequentially consistent write,
1726                          so we are initialized. */
1727                 ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
1728                 if (last_seq_cst != NULL) {
1729                         mo_graph->addEdge(last_seq_cst, curr);
1730                         added = true;
1731                 }
1732         }
1733
1734         /* Last SC fence in the current thread */
1735         ModelAction *last_sc_fence_local = get_last_seq_cst_fence(curr->get_tid(), NULL);
1736
1737         /* Iterate over all threads */
1738         for (i = 0; i < thrd_lists->size(); i++) {
1739                 /* Last SC fence in thread i, before last SC fence in current thread */
1740                 ModelAction *last_sc_fence_thread_before = NULL;
1741                 if (last_sc_fence_local && int_to_id((int)i) != curr->get_tid())
1742                         last_sc_fence_thread_before = get_last_seq_cst_fence(int_to_id(i), last_sc_fence_local);
1743
1744                 /* Iterate over actions in thread, starting from most recent */
1745                 action_list_t *list = &(*thrd_lists)[i];
1746                 action_list_t::reverse_iterator rit;
1747                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1748                         ModelAction *act = *rit;
1749                         if (act == curr) {
1750                                 /*
1751                                  * 1) If RMW and it actually read from something, then we
1752                                  * already have all relevant edges, so just skip to next
1753                                  * thread.
1754                                  *
1755                                  * 2) If RMW and it didn't read from anything, we should
1756                                  * whatever edge we can get to speed up convergence.
1757                                  *
1758                                  * 3) If normal write, we need to look at earlier actions, so
1759                                  * continue processing list.
1760                                  */
1761                                 if (curr->is_rmw()) {
1762                                         if (curr->get_reads_from() != NULL)
1763                                                 break;
1764                                         else
1765                                                 continue;
1766                                 } else
1767                                         continue;
1768                         }
1769
1770                         /* C++, Section 29.3 statement 7 */
1771                         if (last_sc_fence_thread_before && act->is_write() &&
1772                                         *act < *last_sc_fence_thread_before) {
1773                                 mo_graph->addEdge(act, curr);
1774                                 added = true;
1775                                 break;
1776                         }
1777
1778                         /*
1779                          * Include at most one act per-thread that "happens
1780                          * before" curr
1781                          */
1782                         if (act->happens_before(curr)) {
1783                                 /*
1784                                  * Note: if act is RMW, just add edge:
1785                                  *   act --mo--> curr
1786                                  * The following edge should be handled elsewhere:
1787                                  *   readfrom(act) --mo--> act
1788                                  */
1789                                 if (act->is_write())
1790                                         mo_graph->addEdge(act, curr);
1791                                 else if (act->is_read()) {
1792                                         //if previous read accessed a null, just keep going
1793                                         if (act->get_reads_from() == NULL)
1794                                                 continue;
1795                                         mo_graph->addEdge(act->get_reads_from(), curr);
1796                                 }
1797                                 added = true;
1798                                 break;
1799                         } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1800                                                      !act->same_thread(curr)) {
1801                                 /* We have an action that:
1802                                    (1) did not happen before us
1803                                    (2) is a read and we are a write
1804                                    (3) cannot synchronize with us
1805                                    (4) is in a different thread
1806                                    =>
1807                                    that read could potentially read from our write.  Note that
1808                                    these checks are overly conservative at this point, we'll
1809                                    do more checks before actually removing the
1810                                    pendingfuturevalue.
1811
1812                                  */
1813                                 if (thin_air_constraint_may_allow(curr, act)) {
1814                                         if (!is_infeasible() ||
1815                                                         (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
1816                                                 futurevalues->push_back(PendingFutureValue(curr, act));
1817                                         }
1818                                 }
1819                         }
1820                 }
1821         }
1822
1823         return added;
1824 }
1825
1826 /** Arbitrary reads from the future are not allowed.  Section 29.3
1827  * part 9 places some constraints.  This method checks one result of constraint
1828  * constraint.  Others require compiler support. */
1829 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction *writer, const ModelAction *reader)
1830 {
1831         if (!writer->is_rmw())
1832                 return true;
1833
1834         if (!reader->is_rmw())
1835                 return true;
1836
1837         for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1838                 if (search == reader)
1839                         return false;
1840                 if (search->get_tid() == reader->get_tid() &&
1841                                 search->happens_before(reader))
1842                         break;
1843         }
1844
1845         return true;
1846 }
1847
1848 /**
1849  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1850  * some constraints. This method checks one the following constraint (others
1851  * require compiler support):
1852  *
1853  *   If X --hb-> Y --mo-> Z, then X should not read from Z.
1854  */
1855 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1856 {
1857         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1858         unsigned int i;
1859         /* Iterate over all threads */
1860         for (i = 0; i < thrd_lists->size(); i++) {
1861                 const ModelAction *write_after_read = NULL;
1862
1863                 /* Iterate over actions in thread, starting from most recent */
1864                 action_list_t *list = &(*thrd_lists)[i];
1865                 action_list_t::reverse_iterator rit;
1866                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1867                         ModelAction *act = *rit;
1868
1869                         /* Don't disallow due to act == reader */
1870                         if (!reader->happens_before(act) || reader == act)
1871                                 break;
1872                         else if (act->is_write())
1873                                 write_after_read = act;
1874                         else if (act->is_read() && act->get_reads_from() != NULL)
1875                                 write_after_read = act->get_reads_from();
1876                 }
1877
1878                 if (write_after_read && write_after_read != writer && mo_graph->checkReachable(write_after_read, writer))
1879                         return false;
1880         }
1881         return true;
1882 }
1883
1884 /**
1885  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1886  * The ModelAction under consideration is expected to be taking part in
1887  * release/acquire synchronization as an object of the "reads from" relation.
1888  * Note that this can only provide release sequence support for RMW chains
1889  * which do not read from the future, as those actions cannot be traced until
1890  * their "promise" is fulfilled. Similarly, we may not even establish the
1891  * presence of a release sequence with certainty, as some modification order
1892  * constraints may be decided further in the future. Thus, this function
1893  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1894  * and a boolean representing certainty.
1895  *
1896  * @param rf The action that might be part of a release sequence. Must be a
1897  * write.
1898  * @param release_heads A pass-by-reference style return parameter. After
1899  * execution of this function, release_heads will contain the heads of all the
1900  * relevant release sequences, if any exists with certainty
1901  * @param pending A pass-by-reference style return parameter which is only used
1902  * when returning false (i.e., uncertain). Returns most information regarding
1903  * an uncertain release sequence, including any write operations that might
1904  * break the sequence.
1905  * @return true, if the ModelChecker is certain that release_heads is complete;
1906  * false otherwise
1907  */
1908 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1909                 rel_heads_list_t *release_heads,
1910                 struct release_seq *pending) const
1911 {
1912         /* Only check for release sequences if there are no cycles */
1913         if (mo_graph->checkForCycles())
1914                 return false;
1915
1916         while (rf) {
1917                 ASSERT(rf->is_write());
1918
1919                 if (rf->is_release())
1920                         release_heads->push_back(rf);
1921                 else if (rf->get_last_fence_release())
1922                         release_heads->push_back(rf->get_last_fence_release());
1923                 if (!rf->is_rmw())
1924                         break; /* End of RMW chain */
1925
1926                 /** @todo Need to be smarter here...  In the linux lock
1927                  * example, this will run to the beginning of the program for
1928                  * every acquire. */
1929                 /** @todo The way to be smarter here is to keep going until 1
1930                  * thread has a release preceded by an acquire and you've seen
1931                  *       both. */
1932
1933                 /* acq_rel RMW is a sufficient stopping condition */
1934                 if (rf->is_acquire() && rf->is_release())
1935                         return true; /* complete */
1936
1937                 rf = rf->get_reads_from();
1938         };
1939         if (!rf) {
1940                 /* read from future: need to settle this later */
1941                 pending->rf = NULL;
1942                 return false; /* incomplete */
1943         }
1944
1945         if (rf->is_release())
1946                 return true; /* complete */
1947
1948         /* else relaxed write
1949          * - check for fence-release in the same thread (29.8, stmt. 3)
1950          * - check modification order for contiguous subsequence
1951          *   -> rf must be same thread as release */
1952
1953         const ModelAction *fence_release = rf->get_last_fence_release();
1954         /* Synchronize with a fence-release unconditionally; we don't need to
1955          * find any more "contiguous subsequence..." for it */
1956         if (fence_release)
1957                 release_heads->push_back(fence_release);
1958
1959         int tid = id_to_int(rf->get_tid());
1960         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
1961         action_list_t *list = &(*thrd_lists)[tid];
1962         action_list_t::const_reverse_iterator rit;
1963
1964         /* Find rf in the thread list */
1965         rit = std::find(list->rbegin(), list->rend(), rf);
1966         ASSERT(rit != list->rend());
1967
1968         /* Find the last {write,fence}-release */
1969         for (; rit != list->rend(); rit++) {
1970                 if (fence_release && *(*rit) < *fence_release)
1971                         break;
1972                 if ((*rit)->is_release())
1973                         break;
1974         }
1975         if (rit == list->rend()) {
1976                 /* No write-release in this thread */
1977                 return true; /* complete */
1978         } else if (fence_release && *(*rit) < *fence_release) {
1979                 /* The fence-release is more recent (and so, "stronger") than
1980                  * the most recent write-release */
1981                 return true; /* complete */
1982         } /* else, need to establish contiguous release sequence */
1983         ModelAction *release = *rit;
1984
1985         ASSERT(rf->same_thread(release));
1986
1987         pending->writes.clear();
1988
1989         bool certain = true;
1990         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1991                 if (id_to_int(rf->get_tid()) == (int)i)
1992                         continue;
1993                 list = &(*thrd_lists)[i];
1994
1995                 /* Can we ensure no future writes from this thread may break
1996                  * the release seq? */
1997                 bool future_ordered = false;
1998
1999                 ModelAction *last = get_last_action(int_to_id(i));
2000                 Thread *th = get_thread(int_to_id(i));
2001                 if ((last && rf->happens_before(last)) ||
2002                                 !is_enabled(th) ||
2003                                 th->is_complete())
2004                         future_ordered = true;
2005
2006                 ASSERT(!th->is_model_thread() || future_ordered);
2007
2008                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2009                         const ModelAction *act = *rit;
2010                         /* Reach synchronization -> this thread is complete */
2011                         if (act->happens_before(release))
2012                                 break;
2013                         if (rf->happens_before(act)) {
2014                                 future_ordered = true;
2015                                 continue;
2016                         }
2017
2018                         /* Only non-RMW writes can break release sequences */
2019                         if (!act->is_write() || act->is_rmw())
2020                                 continue;
2021
2022                         /* Check modification order */
2023                         if (mo_graph->checkReachable(rf, act)) {
2024                                 /* rf --mo--> act */
2025                                 future_ordered = true;
2026                                 continue;
2027                         }
2028                         if (mo_graph->checkReachable(act, release))
2029                                 /* act --mo--> release */
2030                                 break;
2031                         if (mo_graph->checkReachable(release, act) &&
2032                                       mo_graph->checkReachable(act, rf)) {
2033                                 /* release --mo-> act --mo--> rf */
2034                                 return true; /* complete */
2035                         }
2036                         /* act may break release sequence */
2037                         pending->writes.push_back(act);
2038                         certain = false;
2039                 }
2040                 if (!future_ordered)
2041                         certain = false; /* This thread is uncertain */
2042         }
2043
2044         if (certain) {
2045                 release_heads->push_back(release);
2046                 pending->writes.clear();
2047         } else {
2048                 pending->release = release;
2049                 pending->rf = rf;
2050         }
2051         return certain;
2052 }
2053
2054 /**
2055  * An interface for getting the release sequence head(s) with which a
2056  * given ModelAction must synchronize. This function only returns a non-empty
2057  * result when it can locate a release sequence head with certainty. Otherwise,
2058  * it may mark the internal state of the ModelChecker so that it will handle
2059  * the release sequence at a later time, causing @a acquire to update its
2060  * synchronization at some later point in execution.
2061  *
2062  * @param acquire The 'acquire' action that may synchronize with a release
2063  * sequence
2064  * @param read The read action that may read from a release sequence; this may
2065  * be the same as acquire, or else an earlier action in the same thread (i.e.,
2066  * when 'acquire' is a fence-acquire)
2067  * @param release_heads A pass-by-reference return parameter. Will be filled
2068  * with the head(s) of the release sequence(s), if they exists with certainty.
2069  * @see ModelChecker::release_seq_heads
2070  */
2071 void ModelChecker::get_release_seq_heads(ModelAction *acquire,
2072                 ModelAction *read, rel_heads_list_t *release_heads)
2073 {
2074         const ModelAction *rf = read->get_reads_from();
2075         struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
2076         sequence->acquire = acquire;
2077         sequence->read = read;
2078
2079         if (!release_seq_heads(rf, release_heads, sequence)) {
2080                 /* add act to 'lazy checking' list */
2081                 pending_rel_seqs->push_back(sequence);
2082         } else {
2083                 snapshot_free(sequence);
2084         }
2085 }
2086
2087 /**
2088  * Attempt to resolve all stashed operations that might synchronize with a
2089  * release sequence for a given location. This implements the "lazy" portion of
2090  * determining whether or not a release sequence was contiguous, since not all
2091  * modification order information is present at the time an action occurs.
2092  *
2093  * @param location The location/object that should be checked for release
2094  * sequence resolutions. A NULL value means to check all locations.
2095  * @param work_queue The work queue to which to add work items as they are
2096  * generated
2097  * @return True if any updates occurred (new synchronization, new mo_graph
2098  * edges)
2099  */
2100 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
2101 {
2102         bool updated = false;
2103         std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
2104         while (it != pending_rel_seqs->end()) {
2105                 struct release_seq *pending = *it;
2106                 ModelAction *acquire = pending->acquire;
2107                 const ModelAction *read = pending->read;
2108
2109                 /* Only resolve sequences on the given location, if provided */
2110                 if (location && read->get_location() != location) {
2111                         it++;
2112                         continue;
2113                 }
2114
2115                 const ModelAction *rf = read->get_reads_from();
2116                 rel_heads_list_t release_heads;
2117                 bool complete;
2118                 complete = release_seq_heads(rf, &release_heads, pending);
2119                 for (unsigned int i = 0; i < release_heads.size(); i++) {
2120                         if (!acquire->has_synchronized_with(release_heads[i])) {
2121                                 if (acquire->synchronize_with(release_heads[i]))
2122                                         updated = true;
2123                                 else
2124                                         set_bad_synchronization();
2125                         }
2126                 }
2127
2128                 if (updated) {
2129                         /* Re-check all pending release sequences */
2130                         work_queue->push_back(CheckRelSeqWorkEntry(NULL));
2131                         /* Re-check read-acquire for mo_graph edges */
2132                         if (acquire->is_read())
2133                                 work_queue->push_back(MOEdgeWorkEntry(acquire));
2134
2135                         /* propagate synchronization to later actions */
2136                         action_list_t::reverse_iterator rit = action_trace->rbegin();
2137                         for (; (*rit) != acquire; rit++) {
2138                                 ModelAction *propagate = *rit;
2139                                 if (acquire->happens_before(propagate)) {
2140                                         propagate->synchronize_with(acquire);
2141                                         /* Re-check 'propagate' for mo_graph edges */
2142                                         work_queue->push_back(MOEdgeWorkEntry(propagate));
2143                                 }
2144                         }
2145                 }
2146                 if (complete) {
2147                         it = pending_rel_seqs->erase(it);
2148                         snapshot_free(pending);
2149                 } else {
2150                         it++;
2151                 }
2152         }
2153
2154         // If we resolved promises or data races, see if we have realized a data race.
2155         checkDataRaces();
2156
2157         return updated;
2158 }
2159
2160 /**
2161  * Performs various bookkeeping operations for the current ModelAction. For
2162  * instance, adds action to the per-object, per-thread action vector and to the
2163  * action trace list of all thread actions.
2164  *
2165  * @param act is the ModelAction to add.
2166  */
2167 void ModelChecker::add_action_to_lists(ModelAction *act)
2168 {
2169         int tid = id_to_int(act->get_tid());
2170         ModelAction *uninit = NULL;
2171         int uninit_id = -1;
2172         action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
2173         if (list->empty() && act->is_atomic_var()) {
2174                 uninit = new_uninitialized_action(act->get_location());
2175                 uninit_id = id_to_int(uninit->get_tid());
2176                 list->push_back(uninit);
2177         }
2178         list->push_back(act);
2179
2180         action_trace->push_back(act);
2181         if (uninit)
2182                 action_trace->push_front(uninit);
2183
2184         std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
2185         if (tid >= (int)vec->size())
2186                 vec->resize(priv->next_thread_id);
2187         (*vec)[tid].push_back(act);
2188         if (uninit)
2189                 (*vec)[uninit_id].push_front(uninit);
2190
2191         if ((int)thrd_last_action->size() <= tid)
2192                 thrd_last_action->resize(get_num_threads());
2193         (*thrd_last_action)[tid] = act;
2194         if (uninit)
2195                 (*thrd_last_action)[uninit_id] = uninit;
2196
2197         if (act->is_fence() && act->is_release()) {
2198                 if ((int)thrd_last_fence_release->size() <= tid)
2199                         thrd_last_fence_release->resize(get_num_threads());
2200                 (*thrd_last_fence_release)[tid] = act;
2201         }
2202
2203         if (act->is_wait()) {
2204                 void *mutex_loc = (void *) act->get_value();
2205                 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
2206
2207                 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
2208                 if (tid >= (int)vec->size())
2209                         vec->resize(priv->next_thread_id);
2210                 (*vec)[tid].push_back(act);
2211         }
2212 }
2213
2214 /**
2215  * @brief Get the last action performed by a particular Thread
2216  * @param tid The thread ID of the Thread in question
2217  * @return The last action in the thread
2218  */
2219 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
2220 {
2221         int threadid = id_to_int(tid);
2222         if (threadid < (int)thrd_last_action->size())
2223                 return (*thrd_last_action)[id_to_int(tid)];
2224         else
2225                 return NULL;
2226 }
2227
2228 /**
2229  * @brief Get the last fence release performed by a particular Thread
2230  * @param tid The thread ID of the Thread in question
2231  * @return The last fence release in the thread, if one exists; NULL otherwise
2232  */
2233 ModelAction * ModelChecker::get_last_fence_release(thread_id_t tid) const
2234 {
2235         int threadid = id_to_int(tid);
2236         if (threadid < (int)thrd_last_fence_release->size())
2237                 return (*thrd_last_fence_release)[id_to_int(tid)];
2238         else
2239                 return NULL;
2240 }
2241
2242 /**
2243  * Gets the last memory_order_seq_cst write (in the total global sequence)
2244  * performed on a particular object (i.e., memory location), not including the
2245  * current action.
2246  * @param curr The current ModelAction; also denotes the object location to
2247  * check
2248  * @return The last seq_cst write
2249  */
2250 ModelAction * ModelChecker::get_last_seq_cst_write(ModelAction *curr) const
2251 {
2252         void *location = curr->get_location();
2253         action_list_t *list = get_safe_ptr_action(obj_map, location);
2254         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
2255         action_list_t::reverse_iterator rit;
2256         for (rit = list->rbegin(); rit != list->rend(); rit++)
2257                 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
2258                         return *rit;
2259         return NULL;
2260 }
2261
2262 /**
2263  * Gets the last memory_order_seq_cst fence (in the total global sequence)
2264  * performed in a particular thread, prior to a particular fence.
2265  * @param tid The ID of the thread to check
2266  * @param before_fence The fence from which to begin the search; if NULL, then
2267  * search for the most recent fence in the thread.
2268  * @return The last prior seq_cst fence in the thread, if exists; otherwise, NULL
2269  */
2270 ModelAction * ModelChecker::get_last_seq_cst_fence(thread_id_t tid, const ModelAction *before_fence) const
2271 {
2272         /* All fences should have NULL location */
2273         action_list_t *list = get_safe_ptr_action(obj_map, NULL);
2274         action_list_t::reverse_iterator rit = list->rbegin();
2275
2276         if (before_fence) {
2277                 for (; rit != list->rend(); rit++)
2278                         if (*rit == before_fence)
2279                                 break;
2280
2281                 ASSERT(*rit == before_fence);
2282                 rit++;
2283         }
2284
2285         for (; rit != list->rend(); rit++)
2286                 if ((*rit)->is_fence() && (tid == (*rit)->get_tid()) && (*rit)->is_seqcst())
2287                         return *rit;
2288         return NULL;
2289 }
2290
2291 /**
2292  * Gets the last unlock operation performed on a particular mutex (i.e., memory
2293  * location). This function identifies the mutex according to the current
2294  * action, which is presumed to perform on the same mutex.
2295  * @param curr The current ModelAction; also denotes the object location to
2296  * check
2297  * @return The last unlock operation
2298  */
2299 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
2300 {
2301         void *location = curr->get_location();
2302         action_list_t *list = get_safe_ptr_action(obj_map, location);
2303         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
2304         action_list_t::reverse_iterator rit;
2305         for (rit = list->rbegin(); rit != list->rend(); rit++)
2306                 if ((*rit)->is_unlock() || (*rit)->is_wait())
2307                         return *rit;
2308         return NULL;
2309 }
2310
2311 ModelAction * ModelChecker::get_parent_action(thread_id_t tid) const
2312 {
2313         ModelAction *parent = get_last_action(tid);
2314         if (!parent)
2315                 parent = get_thread(tid)->get_creation();
2316         return parent;
2317 }
2318
2319 /**
2320  * Returns the clock vector for a given thread.
2321  * @param tid The thread whose clock vector we want
2322  * @return Desired clock vector
2323  */
2324 ClockVector * ModelChecker::get_cv(thread_id_t tid) const
2325 {
2326         return get_parent_action(tid)->get_cv();
2327 }
2328
2329 /**
2330  * Resolve a set of Promises with a current write. The set is provided in the
2331  * Node corresponding to @a write.
2332  * @param write The ModelAction that is fulfilling Promises
2333  * @return True if promises were resolved; false otherwise
2334  */
2335 bool ModelChecker::resolve_promises(ModelAction *write)
2336 {
2337         bool resolved = false;
2338         std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
2339
2340         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
2341                 Promise *promise = (*promises)[promise_index];
2342                 if (write->get_node()->get_promise(i)) {
2343                         ModelAction *read = promise->get_action();
2344                         if (read->is_rmw()) {
2345                                 mo_graph->addRMWEdge(write, read);
2346                         }
2347                         read_from(read, write);
2348                         //First fix up the modification order for actions that happened
2349                         //before the read
2350                         r_modification_order(read, write);
2351                         //Next fix up the modification order for actions that happened
2352                         //after the read.
2353                         post_r_modification_order(read, write);
2354                         //Make sure the promise's value matches the write's value
2355                         ASSERT(promise->get_value() == write->get_value());
2356                         delete(promise);
2357
2358                         promises->erase(promises->begin() + promise_index);
2359                         actions_to_check.push_back(read);
2360
2361                         resolved = true;
2362                 } else
2363                         promise_index++;
2364         }
2365
2366         //Check whether reading these writes has made threads unable to
2367         //resolve promises
2368
2369         for (unsigned int i = 0; i < actions_to_check.size(); i++) {
2370                 ModelAction *read=actions_to_check[i];
2371                 mo_check_promises(read->get_tid(), write, read);
2372         }
2373
2374         return resolved;
2375 }
2376
2377 /**
2378  * Compute the set of promises that could potentially be satisfied by this
2379  * action. Note that the set computation actually appears in the Node, not in
2380  * ModelChecker.
2381  * @param curr The ModelAction that may satisfy promises
2382  */
2383 void ModelChecker::compute_promises(ModelAction *curr)
2384 {
2385         for (unsigned int i = 0; i < promises->size(); i++) {
2386                 Promise *promise = (*promises)[i];
2387                 const ModelAction *act = promise->get_action();
2388                 if (!act->happens_before(curr) &&
2389                                 act->is_read() &&
2390                                 !act->could_synchronize_with(curr) &&
2391                                 !act->same_thread(curr) &&
2392                                 act->get_location() == curr->get_location() &&
2393                                 promise->get_value() == curr->get_value()) {
2394                         curr->get_node()->set_promise(i, act->is_rmw());
2395                 }
2396         }
2397 }
2398
2399 /** Checks promises in response to change in ClockVector Threads. */
2400 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2401 {
2402         for (unsigned int i = 0; i < promises->size(); i++) {
2403                 Promise *promise = (*promises)[i];
2404                 const ModelAction *act = promise->get_action();
2405                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2406                                 merge_cv->synchronized_since(act)) {
2407                         if (promise->eliminate_thread(tid)) {
2408                                 //Promise has failed
2409                                 priv->failed_promise = true;
2410                                 return;
2411                         }
2412                 }
2413         }
2414 }
2415
2416 void ModelChecker::check_promises_thread_disabled()
2417 {
2418         for (unsigned int i = 0; i < promises->size(); i++) {
2419                 Promise *promise = (*promises)[i];
2420                 if (promise->has_failed()) {
2421                         priv->failed_promise = true;
2422                         return;
2423                 }
2424         }
2425 }
2426
2427 /**
2428  * @brief Checks promises in response to addition to modification order for
2429  * threads.
2430  *
2431  * Definitions:
2432  *
2433  * pthread is the thread that performed the read that created the promise
2434  *
2435  * pread is the read that created the promise
2436  *
2437  * pwrite is either the first write to same location as pread by
2438  * pthread that is sequenced after pread or the write read by the
2439  * first read to the same location as pread by pthread that is
2440  * sequenced after pread.
2441  *
2442  * 1. If tid=pthread, then we check what other threads are reachable
2443  * through the mod order starting with pwrite.  Those threads cannot
2444  * perform a write that will resolve the promise due to modification
2445  * order constraints.
2446  *
2447  * 2. If the tid is not pthread, we check whether pwrite can reach the
2448  * action write through the modification order.  If so, that thread
2449  * cannot perform a future write that will resolve the promise due to
2450  * modificatin order constraints.
2451  *
2452  * @param tid The thread that either read from the model action write, or
2453  * actually did the model action write.
2454  *
2455  * @param write The ModelAction representing the relevant write.
2456  * @param read  The ModelAction that reads a promised write, or NULL otherwise.
2457  */
2458 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
2459 {
2460         void *location = write->get_location();
2461         for (unsigned int i = 0; i < promises->size(); i++) {
2462                 Promise *promise = (*promises)[i];
2463                 const ModelAction *act = promise->get_action();
2464
2465                 // Is this promise on the same location?
2466                 if (act->get_location() != location)
2467                         continue;
2468
2469                 // same thread as the promise
2470                 if (act->get_tid() == tid) {
2471                         // make sure that the reader of this write happens after the promise
2472                         if ((read == NULL) || (promise->get_action()->happens_before(read))) {
2473                                 // do we have a pwrite for the promise, if not, set it
2474                                 if (promise->get_write() == NULL) {
2475                                         promise->set_write(write);
2476                                         // The pwrite cannot happen before the promise
2477                                         if (write->happens_before(act) && (write != act)) {
2478                                                 priv->failed_promise = true;
2479                                                 return;
2480                                         }
2481                                 }
2482
2483                                 if (mo_graph->checkPromise(write, promise)) {
2484                                         priv->failed_promise = true;
2485                                         return;
2486                                 }
2487                         }
2488                 }
2489
2490                 // Don't do any lookups twice for the same thread
2491                 if (!promise->thread_is_available(tid))
2492                         continue;
2493
2494                 if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
2495                         if (promise->eliminate_thread(tid)) {
2496                                 priv->failed_promise = true;
2497                                 return;
2498                         }
2499                 }
2500         }
2501 }
2502
2503 /**
2504  * Compute the set of writes that may break the current pending release
2505  * sequence. This information is extracted from previou release sequence
2506  * calculations.
2507  *
2508  * @param curr The current ModelAction. Must be a release sequence fixup
2509  * action.
2510  */
2511 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2512 {
2513         if (pending_rel_seqs->empty())
2514                 return;
2515
2516         struct release_seq *pending = pending_rel_seqs->back();
2517         for (unsigned int i = 0; i < pending->writes.size(); i++) {
2518                 const ModelAction *write = pending->writes[i];
2519                 curr->get_node()->add_relseq_break(write);
2520         }
2521
2522         /* NULL means don't break the sequence; just synchronize */
2523         curr->get_node()->add_relseq_break(NULL);
2524 }
2525
2526 /**
2527  * Build up an initial set of all past writes that this 'read' action may read
2528  * from. This set is determined by the clock vector's "happens before"
2529  * relationship.
2530  * @param curr is the current ModelAction that we are exploring; it must be a
2531  * 'read' operation.
2532  */
2533 void ModelChecker::build_reads_from_past(ModelAction *curr)
2534 {
2535         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2536         unsigned int i;
2537         ASSERT(curr->is_read());
2538
2539         ModelAction *last_sc_write = NULL;
2540
2541         if (curr->is_seqcst())
2542                 last_sc_write = get_last_seq_cst_write(curr);
2543
2544         /* Iterate over all threads */
2545         for (i = 0; i < thrd_lists->size(); i++) {
2546                 /* Iterate over actions in thread, starting from most recent */
2547                 action_list_t *list = &(*thrd_lists)[i];
2548                 action_list_t::reverse_iterator rit;
2549                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2550                         ModelAction *act = *rit;
2551
2552                         /* Only consider 'write' actions */
2553                         if (!act->is_write() || act == curr)
2554                                 continue;
2555
2556                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2557                         bool allow_read = true;
2558
2559                         if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write)
2560                                 allow_read = false;
2561                         else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
2562                                 allow_read = false;
2563
2564                         if (allow_read)
2565                                 curr->get_node()->add_read_from(act);
2566
2567                         /* Include at most one act per-thread that "happens before" curr */
2568                         if (act->happens_before(curr))
2569                                 break;
2570                 }
2571         }
2572
2573         if (DBG_ENABLED()) {
2574                 model_print("Reached read action:\n");
2575                 curr->print();
2576                 model_print("Printing may_read_from\n");
2577                 curr->get_node()->print_may_read_from();
2578                 model_print("End printing may_read_from\n");
2579         }
2580 }
2581
2582 bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
2583 {
2584         while (true) {
2585                 /* UNINIT actions don't have a Node, and they never sleep */
2586                 if (write->is_uninitialized())
2587                         return true;
2588                 Node *prevnode = write->get_node()->get_parent();
2589
2590                 bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
2591                 if (write->is_release() && thread_sleep)
2592                         return true;
2593                 if (!write->is_rmw()) {
2594                         return false;
2595                 }
2596                 if (write->get_reads_from() == NULL)
2597                         return true;
2598                 write = write->get_reads_from();
2599         }
2600 }
2601
2602 /**
2603  * @brief Create a new action representing an uninitialized atomic
2604  * @param location The memory location of the atomic object
2605  * @return A pointer to a new ModelAction
2606  */
2607 ModelAction * ModelChecker::new_uninitialized_action(void *location) const
2608 {
2609         ModelAction *act = (ModelAction *)snapshot_malloc(sizeof(class ModelAction));
2610         act = new (act) ModelAction(ATOMIC_UNINIT, std::memory_order_relaxed, location, 0, model_thread);
2611         act->create_cv(NULL);
2612         return act;
2613 }
2614
2615 static void print_list(action_list_t *list)
2616 {
2617         action_list_t::iterator it;
2618
2619         model_print("---------------------------------------------------------------------\n");
2620
2621         unsigned int hash = 0;
2622
2623         for (it = list->begin(); it != list->end(); it++) {
2624                 (*it)->print();
2625                 hash = hash^(hash<<3)^((*it)->hash());
2626         }
2627         model_print("HASH %u\n", hash);
2628         model_print("---------------------------------------------------------------------\n");
2629 }
2630
2631 #if SUPPORT_MOD_ORDER_DUMP
2632 void ModelChecker::dumpGraph(char *filename) const
2633 {
2634         char buffer[200];
2635         sprintf(buffer, "%s.dot", filename);
2636         FILE *file = fopen(buffer, "w");
2637         fprintf(file, "digraph %s {\n", filename);
2638         mo_graph->dumpNodes(file);
2639         ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
2640
2641         for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2642                 ModelAction *action = *it;
2643                 if (action->is_read()) {
2644                         fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
2645                         if (action->get_reads_from() != NULL)
2646                                 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2647                 }
2648                 if (thread_array[action->get_tid()] != NULL) {
2649                         fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2650                 }
2651
2652                 thread_array[action->get_tid()] = action;
2653         }
2654         fprintf(file, "}\n");
2655         model_free(thread_array);
2656         fclose(file);
2657 }
2658 #endif
2659
2660 /** @brief Prints an execution trace summary. */
2661 void ModelChecker::print_summary() const
2662 {
2663 #if SUPPORT_MOD_ORDER_DUMP
2664         scheduler->print();
2665         char buffername[100];
2666         sprintf(buffername, "exec%04u", stats.num_total);
2667         mo_graph->dumpGraphToFile(buffername);
2668         sprintf(buffername, "graph%04u", stats.num_total);
2669         dumpGraph(buffername);
2670 #endif
2671
2672         model_print("Execution %d:", stats.num_total);
2673         if (isfeasibleprefix())
2674                 model_print("\n");
2675         else
2676                 print_infeasibility(" INFEASIBLE");
2677         print_list(action_trace);
2678         model_print("\n");
2679 }
2680
2681 /**
2682  * Add a Thread to the system for the first time. Should only be called once
2683  * per thread.
2684  * @param t The Thread to add
2685  */
2686 void ModelChecker::add_thread(Thread *t)
2687 {
2688         thread_map->put(id_to_int(t->get_id()), t);
2689         scheduler->add_thread(t);
2690 }
2691
2692 /**
2693  * Removes a thread from the scheduler.
2694  * @param the thread to remove.
2695  */
2696 void ModelChecker::remove_thread(Thread *t)
2697 {
2698         scheduler->remove_thread(t);
2699 }
2700
2701 /**
2702  * @brief Get a Thread reference by its ID
2703  * @param tid The Thread's ID
2704  * @return A Thread reference
2705  */
2706 Thread * ModelChecker::get_thread(thread_id_t tid) const
2707 {
2708         return thread_map->get(id_to_int(tid));
2709 }
2710
2711 /**
2712  * @brief Get a reference to the Thread in which a ModelAction was executed
2713  * @param act The ModelAction
2714  * @return A Thread reference
2715  */
2716 Thread * ModelChecker::get_thread(const ModelAction *act) const
2717 {
2718         return get_thread(act->get_tid());
2719 }
2720
2721 /**
2722  * @brief Check if a Thread is currently enabled
2723  * @param t The Thread to check
2724  * @return True if the Thread is currently enabled
2725  */
2726 bool ModelChecker::is_enabled(Thread *t) const
2727 {
2728         return scheduler->is_enabled(t);
2729 }
2730
2731 /**
2732  * @brief Check if a Thread is currently enabled
2733  * @param tid The ID of the Thread to check
2734  * @return True if the Thread is currently enabled
2735  */
2736 bool ModelChecker::is_enabled(thread_id_t tid) const
2737 {
2738         return scheduler->is_enabled(tid);
2739 }
2740
2741 /**
2742  * Switch from a user-context to the "master thread" context (a.k.a. system
2743  * context). This switch is made with the intention of exploring a particular
2744  * model-checking action (described by a ModelAction object). Must be called
2745  * from a user-thread context.
2746  *
2747  * @param act The current action that will be explored. May be NULL only if
2748  * trace is exiting via an assertion (see ModelChecker::set_assert and
2749  * ModelChecker::has_asserted).
2750  * @return Return the value returned by the current action
2751  */
2752 uint64_t ModelChecker::switch_to_master(ModelAction *act)
2753 {
2754         DBG();
2755         Thread *old = thread_current();
2756         set_current_action(act);
2757         old->set_state(THREAD_READY);
2758         if (Thread::swap(old, &system_context) < 0) {
2759                 perror("swap threads");
2760                 exit(EXIT_FAILURE);
2761         }
2762         return old->get_return_value();
2763 }
2764
2765 /**
2766  * Takes the next step in the execution, if possible.
2767  * @param curr The current step to take
2768  * @return Returns true (success) if a step was taken and false otherwise.
2769  */
2770 bool ModelChecker::take_step(ModelAction *curr)
2771 {
2772         if (has_asserted())
2773                 return false;
2774
2775         Thread *curr_thrd = get_thread(curr);
2776         ASSERT(curr_thrd->get_state() == THREAD_READY);
2777
2778         curr = check_current_action(curr);
2779
2780         /* Infeasible -> don't take any more steps */
2781         if (is_infeasible())
2782                 return false;
2783         else if (isfeasibleprefix() && have_bug_reports()) {
2784                 set_assert();
2785                 return false;
2786         }
2787
2788         if (params.bound != 0)
2789                 if (priv->used_sequence_numbers > params.bound)
2790                         return false;
2791
2792         if (curr_thrd->is_blocked() || curr_thrd->is_complete())
2793                 scheduler->remove_thread(curr_thrd);
2794
2795         Thread *next_thrd = get_next_thread(curr);
2796         next_thrd = scheduler->next_thread(next_thrd);
2797
2798         DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
2799                         next_thrd ? id_to_int(next_thrd->get_id()) : -1);
2800
2801         /*
2802          * Launch end-of-execution release sequence fixups only when there are:
2803          *
2804          * (1) no more user threads to run (or when execution replay chooses
2805          *     the 'model_thread')
2806          * (2) pending release sequences
2807          * (3) pending assertions (i.e., data races)
2808          * (4) no pending promises
2809          */
2810         if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
2811                         is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
2812                 model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2813                                 pending_rel_seqs->size());
2814                 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2815                                 std::memory_order_seq_cst, NULL, VALUE_NONE,
2816                                 model_thread);
2817                 set_current_action(fixup);
2818                 return true;
2819         }
2820
2821         /* next_thrd == NULL -> don't take any more steps */
2822         if (!next_thrd)
2823                 return false;
2824
2825         next_thrd->set_state(THREAD_RUNNING);
2826
2827         if (next_thrd->get_pending() != NULL) {
2828                 /* restart a pending action */
2829                 set_current_action(next_thrd->get_pending());
2830                 next_thrd->set_pending(NULL);
2831                 next_thrd->set_state(THREAD_READY);
2832                 return true;
2833         }
2834
2835         /* Return false only if swap fails with an error */
2836         return (Thread::swap(&system_context, next_thrd) == 0);
2837 }
2838
2839 /** Wrapper to run the user's main function, with appropriate arguments */
2840 void user_main_wrapper(void *)
2841 {
2842         user_main(model->params.argc, model->params.argv);
2843 }
2844
2845 /** @brief Run ModelChecker for the user program */
2846 void ModelChecker::run()
2847 {
2848         do {
2849                 thrd_t user_thread;
2850                 Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
2851
2852                 add_thread(t);
2853
2854                 /* Run user thread up to its first action */
2855                 scheduler->next_thread(t);
2856                 Thread::swap(&system_context, t);
2857
2858                 /* Wait for all threads to complete */
2859                 while (take_step(priv->current_action));
2860         } while (next_execution());
2861
2862         print_stats();
2863 }