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                 checkDataRaces();
 450                 print_bugs();
 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         checkDataRaces();
 921 }
 922
 923 /**
 924  * Initialize the current action by performing one or more of the following
 925  * actions, as appropriate: merging RMWR and RMWC/RMW actions, stepping forward
 926  * in the NodeStack, manipulating backtracking sets, allocating and
 927  * initializing clock vectors, and computing the promises to fulfill.
 928  *
 929  * @param curr The current action, as passed from the user context; may be
 930  * freed/invalidated after the execution of this function, with a different
 931  * action "returned" its place (pass-by-reference)
 932  * @return True if curr is a newly-explored action; false otherwise
 933  */
 934 bool ModelChecker::initialize_curr_action(ModelAction **curr)
 935 {
 936         ModelAction *newcurr;
 937
 938         if ((*curr)->is_rmwc() || (*curr)->is_rmw()) {
 939                 newcurr = process_rmw(*curr);
 940                 delete *curr;
 941
 942                 if (newcurr->is_rmw())
 943                         compute_promises(newcurr);
 944
 945                 *curr = newcurr;
 946                 return false;
 947         }
 948
 949         (*curr)->set_seq_number(get_next_seq_num());
 950
 951         newcurr = node_stack->explore_action(*curr, scheduler->get_enabled());
 952         if (newcurr) {
 953                 /* First restore type and order in case of RMW operation */
 954                 if ((*curr)->is_rmwr())
 955                         newcurr->copy_typeandorder(*curr);
 956
 957                 ASSERT((*curr)->get_location() == newcurr->get_location());
 958                 newcurr->copy_from_new(*curr);
 959
 960                 /* Discard duplicate ModelAction; use action from NodeStack */
 961                 delete *curr;
 962
 963                 /* Always compute new clock vector */
 964                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 965
 966                 *curr = newcurr;
 967                 return false; /* Action was explored previously */
 968         } else {
 969                 newcurr = *curr;
 970
 971                 /* Always compute new clock vector */
 972                 newcurr->create_cv(get_parent_action(newcurr->get_tid()));
 973                 /*
 974                  * Perform one-time actions when pushing new ModelAction onto
 975                  * NodeStack
 976                  */
 977                 if (newcurr->is_write())
 978                         compute_promises(newcurr);
 979                 else if (newcurr->is_relseq_fixup())
 980                         compute_relseq_breakwrites(newcurr);
 981                 else if (newcurr->is_wait())
 982                         newcurr->get_node()->set_misc_max(2);
 983                 else if (newcurr->is_notify_one()) {
 984                         newcurr->get_node()->set_misc_max(get_safe_ptr_action(condvar_waiters_map, newcurr->get_location())->size());
 985                 }
 986                 return true; /* This was a new ModelAction */
 987         }
 988 }
 989
 990 /**
 991  * @brief Check whether a model action is enabled.
 992  *
 993  * Checks whether a lock or join operation would be successful (i.e., is the
 994  * lock already locked, or is the joined thread already complete). If not, put
 995  * the action in a waiter list.
 996  *
 997  * @param curr is the ModelAction to check whether it is enabled.
 998  * @return a bool that indicates whether the action is enabled.
 999  */
