model.cc

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