model.cc

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