1000 bool ModelChecker::check_action_enabled(ModelAction *curr) {
1001         if (curr->is_lock()) {
1002                 std::mutex * lock = (std::mutex *)curr->get_location();
1003                 struct std::mutex_state * state = lock->get_state();
1004                 if (state->islocked) {
1005                         //Stick the action in the appropriate waiting queue
1006                         get_safe_ptr_action(lock_waiters_map, curr->get_location())->push_back(curr);
1007                         return false;
1008                 }
1009         } else if (curr->get_type() == THREAD_JOIN) {
1010                 Thread *blocking = (Thread *)curr->get_location();
1011                 if (!blocking->is_complete()) {
1012                         blocking->push_wait_list(curr);
1013                         return false;
1014                 }
1015         }
1016
1017         return true;
1018 }
1019
1020 /**
1021  * Stores the ModelAction for the current thread action.  Call this
1022  * immediately before switching from user- to system-context to pass
1023  * data between them.
1024  * @param act The ModelAction created by the user-thread action
1025  */
1026 void ModelChecker::set_current_action(ModelAction *act) {
1027         priv->current_action = act;
1028 }
1029
1030 /**
1031  * This is the heart of the model checker routine. It performs model-checking
1032  * actions corresponding to a given "current action." Among other processes, it
1033  * calculates reads-from relationships, updates synchronization clock vectors,
1034  * forms a memory_order constraints graph, and handles replay/backtrack
1035  * execution when running permutations of previously-observed executions.
1036  *
1037  * @param curr The current action to process
1038  * @return The next Thread that must be executed. May be NULL if ModelChecker
1039  * makes no choice (e.g., according to replay execution, combining RMW actions,
1040  * etc.)
1041  */
1042 Thread * ModelChecker::check_current_action(ModelAction *curr)
1043 {
1044         ASSERT(curr);
1045         bool second_part_of_rmw = curr->is_rmwc() || curr->is_rmw();
1046
1047         if (!check_action_enabled(curr)) {
1048                 /* Make the execution look like we chose to run this action
1049                  * much later, when a lock/join can succeed */
1050                 get_current_thread()->set_pending(curr);
1051                 scheduler->sleep(get_current_thread());
1052                 return get_next_thread(NULL);
1053         }
1054
1055         bool newly_explored = initialize_curr_action(&curr);
1056
1057         wake_up_sleeping_actions(curr);
1058
1059         /* Add the action to lists before any other model-checking tasks */
1060         if (!second_part_of_rmw)
1061                 add_action_to_lists(curr);
1062
1063         /* Build may_read_from set for newly-created actions */
1064         if (newly_explored && curr->is_read())
1065                 build_reads_from_past(curr);
1066
1067         /* Initialize work_queue with the "current action" work */
1068         work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
1069         while (!work_queue.empty() && !has_asserted()) {
1070                 WorkQueueEntry work = work_queue.front();
1071                 work_queue.pop_front();
1072
1073                 switch (work.type) {
1074                 case WORK_CHECK_CURR_ACTION: {
1075                         ModelAction *act = work.action;
1076                         bool update = false; /* update this location's release seq's */
1077                         bool update_all = false; /* update all release seq's */
1078
1079                         if (process_thread_action(curr))
1080                                 update_all = true;
1081
1082                         if (act->is_read() && process_read(act, second_part_of_rmw))
1083                                 update = true;
1084
1085                         if (act->is_write() && process_write(act))
1086                                 update = true;
1087
1088                         if (act->is_mutex_op() && process_mutex(act))
1089                                 update_all = true;
1090
1091                         if (act->is_relseq_fixup())
1092                                 process_relseq_fixup(curr, &work_queue);
1093
1094                         if (update_all)
1095                                 work_queue.push_back(CheckRelSeqWorkEntry(NULL));
1096                         else if (update)
1097                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1098                         break;
1099                 }
1100                 case WORK_CHECK_RELEASE_SEQ:
1101                         resolve_release_sequences(work.location, &work_queue);
1102                         break;
1103                 case WORK_CHECK_MO_EDGES: {
1104                         /** @todo Complete verification of work_queue */
1105                         ModelAction *act = work.action;
1106                         bool updated = false;
1107
1108                         if (act->is_read()) {
1109                                 const ModelAction *rf = act->get_reads_from();
1110                                 if (rf != NULL && r_modification_order(act, rf))
1111                                         updated = true;
1112                         }
1113                         if (act->is_write()) {
1114                                 if (w_modification_order(act))
1115                                         updated = true;
1116                         }
1117                         mo_graph->commitChanges();
1118
1119                         if (updated)
1120                                 work_queue.push_back(CheckRelSeqWorkEntry(act->get_location()));
1121                         break;
1122                 }
1123                 default:
1124                         ASSERT(false);
1125                         break;
1126                 }
1127         }
1128
1129         check_curr_backtracking(curr);
1130         set_backtracking(curr);
1131         return get_next_thread(curr);
1132 }
1133
1134 void ModelChecker::check_curr_backtracking(ModelAction * curr) {
1135         Node *currnode = curr->get_node();
1136         Node *parnode = currnode->get_parent();
1137
1138         if ((!parnode->backtrack_empty() ||
1139                          !currnode->misc_empty() ||
1140                          !currnode->read_from_empty() ||
1141                          !currnode->future_value_empty() ||
1142                          !currnode->promise_empty() ||
1143                          !currnode->relseq_break_empty())
1144                         && (!priv->next_backtrack ||
1145                                         *curr > *priv->next_backtrack)) {
1146                 priv->next_backtrack = curr;
1147         }
1148 }
1149
1150 bool ModelChecker::promises_expired() const
1151 {
1152         for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
1153                 Promise *promise = (*promises)[promise_index];
1154                 if (promise->get_expiration()<priv->used_sequence_numbers) {
1155                         return true;
1156                 }
1157         }
1158         return false;
1159 }
1160
1161 /** @return whether the current partial trace must be a prefix of a
1162  * feasible trace. */
1163 bool ModelChecker::isfeasibleprefix() const
1164 {
1165         return promises->size() == 0 && pending_rel_seqs->size() == 0 && isfeasible();
1166 }
1167
1168 /** @return whether the current partial trace is feasible. */
1169 bool ModelChecker::isfeasible() const
1170 {
1171         if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
1172                 DEBUG("Infeasible: RMW violation\n");
1173
1174         return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
1175 }
1176
1177 /** @return whether the current partial trace is feasible other than
1178  * multiple RMW reading from the same store. */
1179 bool ModelChecker::isfeasibleotherthanRMW() const
1180 {
1181         if (DBG_ENABLED()) {
1182                 if (mo_graph->checkForCycles())
1183                         DEBUG("Infeasible: modification order cycles\n");
1184                 if (failed_promise)
1185                         DEBUG("Infeasible: failed promise\n");
1186                 if (too_many_reads)
1187                         DEBUG("Infeasible: too many reads\n");
1188                 if (bad_synchronization)
1189                         DEBUG("Infeasible: bad synchronization ordering\n");
1190                 if (promises_expired())
1191                         DEBUG("Infeasible: promises expired\n");
1192         }
1193         return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !bad_synchronization && !promises_expired();
1194 }
1195
1196 /** Returns whether the current completed trace is feasible. */
1197 bool ModelChecker::isfinalfeasible() const
1198 {
1199         if (DBG_ENABLED() && promises->size() != 0)
1200                 DEBUG("Infeasible: unrevolved promises\n");
1201
1202         return isfeasible() && promises->size() == 0;
1203 }
1204
1205 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
1206 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
1207         ModelAction *lastread = get_last_action(act->get_tid());
1208         lastread->process_rmw(act);
1209         if (act->is_rmw() && lastread->get_reads_from()!=NULL) {
1210                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
1211                 mo_graph->commitChanges();
1212         }
1213         return lastread;
1214 }
1215
1216 /**
1217  * Checks whether a thread has read from the same write for too many times
1218  * without seeing the effects of a later write.
1219  *
1220  * Basic idea:
1221  * 1) there must a different write that we could read from that would satisfy the modification order,
1222  * 2) we must have read from the same value in excess of maxreads times, and
1223  * 3) that other write must have been in the reads_from set for maxreads times.
1224  *
1225  * If so, we decide that the execution is no longer feasible.
1226  */
1227 void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) {
1228         if (params.maxreads != 0) {
1229
1230                 if (curr->get_node()->get_read_from_size() <= 1)
1231                         return;
1232                 //Must make sure that execution is currently feasible...  We could
1233                 //accidentally clear by rolling back
1234                 if (!isfeasible())
1235                         return;
1236                 std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1237                 int tid = id_to_int(curr->get_tid());
1238
1239                 /* Skip checks */
1240                 if ((int)thrd_lists->size() <= tid)
1241                         return;
1242                 action_list_t *list = &(*thrd_lists)[tid];
1243
1244                 action_list_t::reverse_iterator rit = list->rbegin();
1245                 /* Skip past curr */
1246                 for (; (*rit) != curr; rit++)
1247                         ;
1248                 /* go past curr now */
1249                 rit++;
1250
1251                 action_list_t::reverse_iterator ritcopy = rit;
1252                 //See if we have enough reads from the same value
1253                 int count = 0;
1254                 for (; count < params.maxreads; rit++,count++) {
1255                         if (rit==list->rend())
1256                                 return;
1257                         ModelAction *act = *rit;
1258                         if (!act->is_read())
1259                                 return;
1260
1261                         if (act->get_reads_from() != rf)
1262                                 return;
1263                         if (act->get_node()->get_read_from_size() <= 1)
1264                                 return;
1265                 }
1266                 for (int i = 0; i<curr->get_node()->get_read_from_size(); i++) {
1267                         //Get write
1268                         const ModelAction * write = curr->get_node()->get_read_from_at(i);
1269
1270                         //Need a different write
1271                         if (write==rf)
1272                                 continue;
1273
1274                         /* Test to see whether this is a feasible write to read from*/
1275                         mo_graph->startChanges();
1276                         r_modification_order(curr, write);
1277                         bool feasiblereadfrom = isfeasible();
1278                         mo_graph->rollbackChanges();
1279
1280                         if (!feasiblereadfrom)
1281                                 continue;
1282                         rit = ritcopy;
1283
1284                         bool feasiblewrite = true;
1285                         //new we need to see if this write works for everyone
1286
1287                         for (int loop = count; loop>0; loop--,rit++) {
1288                                 ModelAction *act=*rit;
1289                                 bool foundvalue = false;
1290                                 for (int j = 0; j<act->get_node()->get_read_from_size(); j++) {
1291                                         if (act->get_node()->get_read_from_at(j)==write) {
1292                                                 foundvalue = true;
1293                                                 break;
1294                                         }
1295                                 }
1296                                 if (!foundvalue) {
1297                                         feasiblewrite = false;
1298                                         break;
1299                                 }
1300                         }
1301                         if (feasiblewrite) {
1302                                 too_many_reads = true;
1303                                 return;
1304                         }
1305                 }
1306         }
1307 }
1308
1309 /**
1310  * Updates the mo_graph with the constraints imposed from the current
1311  * read.
1312  *
1313  * Basic idea is the following: Go through each other thread and find
1314  * the lastest action that happened before our read.  Two cases:
1315  *
1316  * (1) The action is a write => that write must either occur before
1317  * the write we read from or be the write we read from.
1318  *
1319  * (2) The action is a read => the write that that action read from
1320  * must occur before the write we read from or be the same write.
1321  *
1322  * @param curr The current action. Must be a read.
1323  * @param rf The action that curr reads from. Must be a write.
1324  * @return True if modification order edges were added; false otherwise
1325  */
1326 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
1327 {
1328         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1329         unsigned int i;
1330         bool added = false;
1331         ASSERT(curr->is_read());
1332
1333         /* Iterate over all threads */
1334         for (i = 0; i < thrd_lists->size(); i++) {
1335                 /* Iterate over actions in thread, starting from most recent */
1336                 action_list_t *list = &(*thrd_lists)[i];
1337                 action_list_t::reverse_iterator rit;
1338                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1339                         ModelAction *act = *rit;
1340
1341                         /*
1342                          * Include at most one act per-thread that "happens
1343                          * before" curr. Don't consider reflexively.
1344                          */
1345                         if (act->happens_before(curr) && act != curr) {
1346                                 if (act->is_write()) {
1347                                         if (rf != act) {
1348                                                 mo_graph->addEdge(act, rf);
1349                                                 added = true;
1350                                         }
1351                                 } else {
1352                                         const ModelAction *prevreadfrom = act->get_reads_from();
1353                                         //if the previous read is unresolved, keep going...
1354                                         if (prevreadfrom == NULL)
1355                                                 continue;
1356
1357                                         if (rf != prevreadfrom) {
1358                                                 mo_graph->addEdge(prevreadfrom, rf);
1359                                                 added = true;
1360                                         }
1361                                 }
1362                                 break;
1363                         }
1364                 }
1365         }
1366
1367         return added;
1368 }
1369
1370 /** This method fixes up the modification order when we resolve a
1371  *  promises.  The basic problem is that actions that occur after the
1372  *  read curr could not property add items to the modification order
1373  *  for our read.
1374  *
1375  *  So for each thread, we find the earliest item that happens after
1376  *  the read curr.  This is the item we have to fix up with additional
1377  *  constraints.  If that action is write, we add a MO edge between
1378  *  the Action rf and that action.  If the action is a read, we add a
1379  *  MO edge between the Action rf, and whatever the read accessed.
1380  *
1381  * @param curr is the read ModelAction that we are fixing up MO edges for.
1382  * @param rf is the write ModelAction that curr reads from.
1383  *
1384  */
1385 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
1386 {
1387         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1388         unsigned int i;
1389         ASSERT(curr->is_read());
1390
1391         /* Iterate over all threads */
1392         for (i = 0; i < thrd_lists->size(); i++) {
1393                 /* Iterate over actions in thread, starting from most recent */
1394                 action_list_t *list = &(*thrd_lists)[i];
1395                 action_list_t::reverse_iterator rit;
1396                 ModelAction *lastact = NULL;
1397
1398                 /* Find last action that happens after curr that is either not curr or a rmw */
1399                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1400                         ModelAction *act = *rit;
1401                         if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
1402                                 lastact = act;
1403                         } else
1404                                 break;
1405                 }
1406
1407                         /* Include at most one act per-thread that "happens before" curr */
1408                 if (lastact != NULL) {
1409                         if (lastact==curr) {
1410                                 //Case 1: The resolved read is a RMW, and we need to make sure
1411                                 //that the write portion of the RMW mod order after rf
1412
1413                                 mo_graph->addEdge(rf, lastact);
1414                         } else if (lastact->is_read()) {
1415                                 //Case 2: The resolved read is a normal read and the next
1416                                 //operation is a read, and we need to make sure the value read
1417                                 //is mod ordered after rf
1418
1419                                 const ModelAction *postreadfrom = lastact->get_reads_from();
1420                                 if (postreadfrom != NULL&&rf != postreadfrom)
1421                                         mo_graph->addEdge(rf, postreadfrom);
1422                         } else {
1423                                 //Case 3: The resolved read is a normal read and the next
1424                                 //operation is a write, and we need to make sure that the
1425                                 //write is mod ordered after rf
1426                                 if (lastact!=rf)
1427                                         mo_graph->addEdge(rf, lastact);
1428                         }
1429                         break;
1430                 }
1431         }
1432 }
1433
1434 /**
1435  * Updates the mo_graph with the constraints imposed from the current write.
1436  *
1437  * Basic idea is the following: Go through each other thread and find
1438  * the lastest action that happened before our write.  Two cases:
1439  *
1440  * (1) The action is a write => that write must occur before
1441  * the current write
1442  *
1443  * (2) The action is a read => the write that that action read from
1444  * must occur before the current write.
1445  *
1446  * This method also handles two other issues:
1447  *
1448  * (I) Sequential Consistency: Making sure that if the current write is
1449  * seq_cst, that it occurs after the previous seq_cst write.
1450  *
1451  * (II) Sending the write back to non-synchronizing reads.
1452  *
1453  * @param curr The current action. Must be a write.
1454  * @return True if modification order edges were added; false otherwise
1455  */
1456 bool ModelChecker::w_modification_order(ModelAction *curr)
1457 {
1458         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
1459         unsigned int i;
1460         bool added = false;
1461         ASSERT(curr->is_write());
1462
1463         if (curr->is_seqcst()) {
1464                 /* We have to at least see the last sequentially consistent write,
1465                          so we are initialized. */
1466                 ModelAction *last_seq_cst = get_last_seq_cst(curr);
1467                 if (last_seq_cst != NULL) {
1468                         mo_graph->addEdge(last_seq_cst, curr);
1469                         added = true;
1470                 }
1471         }
1472
1473         /* Iterate over all threads */
1474         for (i = 0; i < thrd_lists->size(); i++) {
1475                 /* Iterate over actions in thread, starting from most recent */
1476                 action_list_t *list = &(*thrd_lists)[i];
1477                 action_list_t::reverse_iterator rit;
1478                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1479                         ModelAction *act = *rit;
1480                         if (act == curr) {
1481                                 /*
1482                                  * 1) If RMW and it actually read from something, then we
1483                                  * already have all relevant edges, so just skip to next
1484                                  * thread.
1485                                  *
1486                                  * 2) If RMW and it didn't read from anything, we should
1487                                  * whatever edge we can get to speed up convergence.
1488                                  *
1489                                  * 3) If normal write, we need to look at earlier actions, so
1490                                  * continue processing list.
1491                                  */
1492                                 if (curr->is_rmw()) {
1493                                         if (curr->get_reads_from()!=NULL)
1494                                                 break;
1495                                         else
1496                                                 continue;
1497                                 } else
1498                                         continue;
1499                         }
1500
1501                         /*
1502                          * Include at most one act per-thread that "happens
1503                          * before" curr
1504                          */
1505                         if (act->happens_before(curr)) {
1506                                 /*
1507                                  * Note: if act is RMW, just add edge:
1508                                  *   act --mo--> curr
1509                                  * The following edge should be handled elsewhere:
1510                                  *   readfrom(act) --mo--> act
1511                                  */
1512                                 if (act->is_write())
1513                                         mo_graph->addEdge(act, curr);
1514                                 else if (act->is_read()) {
1515                                         //if previous read accessed a null, just keep going
1516                                         if (act->get_reads_from() == NULL)
1517                                                 continue;
1518                                         mo_graph->addEdge(act->get_reads_from(), curr);
1519                                 }
1520                                 added = true;
1521                                 break;
1522                         } else if (act->is_read() && !act->could_synchronize_with(curr) &&
1523                                                      !act->same_thread(curr)) {
1524                                 /* We have an action that:
1525                                    (1) did not happen before us
1526                                    (2) is a read and we are a write
1527                                    (3) cannot synchronize with us
1528                                    (4) is in a different thread
1529                                    =>
1530                                    that read could potentially read from our write.  Note that
1531                                    these checks are overly conservative at this point, we'll
1532                                    do more checks before actually removing the
1533                                    pendingfuturevalue.
1534
1535                                  */
1536                                 if (thin_air_constraint_may_allow(curr, act)) {
1537                                         if (isfeasible() ||
1538                                                         (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && isfeasibleotherthanRMW())) {
1539                                                 struct PendingFutureValue pfv = {curr,act};
1540                                                 futurevalues->push_back(pfv);
1541                                         }
1542                                 }
1543                         }
1544                 }
1545         }
1546
1547         return added;
1548 }
1549
1550 /** Arbitrary reads from the future are not allowed.  Section 29.3
1551  * part 9 places some constraints.  This method checks one result of constraint
1552  * constraint.  Others require compiler support. */
1553 bool ModelChecker::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
1554         if (!writer->is_rmw())
1555                 return true;
1556
1557         if (!reader->is_rmw())
1558                 return true;
1559
1560         for (const ModelAction *search = writer->get_reads_from(); search != NULL; search = search->get_reads_from()) {
1561                 if (search == reader)
1562                         return false;
1563                 if (search->get_tid() == reader->get_tid() &&
1564                                 search->happens_before(reader))
1565                         break;
1566         }
1567
1568         return true;
1569 }
1570
1571 /**
1572  * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
1573  * some constraints. This method checks one the following constraint (others
1574  * require compiler support):
1575  *
1576  *   If X --hb-> Y --mo-> Z, then X should not read from Z.
1577  */
1578 bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
1579 {
1580         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, reader->get_location());
1581         unsigned int i;
1582         /* Iterate over all threads */
1583         for (i = 0; i < thrd_lists->size(); i++) {
1584                 const ModelAction *write_after_read = NULL;
1585
1586                 /* Iterate over actions in thread, starting from most recent */
1587                 action_list_t *list = &(*thrd_lists)[i];
1588                 action_list_t::reverse_iterator rit;
1589                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1590                         ModelAction *act = *rit;
1591
1592                         if (!reader->happens_before(act))
1593                                 break;
1594                         else if (act->is_write())
1595                                 write_after_read = act;
1596                         else if (act->is_read() && act->get_reads_from() != NULL && act != reader) {
1597                                 write_after_read = act->get_reads_from();
1598                         }
1599                 }
1600
1601                 if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
1602                         return false;
1603         }
1604         return true;
1605 }
1606
1607 /**
1608  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
1609  * The ModelAction under consideration is expected to be taking part in
1610  * release/acquire synchronization as an object of the "reads from" relation.
1611  * Note that this can only provide release sequence support for RMW chains
1612  * which do not read from the future, as those actions cannot be traced until
1613  * their "promise" is fulfilled. Similarly, we may not even establish the
1614  * presence of a release sequence with certainty, as some modification order
1615  * constraints may be decided further in the future. Thus, this function
1616  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
1617  * and a boolean representing certainty.
1618  *
1619  * @param rf The action that might be part of a release sequence. Must be a
1620  * write.
1621  * @param release_heads A pass-by-reference style return parameter. After
1622  * execution of this function, release_heads will contain the heads of all the
1623  * relevant release sequences, if any exists with certainty
1624  * @param pending A pass-by-reference style return parameter which is only used
1625  * when returning false (i.e., uncertain). Returns most information regarding
1626  * an uncertain release sequence, including any write operations that might
1627  * break the sequence.
1628  * @return true, if the ModelChecker is certain that release_heads is complete;
1629  * false otherwise
1630  */
1631 bool ModelChecker::release_seq_heads(const ModelAction *rf,
1632                 rel_heads_list_t *release_heads,
1633                 struct release_seq *pending) const
1634 {
1635         /* Only check for release sequences if there are no cycles */
1636         if (mo_graph->checkForCycles())
1637                 return false;
1638
1639         while (rf) {
1640                 ASSERT(rf->is_write());
1641
1642                 if (rf->is_release())
1643                         release_heads->push_back(rf);
1644                 if (!rf->is_rmw())
1645                         break; /* End of RMW chain */
1646
1647                 /** @todo Need to be smarter here...  In the linux lock
1648                  * example, this will run to the beginning of the program for
1649                  * every acquire. */
1650                 /** @todo The way to be smarter here is to keep going until 1
1651                  * thread has a release preceded by an acquire and you've seen
1652                  *       both. */
1653
1654                 /* acq_rel RMW is a sufficient stopping condition */
1655                 if (rf->is_acquire() && rf->is_release())
1656                         return true; /* complete */
1657
1658                 rf = rf->get_reads_from();
1659         };
1660         if (!rf) {
1661                 /* read from future: need to settle this later */
1662                 pending->rf = NULL;
1663                 return false; /* incomplete */
1664         }
1665
1666         if (rf->is_release())
1667                 return true; /* complete */
1668
1669         /* else relaxed write; check modification order for contiguous subsequence
1670          * -> rf must be same thread as release */
1671         int tid = id_to_int(rf->get_tid());
1672         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, rf->get_location());
1673         action_list_t *list = &(*thrd_lists)[tid];
1674         action_list_t::const_reverse_iterator rit;
1675
1676         /* Find rf in the thread list */
1677         rit = std::find(list->rbegin(), list->rend(), rf);
1678         ASSERT(rit != list->rend());
1679
1680         /* Find the last write/release */
1681         for (; rit != list->rend(); rit++)
1682                 if ((*rit)->is_release())
1683                         break;
1684         if (rit == list->rend()) {
1685                 /* No write-release in this thread */
1686                 return true; /* complete */
1687         }
1688         ModelAction *release = *rit;
1689
1690         ASSERT(rf->same_thread(release));
1691
1692         pending->writes.clear();
1693
1694         bool certain = true;
1695         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
1696                 if (id_to_int(rf->get_tid()) == (int)i)
1697                         continue;
1698                 list = &(*thrd_lists)[i];
1699
1700                 /* Can we ensure no future writes from this thread may break
1701                  * the release seq? */
1702                 bool future_ordered = false;
1703
1704                 ModelAction *last = get_last_action(int_to_id(i));
1705                 Thread *th = get_thread(int_to_id(i));
1706                 if ((last && rf->happens_before(last)) ||
1707                                 !is_enabled(th) ||
1708                                 th->is_complete())
1709                         future_ordered = true;
1710
1711                 ASSERT(!th->is_model_thread() || future_ordered);
1712
1713                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
1714                         const ModelAction *act = *rit;
1715                         /* Reach synchronization -> this thread is complete */
1716                         if (act->happens_before(release))
1717                                 break;
1718                         if (rf->happens_before(act)) {
1719                                 future_ordered = true;
1720                                 continue;
1721                         }
1722
1723                         /* Only non-RMW writes can break release sequences */
1724                         if (!act->is_write() || act->is_rmw())
1725                                 continue;
1726
1727                         /* Check modification order */
1728                         if (mo_graph->checkReachable(rf, act)) {
1729                                 /* rf --mo--> act */
1730                                 future_ordered = true;
1731                                 continue;
1732                         }
1733                         if (mo_graph->checkReachable(act, release))
1734                                 /* act --mo--> release */
1735                                 break;
1736                         if (mo_graph->checkReachable(release, act) &&
1737                                       mo_graph->checkReachable(act, rf)) {
1738                                 /* release --mo-> act --mo--> rf */
1739                                 return true; /* complete */
1740                         }
1741                         /* act may break release sequence */
1742                         pending->writes.push_back(act);
1743                         certain = false;
1744                 }
1745                 if (!future_ordered)
1746                         certain = false; /* This thread is uncertain */
1747         }
1748
1749         if (certain) {
1750                 release_heads->push_back(release);
1751                 pending->writes.clear();
1752         } else {
1753                 pending->release = release;
1754                 pending->rf = rf;
1755         }
1756         return certain;
1757 }
1758
1759 /**
1760  * A public interface for getting the release sequence head(s) with which a
1761  * given ModelAction must synchronize. This function only returns a non-empty
1762  * result when it can locate a release sequence head with certainty. Otherwise,
1763  * it may mark the internal state of the ModelChecker so that it will handle
1764  * the release sequence at a later time, causing @a act to update its
1765  * synchronization at some later point in execution.
1766  * @param act The 'acquire' action that may read from a release sequence
1767  * @param release_heads A pass-by-reference return parameter. Will be filled
1768  * with the head(s) of the release sequence(s), if they exists with certainty.
1769  * @see ModelChecker::release_seq_heads
1770  */
1771 void ModelChecker::get_release_seq_heads(ModelAction *act, rel_heads_list_t *release_heads)
1772 {
1773         const ModelAction *rf = act->get_reads_from();
1774         struct release_seq *sequence = (struct release_seq *)snapshot_calloc(1, sizeof(struct release_seq));
1775         sequence->acquire = act;
1776
1777         if (!release_seq_heads(rf, release_heads, sequence)) {
1778                 /* add act to 'lazy checking' list */
1779                 pending_rel_seqs->push_back(sequence);
1780         } else {
1781                 snapshot_free(sequence);
1782         }
1783 }
1784
1785 /**
1786  * Attempt to resolve all stashed operations that might synchronize with a
1787  * release sequence for a given location. This implements the "lazy" portion of
1788  * determining whether or not a release sequence was contiguous, since not all
1789  * modification order information is present at the time an action occurs.
1790  *
1791  * @param location The location/object that should be checked for release
1792  * sequence resolutions. A NULL value means to check all locations.
1793  * @param work_queue The work queue to which to add work items as they are
1794  * generated
1795  * @return True if any updates occurred (new synchronization, new mo_graph
1796  * edges)
1797  */
1798 bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_queue)
1799 {
1800         bool updated = false;
1801         std::vector< struct release_seq *, SnapshotAlloc<struct release_seq *> >::iterator it = pending_rel_seqs->begin();
1802         while (it != pending_rel_seqs->end()) {
1803                 struct release_seq *pending = *it;
1804                 ModelAction *act = pending->acquire;
1805
1806                 /* Only resolve sequences on the given location, if provided */
1807                 if (location && act->get_location() != location) {
1808                         it++;
1809                         continue;
1810                 }
1811
1812                 const ModelAction *rf = act->get_reads_from();
1813                 rel_heads_list_t release_heads;
1814                 bool complete;
1815                 complete = release_seq_heads(rf, &release_heads, pending);
1816                 for (unsigned int i = 0; i < release_heads.size(); i++) {
1817                         if (!act->has_synchronized_with(release_heads[i])) {
1818                                 if (act->synchronize_with(release_heads[i]))
1819                                         updated = true;
1820                                 else
1821                                         set_bad_synchronization();
1822                         }
1823                 }
1824
1825                 if (updated) {
1826                         /* Re-check all pending release sequences */
1827                         work_queue->push_back(CheckRelSeqWorkEntry(NULL));
1828                         /* Re-check act for mo_graph edges */
1829                         work_queue->push_back(MOEdgeWorkEntry(act));
1830
1831                         /* propagate synchronization to later actions */
1832                         action_list_t::reverse_iterator rit = action_trace->rbegin();
1833                         for (; (*rit) != act; rit++) {
1834                                 ModelAction *propagate = *rit;
1835                                 if (act->happens_before(propagate)) {
1836                                         propagate->synchronize_with(act);
1837                                         /* Re-check 'propagate' for mo_graph edges */
1838                                         work_queue->push_back(MOEdgeWorkEntry(propagate));
1839                                 }
1840                         }
1841                 }
1842                 if (complete) {
1843                         it = pending_rel_seqs->erase(it);
1844                         snapshot_free(pending);
1845                 } else {
1846                         it++;
1847                 }
1848         }
1849
1850         // If we resolved promises or data races, see if we have realized a data race.
1851         checkDataRaces();
1852
1853         return updated;
1854 }
1855
1856 /**
1857  * Performs various bookkeeping operations for the current ModelAction. For
1858  * instance, adds action to the per-object, per-thread action vector and to the
1859  * action trace list of all thread actions.
1860  *
1861  * @param act is the ModelAction to add.
1862  */
1863 void ModelChecker::add_action_to_lists(ModelAction *act)
1864 {
1865         int tid = id_to_int(act->get_tid());
1866         action_trace->push_back(act);
1867
1868         get_safe_ptr_action(obj_map, act->get_location())->push_back(act);
1869
1870         std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, act->get_location());
1871         if (tid >= (int)vec->size())
1872                 vec->resize(priv->next_thread_id);
1873         (*vec)[tid].push_back(act);
1874
1875         if ((int)thrd_last_action->size() <= tid)
1876                 thrd_last_action->resize(get_num_threads());
1877         (*thrd_last_action)[tid] = act;
1878
1879         if (act->is_wait()) {
1880                 void *mutex_loc=(void *) act->get_value();
1881                 get_safe_ptr_action(obj_map, mutex_loc)->push_back(act);
1882
1883                 std::vector<action_list_t> *vec = get_safe_ptr_vect_action(obj_thrd_map, mutex_loc);
1884                 if (tid >= (int)vec->size())
1885                         vec->resize(priv->next_thread_id);
1886                 (*vec)[tid].push_back(act);
1887
1888                 if ((int)thrd_last_action->size() <= tid)
1889                         thrd_last_action->resize(get_num_threads());
1890                 (*thrd_last_action)[tid] = act;
1891         }
1892 }
1893
1894 /**
1895  * @brief Get the last action performed by a particular Thread
1896  * @param tid The thread ID of the Thread in question
1897  * @return The last action in the thread
1898  */
1899 ModelAction * ModelChecker::get_last_action(thread_id_t tid) const
1900 {
1901         int threadid = id_to_int(tid);
1902         if (threadid < (int)thrd_last_action->size())
1903                 return (*thrd_last_action)[id_to_int(tid)];
1904         else
1905                 return NULL;
1906 }
1907
1908 /**
1909  * Gets the last memory_order_seq_cst write (in the total global sequence)
1910  * performed on a particular object (i.e., memory location), not including the
1911  * current action.
1912  * @param curr The current ModelAction; also denotes the object location to
1913  * check
1914  * @return The last seq_cst write
1915  */
1916 ModelAction * ModelChecker::get_last_seq_cst(ModelAction *curr) const
1917 {
1918         void *location = curr->get_location();
1919         action_list_t *list = get_safe_ptr_action(obj_map, location);
1920         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
1921         action_list_t::reverse_iterator rit;
1922         for (rit = list->rbegin(); rit != list->rend(); rit++)
1923                 if ((*rit)->is_write() && (*rit)->is_seqcst() && (*rit) != curr)
1924                         return *rit;
1925         return NULL;
1926 }
1927
1928 /**
1929  * Gets the last unlock operation performed on a particular mutex (i.e., memory
1930  * location). This function identifies the mutex according to the current
1931  * action, which is presumed to perform on the same mutex.
1932  * @param curr The current ModelAction; also denotes the object location to
1933  * check
1934  * @return The last unlock operation
1935  */
1936 ModelAction * ModelChecker::get_last_unlock(ModelAction *curr) const
1937 {
1938         void *location = curr->get_location();
1939         action_list_t *list = get_safe_ptr_action(obj_map, location);
1940         /* Find: max({i in dom(S) | isUnlock(t_i) && samevar(t_i, t)}) */
1941         action_list_t::reverse_iterator rit;
1942         for (rit = list->rbegin(); rit != list->rend(); rit++)
1943                 if ((*rit)->is_unlock() || (*rit)->is_wait())
1944                         return *rit;
1945         return NULL;
1946 }
1947
1948 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
1949 {
1950         ModelAction *parent = get_last_action(tid);
1951         if (!parent)
1952                 parent = get_thread(tid)->get_creation();
1953         return parent;
1954 }
1955
1956 /**
1957  * Returns the clock vector for a given thread.
1958  * @param tid The thread whose clock vector we want
1959  * @return Desired clock vector
1960  */
1961 ClockVector * ModelChecker::get_cv(thread_id_t tid)
1962 {
1963         return get_parent_action(tid)->get_cv();
1964 }
1965
1966 /**
1967  * Resolve a set of Promises with a current write. The set is provided in the
1968  * Node corresponding to @a write.
1969  * @param write The ModelAction that is fulfilling Promises
1970  * @return True if promises were resolved; false otherwise
1971  */
1972 bool ModelChecker::resolve_promises(ModelAction *write)
1973 {
1974         bool resolved = false;
1975         std::vector< thread_id_t, ModelAlloc<thread_id_t> > threads_to_check;
1976
1977         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
1978                 Promise *promise = (*promises)[promise_index];
1979                 if (write->get_node()->get_promise(i)) {
1980                         ModelAction *read = promise->get_action();
1981                         if (read->is_rmw()) {
1982                                 mo_graph->addRMWEdge(write, read);
1983                         }
1984                         read->read_from(write);
1985                         //First fix up the modification order for actions that happened
1986                         //before the read
1987                         r_modification_order(read, write);
1988                         //Next fix up the modification order for actions that happened
1989                         //after the read.
1990                         post_r_modification_order(read, write);
1991                         //Make sure the promise's value matches the write's value
1992                         ASSERT(promise->get_value() == write->get_value());
1993                         delete(promise);
1994
1995                         promises->erase(promises->begin() + promise_index);
1996                         threads_to_check.push_back(read->get_tid());
1997
1998                         resolved = true;
1999                 } else
2000                         promise_index++;
2001         }
2002
2003         //Check whether reading these writes has made threads unable to
2004         //resolve promises
2005
2006         for(unsigned int i=0;i<threads_to_check.size();i++)
2007                 mo_check_promises(threads_to_check[i], write);
2008
2009         return resolved;
2010 }
2011
2012 /**
2013  * Compute the set of promises that could potentially be satisfied by this
2014  * action. Note that the set computation actually appears in the Node, not in
2015  * ModelChecker.
2016  * @param curr The ModelAction that may satisfy promises
2017  */
2018 void ModelChecker::compute_promises(ModelAction *curr)
2019 {
2020         for (unsigned int i = 0; i < promises->size(); i++) {
2021                 Promise *promise = (*promises)[i];
2022                 const ModelAction *act = promise->get_action();
2023                 if (!act->happens_before(curr) &&
2024                                 act->is_read() &&
2025                                 !act->could_synchronize_with(curr) &&
2026                                 !act->same_thread(curr) &&
2027                                 act->get_location() == curr->get_location() &&
2028                                 promise->get_value() == curr->get_value()) {
2029                         curr->get_node()->set_promise(i, act->is_rmw());
2030                 }
2031         }
2032 }
2033
2034 /** Checks promises in response to change in ClockVector Threads. */
2035 void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVector *merge_cv)
2036 {
2037         for (unsigned int i = 0; i < promises->size(); i++) {
2038                 Promise *promise = (*promises)[i];
2039                 const ModelAction *act = promise->get_action();
2040                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
2041                                 merge_cv->synchronized_since(act)) {
2042                         if (promise->increment_threads(tid)) {
2043                                 //Promise has failed
2044                                 failed_promise = true;
2045                                 return;
2046                         }
2047                 }
2048         }
2049 }
2050
2051 void ModelChecker::check_promises_thread_disabled() {
2052         for (unsigned int i = 0; i < promises->size(); i++) {
2053                 Promise *promise = (*promises)[i];
2054                 if (promise->check_promise()) {
2055                         failed_promise = true;
2056                         return;
2057                 }
2058         }
2059 }
2060
2061 /** Checks promises in response to addition to modification order for threads.
2062  * Definitions:
2063  * pthread is the thread that performed the read that created the promise
2064  *
2065  * pread is the read that created the promise
2066  *
2067  * pwrite is either the first write to same location as pread by
2068  * pthread that is sequenced after pread or the value read by the
2069  * first read to the same lcoation as pread by pthread that is
2070  * sequenced after pread..
2071  *
2072  *      1. If tid=pthread, then we check what other threads are reachable
2073  * through the mode order starting with pwrite.  Those threads cannot
2074  * perform a write that will resolve the promise due to modification
2075  * order constraints.
2076  *
2077  * 2. If the tid is not pthread, we check whether pwrite can reach the
2078  * action write through the modification order.  If so, that thread
2079  * cannot perform a future write that will resolve the promise due to
2080  * modificatin order constraints.
2081  *
2082  *      @parem tid The thread that either read from the model action
2083  *      write, or actually did the model action write.
2084  *
2085  *      @parem write The ModelAction representing the relevant write.
2086  */
2087
2088 void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write) {
2089         void * location = write->get_location();
2090         for (unsigned int i = 0; i < promises->size(); i++) {
2091                 Promise *promise = (*promises)[i];
2092                 const ModelAction *act = promise->get_action();
2093
2094                 //Is this promise on the same location?
2095                 if ( act->get_location() != location )
2096                         continue;
2097
2098                 //same thread as the promise
2099                 if ( act->get_tid()==tid ) {
2100
2101                         //do we have a pwrite for the promise, if not, set it
2102                         if (promise->get_write() == NULL ) {
2103                                 promise->set_write(write);
2104                                 //The pwrite cannot happen before the promise
2105                                 if (write->happens_before(act) && (write != act)) {
2106                                         failed_promise = true;
2107                                         return;
2108                                 }
2109                         }
2110                         if (mo_graph->checkPromise(write, promise)) {
2111                                 failed_promise = true;
2112                                 return;
2113                         }
2114                 }
2115
2116                 //Don't do any lookups twice for the same thread
2117                 if (promise->has_sync_thread(tid))
2118                         continue;
2119
2120                 if (promise->get_write()&&mo_graph->checkReachable(promise->get_write(), write)) {
2121                         if (promise->increment_threads(tid)) {
2122                                 failed_promise = true;
2123                                 return;
2124                         }
2125                 }
2126         }
2127 }
2128
2129 /**
2130  * Compute the set of writes that may break the current pending release
2131  * sequence. This information is extracted from previou release sequence
2132  * calculations.
2133  *
2134  * @param curr The current ModelAction. Must be a release sequence fixup
2135  * action.
2136  */
2137 void ModelChecker::compute_relseq_breakwrites(ModelAction *curr)
2138 {
2139         if (pending_rel_seqs->empty())
2140                 return;
2141
2142         struct release_seq *pending = pending_rel_seqs->back();
2143         for (unsigned int i = 0; i < pending->writes.size(); i++) {
2144                 const ModelAction *write = pending->writes[i];
2145                 curr->get_node()->add_relseq_break(write);
2146         }
2147
2148         /* NULL means don't break the sequence; just synchronize */
2149         curr->get_node()->add_relseq_break(NULL);
2150 }
2151
2152 /**
2153  * Build up an initial set of all past writes that this 'read' action may read
2154  * from. This set is determined by the clock vector's "happens before"
2155  * relationship.
2156  * @param curr is the current ModelAction that we are exploring; it must be a
2157  * 'read' operation.
2158  */
2159 void ModelChecker::build_reads_from_past(ModelAction *curr)
2160 {
2161         std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
2162         unsigned int i;
2163         ASSERT(curr->is_read());
2164
2165         ModelAction *last_seq_cst = NULL;
2166
2167         /* Track whether this object has been initialized */
2168         bool initialized = false;
2169
2170         if (curr->is_seqcst()) {
2171                 last_seq_cst = get_last_seq_cst(curr);
2172                 /* We have to at least see the last sequentially consistent write,
2173                          so we are initialized. */
2174                 if (last_seq_cst != NULL)
2175                         initialized = true;
2176         }
2177
2178         /* Iterate over all threads */
2179         for (i = 0; i < thrd_lists->size(); i++) {
2180                 /* Iterate over actions in thread, starting from most recent */
2181                 action_list_t *list = &(*thrd_lists)[i];
2182                 action_list_t::reverse_iterator rit;
2183                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
2184                         ModelAction *act = *rit;
2185
2186                         /* Only consider 'write' actions */
2187                         if (!act->is_write() || act == curr)
2188                                 continue;
2189
2190                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
2191                         if (!curr->is_seqcst() || (!act->is_seqcst() && (last_seq_cst == NULL || !act->happens_before(last_seq_cst))) || act == last_seq_cst) {
2192                                 if (!curr->get_sleep_flag() || curr->is_seqcst() || sleep_can_read_from(curr, act)) {
2193                                         DEBUG("Adding action to may_read_from:\n");
2194                                         if (DBG_ENABLED()) {
2195                                                 act->print();
2196                                                 curr->print();
2197                                         }
2198                                         curr->get_node()->add_read_from(act);
2199                                 }
2200                         }
2201
2202                         /* Include at most one act per-thread that "happens before" curr */
2203                         if (act->happens_before(curr)) {
2204                                 initialized = true;
2205                                 break;
2206                         }
2207                 }
2208         }
2209
2210         if (!initialized)
2211                 assert_bug("May read from uninitialized atomic");
2212
2213         if (DBG_ENABLED() || !initialized) {
2214                 printf("Reached read action:\n");
2215                 curr->print();
2216                 printf("Printing may_read_from\n");
2217                 curr->get_node()->print_may_read_from();
2218                 printf("End printing may_read_from\n");
2219         }
2220 }
2221
2222 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {
2223         while(true) {
2224                 Node *prevnode=write->get_node()->get_parent();
2225
2226                 bool thread_sleep=prevnode->enabled_status(curr->get_tid())==THREAD_SLEEP_SET;
2227                 if (write->is_release()&&thread_sleep)
2228                         return true;
2229                 if (!write->is_rmw()) {
2230                         return false;
2231                 }
2232                 if (write->get_reads_from()==NULL)
2233                         return true;
2234                 write=write->get_reads_from();
2235         }
2236 }
2237
2238 static void print_list(action_list_t *list)
2239 {
2240         action_list_t::iterator it;
2241
2242         printf("---------------------------------------------------------------------\n");
2243         printf("Trace:\n");
2244         unsigned int hash=0;
2245
2246         for (it = list->begin(); it != list->end(); it++) {
2247                 (*it)->print();
2248                 hash=hash^(hash<<3)^((*it)->hash());
2249         }
2250         printf("HASH %u\n", hash);
2251         printf("---------------------------------------------------------------------\n");
2252 }
2253
2254 #if SUPPORT_MOD_ORDER_DUMP
2255 void ModelChecker::dumpGraph(char *filename) {
2256         char buffer[200];
2257         sprintf(buffer, "%s.dot",filename);
2258         FILE *file=fopen(buffer, "w");
2259         fprintf(file, "digraph %s {\n",filename);
2260         mo_graph->dumpNodes(file);
2261         ModelAction ** thread_array=(ModelAction **)model_calloc(1, sizeof(ModelAction *)*get_num_threads());
2262
2263         for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
2264                 ModelAction *action=*it;
2265                 if (action->is_read()) {
2266                         fprintf(file, "N%u [label=\"%u, T%u\"];\n", action->get_seq_number(),action->get_seq_number(), action->get_tid());
2267                         if (action->get_reads_from()!=NULL)
2268                                 fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
2269                 }
2270                 if (thread_array[action->get_tid()] != NULL) {
2271                         fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
2272                 }
2273
2274                 thread_array[action->get_tid()]=action;
2275         }
2276         fprintf(file,"}\n");
2277         model_free(thread_array);
2278         fclose(file);
2279 }
2280 #endif
2281
2282 void ModelChecker::print_summary()
2283 {
2284 #if SUPPORT_MOD_ORDER_DUMP
2285         scheduler->print();
2286         char buffername[100];
2287         sprintf(buffername, "exec%04u", stats.num_total);
2288         mo_graph->dumpGraphToFile(buffername);
2289         sprintf(buffername, "graph%04u", stats.num_total);
2290         dumpGraph(buffername);
2291 #endif
2292
2293         if (!isfinalfeasible())
2294                 printf("INFEASIBLE EXECUTION!\n");
2295         print_list(action_trace);
2296         printf("\n");
2297 }
2298
2299 /**
2300  * Add a Thread to the system for the first time. Should only be called once
2301  * per thread.
2302  * @param t The Thread to add
2303  */
2304 void ModelChecker::add_thread(Thread *t)
2305 {
2306         thread_map->put(id_to_int(t->get_id()), t);
2307         scheduler->add_thread(t);
2308 }
2309
2310 /**
2311  * Removes a thread from the scheduler.
2312  * @param the thread to remove.
2313  */
2314 void ModelChecker::remove_thread(Thread *t)
2315 {
2316         scheduler->remove_thread(t);
2317 }
2318
2319 /**
2320  * @brief Get a Thread reference by its ID
2321  * @param tid The Thread's ID
2322  * @return A Thread reference
2323  */
2324 Thread * ModelChecker::get_thread(thread_id_t tid) const
2325 {
2326         return thread_map->get(id_to_int(tid));
2327 }
2328
2329 /**
2330  * @brief Get a reference to the Thread in which a ModelAction was executed
2331  * @param act The ModelAction
2332  * @return A Thread reference
2333  */
2334 Thread * ModelChecker::get_thread(ModelAction *act) const
2335 {
2336         return get_thread(act->get_tid());
2337 }
2338
2339 /**
2340  * @brief Check if a Thread is currently enabled
2341  * @param t The Thread to check
2342  * @return True if the Thread is currently enabled
2343  */
2344 bool ModelChecker::is_enabled(Thread *t) const
2345 {
2346         return scheduler->is_enabled(t);
2347 }
2348
2349 /**
2350  * @brief Check if a Thread is currently enabled
2351  * @param tid The ID of the Thread to check
2352  * @return True if the Thread is currently enabled
2353  */
2354 bool ModelChecker::is_enabled(thread_id_t tid) const
2355 {
2356         return scheduler->is_enabled(tid);
2357 }
2358
2359 /**
2360  * Switch from a user-context to the "master thread" context (a.k.a. system
2361  * context). This switch is made with the intention of exploring a particular
2362  * model-checking action (described by a ModelAction object). Must be called
2363  * from a user-thread context.
2364  *
2365  * @param act The current action that will be explored. May be NULL only if
2366  * trace is exiting via an assertion (see ModelChecker::set_assert and
2367  * ModelChecker::has_asserted).
2368  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
2369  */
2370 int ModelChecker::switch_to_master(ModelAction *act)
2371 {
2372         DBG();
2373         Thread *old = thread_current();
2374         set_current_action(act);
2375         old->set_state(THREAD_READY);
2376         return Thread::swap(old, &system_context);
2377 }
2378
2379 /**
2380  * Takes the next step in the execution, if possible.
2381  * @return Returns true (success) if a step was taken and false otherwise.
2382  */
2383 bool ModelChecker::take_step() {
2384         if (has_asserted())
2385                 return false;
2386
2387         Thread *curr = priv->current_action ? get_thread(priv->current_action) : NULL;
2388         if (curr) {
2389                 if (curr->get_state() == THREAD_READY) {
2390                         ASSERT(priv->current_action);
2391
2392                         priv->nextThread = check_current_action(priv->current_action);
2393                         priv->current_action = NULL;
2394
2395                         if (curr->is_blocked() || curr->is_complete())
2396                                 scheduler->remove_thread(curr);
2397                 } else {
2398                         ASSERT(false);
2399                 }
2400         }
2401         Thread *next = scheduler->next_thread(priv->nextThread);
2402
2403         /* Infeasible -> don't take any more steps */
2404         if (!isfeasible())
2405                 return false;
2406         else if (isfeasibleprefix() && have_bug_reports()) {
2407                 set_assert();
2408                 return false;
2409         }
2410
2411         if (params.bound != 0) {
2412                 if (priv->used_sequence_numbers > params.bound) {
2413                         return false;
2414                 }
2415         }
2416
2417         DEBUG("(%d, %d)\n", curr ? id_to_int(curr->get_id()) : -1,
2418                         next ? id_to_int(next->get_id()) : -1);
2419
2420         /*
2421          * Launch end-of-execution release sequence fixups only when there are:
2422          *
2423          * (1) no more user threads to run (or when execution replay chooses
2424          *     the 'model_thread')
2425          * (2) pending release sequences
2426          * (3) pending assertions (i.e., data races)
2427          * (4) no pending promises
2428          */
2429         if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
2430                         isfinalfeasible() && !unrealizedraces.empty()) {
2431                 printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
2432                                 pending_rel_seqs->size());
2433                 ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
2434                                 std::memory_order_seq_cst, NULL, VALUE_NONE,
2435                                 model_thread);
2436                 set_current_action(fixup);
2437                 return true;
2438         }
2439
2440         /* next == NULL -> don't take any more steps */
2441         if (!next)
2442                 return false;
2443
2444         next->set_state(THREAD_RUNNING);
2445
2446         if (next->get_pending() != NULL) {
2447                 /* restart a pending action */
2448                 set_current_action(next->get_pending());
2449                 next->set_pending(NULL);
2450                 next->set_state(THREAD_READY);
2451                 return true;
2452         }
2453
2454         /* Return false only if swap fails with an error */
2455         return (Thread::swap(&system_context, next) == 0);
2456 }
2457
2458 /** Runs the current execution until threre are no more steps to take. */
2459 void ModelChecker::finish_execution() {
2460         DBG();
2461
2462         while (take_step());
2463 }