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