model.cc

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