model.cc

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