model.cc

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