model.cc

   1 #include <stdio.h>
   2 #include <algorithm>
   3
   4 #include "model.h"
   5 #include "action.h"
   6 #include "nodestack.h"
   7 #include "schedule.h"
   8 #include "snapshot-interface.h"
   9 #include "common.h"
  10 #include "clockvector.h"
  11 #include "cyclegraph.h"
  12 #include "promise.h"
  13 #include "datarace.h"
  14
  15 #define INITIAL_THREAD_ID       0
  16
  17 ModelChecker *model;
  18
  19 /** @brief Constructor */
  20 ModelChecker::ModelChecker(struct model_params params) :
  21         /* Initialize default scheduler */
  22         scheduler(new Scheduler()),
  23         num_executions(0),
  24         params(params),
  25         diverge(NULL),
  26         action_trace(new action_list_t()),
  27         thread_map(new HashTable<int, Thread *, int>()),
  28         obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
  29         obj_thrd_map(new HashTable<void *, std::vector<action_list_t>, uintptr_t, 4 >()),
  30         promises(new std::vector<Promise *>()),
  31         lazy_sync_with_release(new HashTable<void *, std::list<ModelAction *>, uintptr_t, 4>()),
  32         thrd_last_action(new std::vector<ModelAction *>(1)),
  33         node_stack(new NodeStack()),
  34         mo_graph(new CycleGraph()),
  35         failed_promise(false),
  36         asserted(false)
  37 {
  38         /* Allocate this "size" on the snapshotting heap */
  39         priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
  40         /* First thread created will have id INITIAL_THREAD_ID */
  41         priv->next_thread_id = INITIAL_THREAD_ID;
  42 }
  43
  44 /** @brief Destructor */
  45 ModelChecker::~ModelChecker()
  46 {
  47         for (int i = 0; i < get_num_threads(); i++)
  48                 delete thread_map->get(i);
  49         delete thread_map;
  50
  51         delete obj_thrd_map;
  52         delete obj_map;
  53         delete action_trace;
  54
  55         for (unsigned int i = 0; i < promises->size(); i++)
  56                 delete (*promises)[i];
  57         delete promises;
  58
  59         delete lazy_sync_with_release;
  60
  61         delete thrd_last_action;
  62         delete node_stack;
  63         delete scheduler;
  64         delete mo_graph;
  65 }
  66
  67 /**
  68  * Restores user program to initial state and resets all model-checker data
  69  * structures.
  70  */
  71 void ModelChecker::reset_to_initial_state()
  72 {
  73         DEBUG("+++ Resetting to initial state +++\n");
  74         node_stack->reset_execution();
  75         failed_promise = false;
  76         reset_asserted();
  77         snapshotObject->backTrackBeforeStep(0);
  78 }
  79
  80 /** @returns a thread ID for a new Thread */
  81 thread_id_t ModelChecker::get_next_id()
  82 {
  83         return priv->next_thread_id++;
  84 }
  85
  86 /** @returns the number of user threads created during this execution */
  87 int ModelChecker::get_num_threads()
  88 {
  89         return priv->next_thread_id;
  90 }
  91
  92 /** @returns a sequence number for a new ModelAction */
  93 modelclock_t ModelChecker::get_next_seq_num()
  94 {
  95         return ++priv->used_sequence_numbers;
  96 }
  97
  98 /**
  99  * Choose the next thread in the replay sequence.
 100  *
 101  * If the replay sequence has reached the 'diverge' point, returns a thread
 102  * from the backtracking set. Otherwise, simply returns the next thread in the
 103  * sequence that is being replayed.
 104  */
 105 Thread * ModelChecker::get_next_replay_thread()
 106 {
 107         thread_id_t tid;
 108
 109         /* Have we completed exploring the preselected path? */
 110         if (diverge == NULL)
 111                 return NULL;
 112
 113         /* Else, we are trying to replay an execution */
 114         ModelAction *next = node_stack->get_next()->get_action();
 115
 116         if (next == diverge) {
 117                 Node *nextnode = next->get_node();
 118                 /* Reached divergence point */
 119                 if (nextnode->increment_promise()) {
 120                         /* The next node will try to satisfy a different set of promises. */
 121                         tid = next->get_tid();
 122                         node_stack->pop_restofstack(2);
 123                 } else if (nextnode->increment_read_from()) {
 124                         /* The next node will read from a different value. */
 125                         tid = next->get_tid();
 126                         node_stack->pop_restofstack(2);
 127                 } else if (nextnode->increment_future_value()) {
 128                         /* The next node will try to read from a different future value. */
 129                         tid = next->get_tid();
 130                         node_stack->pop_restofstack(2);
 131                 } else {
 132                         /* Make a different thread execute for next step */
 133                         Node *node = nextnode->get_parent();
 134                         tid = node->get_next_backtrack();
 135                         node_stack->pop_restofstack(1);
 136                 }
 137                 DEBUG("*** Divergence point ***\n");
 138                 diverge = NULL;
 139         } else {
 140                 tid = next->get_tid();
 141         }
 142         DEBUG("*** ModelChecker chose next thread = %d ***\n", tid);
 143         ASSERT(tid != THREAD_ID_T_NONE);
 144         return thread_map->get(id_to_int(tid));
 145 }
 146
 147 /**
 148  * Queries the model-checker for more executions to explore and, if one
 149  * exists, resets the model-checker state to execute a new execution.
 150  *
 151  * @return If there are more executions to explore, return true. Otherwise,
 152  * return false.
 153  */
 154 bool ModelChecker::next_execution()
 155 {
 156         DBG();
 157
 158         num_executions++;
 159
 160         if (isfinalfeasible() || DBG_ENABLED())
 161                 print_summary();
 162
 163         if ((diverge = get_next_backtrack()) == NULL)
 164                 return false;
 165
 166         if (DBG_ENABLED()) {
 167                 printf("Next execution will diverge at:\n");
 168                 diverge->print();
 169         }
 170
 171         reset_to_initial_state();
 172         return true;
 173 }
 174
 175 ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
 176 {
 177         action_type type = act->get_type();
 178
 179         switch (type) {
 180                 case ATOMIC_READ:
 181                 case ATOMIC_WRITE:
 182                 case ATOMIC_RMW:
 183                         break;
 184                 default:
 185                         return NULL;
 186         }
 187         /* linear search: from most recent to oldest */
 188         action_list_t *list = obj_map->get_safe_ptr(act->get_location());
 189         action_list_t::reverse_iterator rit;
 190         for (rit = list->rbegin(); rit != list->rend(); rit++) {
 191                 ModelAction *prev = *rit;
 192                 if (act->is_synchronizing(prev))
 193                         return prev;
 194         }
 195         return NULL;
 196 }
 197
 198 void ModelChecker::set_backtracking(ModelAction *act)
 199 {
 200         ModelAction *prev;
 201         Node *node;
 202         Thread *t = get_thread(act->get_tid());
 203
 204         prev = get_last_conflict(act);
 205         if (prev == NULL)
 206                 return;
 207
 208         node = prev->get_node()->get_parent();
 209
 210         while (!node->is_enabled(t))
 211                 t = t->get_parent();
 212
 213         /* Check if this has been explored already */
 214         if (node->has_been_explored(t->get_id()))
 215                 return;
 216
 217         /* Cache the latest backtracking point */
 218         if (!priv->next_backtrack || *prev > *priv->next_backtrack)
 219                 priv->next_backtrack = prev;
 220
 221         /* If this is a new backtracking point, mark the tree */
 222         if (!node->set_backtrack(t->get_id()))
 223                 return;
 224         DEBUG("Setting backtrack: conflict = %d, instead tid = %d\n",
 225                         prev->get_tid(), t->get_id());
 226         if (DBG_ENABLED()) {
 227                 prev->print();
 228                 act->print();
 229         }
 230 }
 231
 232 /**
 233  * Returns last backtracking point. The model checker will explore a different
 234  * path for this point in the next execution.
 235  * @return The ModelAction at which the next execution should diverge.
 236  */
 237 ModelAction * ModelChecker::get_next_backtrack()
 238 {
 239         ModelAction *next = priv->next_backtrack;
 240         priv->next_backtrack = NULL;
 241         return next;
 242 }
 243
 244 /**
 245  * This is the heart of the model checker routine. It performs model-checking
 246  * actions corresponding to a given "current action." Among other processes, it
 247  * calculates reads-from relationships, updates synchronization clock vectors,
 248  * forms a memory_order constraints graph, and handles replay/backtrack
 249  * execution when running permutations of previously-observed executions.
 250  *
 251  * @param curr The current action to process
 252  * @return The next Thread that must be executed. May be NULL if ModelChecker
 253  * makes no choice (e.g., according to replay execution, combining RMW actions,
 254  * etc.)
 255  */
 256 Thread * ModelChecker::check_current_action(ModelAction *curr)
 257 {
 258         bool already_added = false;
 259
 260         ASSERT(curr);
 261
 262         if (curr->is_rmwc() || curr->is_rmw()) {
 263                 ModelAction *tmp = process_rmw(curr);
 264                 already_added = true;
 265                 delete curr;
 266                 curr = tmp;
 267         } else {
 268                 ModelAction *tmp = node_stack->explore_action(curr);
 269                 if (tmp) {
 270                         /* Discard duplicate ModelAction; use action from NodeStack */
 271                         /* First restore type and order in case of RMW operation */
 272                         if (curr->is_rmwr())
 273                                 tmp->copy_typeandorder(curr);
 274
 275                         /* If we have diverged, we need to reset the clock vector. */
 276                         if (diverge == NULL)
 277                                 tmp->create_cv(get_parent_action(tmp->get_tid()));
 278
 279                         delete curr;
 280                         curr = tmp;
 281                 } else {
 282                         /*
 283                          * Perform one-time actions when pushing new ModelAction onto
 284                          * NodeStack
 285                          */
 286                         curr->create_cv(get_parent_action(curr->get_tid()));
 287                         /* Build may_read_from set */
 288                         if (curr->is_read())
 289                                 build_reads_from_past(curr);
 290                         if (curr->is_write())
 291                                 compute_promises(curr);
 292                 }
 293         }
 294
 295         /* Assign 'creation' parent */
 296         if (curr->get_type() == THREAD_CREATE) {
 297                 Thread *th = (Thread *)curr->get_location();
 298                 th->set_creation(curr);
 299         } else if (curr->get_type() == THREAD_JOIN) {
 300                 Thread *wait, *join;
 301                 wait = get_thread(curr->get_tid());
 302                 join = (Thread *)curr->get_location();
 303                 if (!join->is_complete())
 304                         scheduler->wait(wait, join);
 305         } else if (curr->get_type() == THREAD_FINISH) {
 306                 Thread *th = get_thread(curr->get_tid());
 307                 while (!th->wait_list_empty()) {
 308                         Thread *wake = th->pop_wait_list();
 309                         scheduler->wake(wake);
 310                 }
 311                 th->complete();
 312         }
 313
 314         /* Deal with new thread */
 315         if (curr->get_type() == THREAD_START)
 316                 check_promises(NULL, curr->get_cv());
 317
 318         /* Assign reads_from values */
 319         Thread *th = get_thread(curr->get_tid());
 320         uint64_t value = VALUE_NONE;
 321         bool updated = false;
 322         if (curr->is_read()) {
 323                 const ModelAction *reads_from = curr->get_node()->get_read_from();
 324                 if (reads_from != NULL) {
 325                         value = reads_from->get_value();
 326                         /* Assign reads_from, perform release/acquire synchronization */
 327                         curr->read_from(reads_from);
 328                         if (r_modification_order(curr,reads_from))
 329                                 updated = true;
 330                 } else {
 331                         /* Read from future value */
 332                         value = curr->get_node()->get_future_value();
 333                         curr->read_from(NULL);
 334                         Promise *valuepromise = new Promise(curr, value);
 335                         promises->push_back(valuepromise);
 336                 }
 337         } else if (curr->is_write()) {
 338                 if (w_modification_order(curr))
 339                         updated = true;
 340                 if (resolve_promises(curr))
 341                         updated = true;
 342         }
 343
 344         if (updated)
 345                 resolve_release_sequences(curr->get_location());
 346
 347         th->set_return_value(value);
 348
 349         /* Add action to list.  */
 350         if (!already_added)
 351                 add_action_to_lists(curr);
 352
 353         Node *currnode = curr->get_node();
 354         Node *parnode = currnode->get_parent();
 355
 356         if (!parnode->backtrack_empty() || !currnode->read_from_empty() ||
 357                   !currnode->future_value_empty() || !currnode->promise_empty())
 358                 if (!priv->next_backtrack || *curr > *priv->next_backtrack)
 359                         priv->next_backtrack = curr;
 360
 361         set_backtracking(curr);
 362
 363         /* Do not split atomic actions. */
 364         if (curr->is_rmwr())
 365                 return thread_current();
 366         /* The THREAD_CREATE action points to the created Thread */
 367         else if (curr->get_type() == THREAD_CREATE)
 368                 return (Thread *)curr->get_location();
 369         else
 370                 return get_next_replay_thread();
 371 }
 372
 373 /** @returns whether the current partial trace must be a prefix of a
 374  * feasible trace. */
 375
 376 bool ModelChecker::isfeasibleprefix() {
 377         return promises->size()==0;
 378 }
 379
 380 /** @returns whether the current partial trace is feasible. */
 381 bool ModelChecker::isfeasible() {
 382         return !mo_graph->checkForCycles() && !failed_promise;
 383 }
 384
 385 /** Returns whether the current completed trace is feasible. */
 386 bool ModelChecker::isfinalfeasible() {
 387         return isfeasible() && promises->size() == 0;
 388 }
 389
 390 /** Close out a RMWR by converting previous RMWR into a RMW or READ. */
 391 ModelAction * ModelChecker::process_rmw(ModelAction *act) {
 392         int tid = id_to_int(act->get_tid());
 393         ModelAction *lastread = get_last_action(tid);
 394         lastread->process_rmw(act);
 395         if (act->is_rmw())
 396                 mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
 397         return lastread;
 398 }
 399
 400 /**
 401  * Updates the mo_graph with the constraints imposed from the current read.
 402  * @param curr The current action. Must be a read.
 403  * @param rf The action that curr reads from. Must be a write.
 404  * @return True if modification order edges were added; false otherwise
 405  */
 406 bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
 407 {
 408         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 409         unsigned int i;
 410         bool added = false;
 411         ASSERT(curr->is_read());
 412
 413         /* Iterate over all threads */
 414         for (i = 0; i < thrd_lists->size(); i++) {
 415                 /* Iterate over actions in thread, starting from most recent */
 416                 action_list_t *list = &(*thrd_lists)[i];
 417                 action_list_t::reverse_iterator rit;
 418                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 419                         ModelAction *act = *rit;
 420
 421                         /* Include at most one act per-thread that "happens before" curr */
 422                         if (act->happens_before(curr)) {
 423                                 if (act->is_read()) {
 424                                         const ModelAction *prevreadfrom = act->get_reads_from();
 425                                         if (prevreadfrom != NULL && rf != prevreadfrom) {
 426                                                 mo_graph->addEdge(prevreadfrom, rf);
 427                                                 added = true;
 428                                         }
 429                                 } else if (rf != act) {
 430                                         mo_graph->addEdge(act, rf);
 431                                         added = true;
 432                                 }
 433                                 break;
 434                         }
 435                 }
 436         }
 437
 438         return added;
 439 }
 440
 441 /** Updates the mo_graph with the constraints imposed from the current read. */
 442 void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
 443 {
 444         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 445         unsigned int i;
 446         ASSERT(curr->is_read());
 447
 448         /* Iterate over all threads */
 449         for (i = 0; i < thrd_lists->size(); i++) {
 450                 /* Iterate over actions in thread, starting from most recent */
 451                 action_list_t *list = &(*thrd_lists)[i];
 452                 action_list_t::reverse_iterator rit;
 453                 ModelAction *lastact = NULL;
 454
 455                 /* Find last action that happens after curr */
 456                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 457                         ModelAction *act = *rit;
 458                         if (curr->happens_before(act)) {
 459                                 lastact = act;
 460                         } else
 461                                 break;
 462                 }
 463
 464                         /* Include at most one act per-thread that "happens before" curr */
 465                 if (lastact != NULL) {
 466                         if (lastact->is_read()) {
 467                                 const ModelAction *postreadfrom = lastact->get_reads_from();
 468                                 if (postreadfrom != NULL&&rf != postreadfrom)
 469                                         mo_graph->addEdge(rf, postreadfrom);
 470                         } else if (rf != lastact) {
 471                                 mo_graph->addEdge(rf, lastact);
 472                         }
 473                         break;
 474                 }
 475         }
 476 }
 477
 478 /**
 479  * Updates the mo_graph with the constraints imposed from the current write.
 480  * @param curr The current action. Must be a write.
 481  * @return True if modification order edges were added; false otherwise
 482  */
 483 bool ModelChecker::w_modification_order(ModelAction *curr)
 484 {
 485         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 486         unsigned int i;
 487         bool added = false;
 488         ASSERT(curr->is_write());
 489
 490         if (curr->is_seqcst()) {
 491                 /* We have to at least see the last sequentially consistent write,
 492                          so we are initialized. */
 493                 ModelAction *last_seq_cst = get_last_seq_cst(curr->get_location());
 494                 if (last_seq_cst != NULL) {
 495                         mo_graph->addEdge(last_seq_cst, curr);
 496                         added = true;
 497                 }
 498         }
 499
 500         /* Iterate over all threads */
 501         for (i = 0; i < thrd_lists->size(); i++) {
 502                 /* Iterate over actions in thread, starting from most recent */
 503                 action_list_t *list = &(*thrd_lists)[i];
 504                 action_list_t::reverse_iterator rit;
 505                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 506                         ModelAction *act = *rit;
 507
 508                         /* Include at most one act per-thread that "happens before" curr */
 509                         if (act->happens_before(curr)) {
 510                                 if (act->is_read())
 511                                         mo_graph->addEdge(act->get_reads_from(), curr);
 512                                 else
 513                                         mo_graph->addEdge(act, curr);
 514                                 added = true;
 515                                 break;
 516                         } else if (act->is_read() && !act->is_synchronizing(curr) &&
 517                                                      !act->same_thread(curr)) {
 518                                 /* We have an action that:
 519                                    (1) did not happen before us
 520                                    (2) is a read and we are a write
 521                                    (3) cannot synchronize with us
 522                                    (4) is in a different thread
 523                                    =>
 524                                    that read could potentially read from our write.
 525                                  */
 526                                 if (act->get_node()->add_future_value(curr->get_value()) &&
 527                                                 (!priv->next_backtrack || *act > *priv->next_backtrack))
 528                                         priv->next_backtrack = act;
 529                         }
 530                 }
 531         }
 532
 533         return added;
 534 }
 535
 536 /**
 537  * Finds the head(s) of the release sequence(s) containing a given ModelAction.
 538  * The ModelAction under consideration is expected to be taking part in
 539  * release/acquire synchronization as an object of the "reads from" relation.
 540  * Note that this can only provide release sequence support for RMW chains
 541  * which do not read from the future, as those actions cannot be traced until
 542  * their "promise" is fulfilled. Similarly, we may not even establish the
 543  * presence of a release sequence with certainty, as some modification order
 544  * constraints may be decided further in the future. Thus, this function
 545  * "returns" two pieces of data: a pass-by-reference vector of @a release_heads
 546  * and a boolean representing certainty.
 547  *
 548  * @todo Finish lazy updating, when promises are fulfilled in the future
 549  * @param rf The action that might be part of a release sequence. Must be a
 550  * write.
 551  * @param release_heads A pass-by-reference style return parameter.  After
 552  * execution of this function, release_heads will contain the heads of all the
 553  * relevant release sequences, if any exists
 554  * @return true, if the ModelChecker is certain that release_heads is complete;
 555  * false otherwise
 556  */
 557 bool ModelChecker::release_seq_head(const ModelAction *rf,
 558                 std::vector<const ModelAction *> *release_heads) const
 559 {
 560         ASSERT(rf->is_write());
 561         if (!rf) {
 562                 /* read from future: need to settle this later */
 563                 return false; /* incomplete */
 564         }
 565         if (rf->is_release())
 566                 release_heads->push_back(rf);
 567         if (rf->is_rmw()) {
 568                 if (rf->is_acquire())
 569                         return true; /* complete */
 570                 return release_seq_head(rf->get_reads_from(), release_heads);
 571         }
 572         if (rf->is_release())
 573                 return true; /* complete */
 574
 575         /* else relaxed write; check modification order for contiguous subsequence
 576          * -> rf must be same thread as release */
 577         int tid = id_to_int(rf->get_tid());
 578         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(rf->get_location());
 579         action_list_t *list = &(*thrd_lists)[tid];
 580         action_list_t::const_reverse_iterator rit;
 581
 582         /* Find rf in the thread list */
 583         rit = std::find(list->rbegin(), list->rend(), rf);
 584         ASSERT(rit != list->rend());
 585
 586         /* Find the last write/release */
 587         for (; rit != list->rend(); rit++)
 588                 if ((*rit)->is_release())
 589                         break;
 590         if (rit == list->rend()) {
 591                 /* No write-release in this thread */
 592                 return true; /* complete */
 593         }
 594         ModelAction *release = *rit;
 595
 596         ASSERT(rf->same_thread(release));
 597
 598         bool certain = true;
 599         for (unsigned int i = 0; i < thrd_lists->size(); i++) {
 600                 if (id_to_int(rf->get_tid()) == (int)i)
 601                         continue;
 602                 list = &(*thrd_lists)[i];
 603
 604                 /* Can we ensure no future writes from this thread may break
 605                  * the release seq? */
 606                 bool future_ordered = false;
 607
 608                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 609                         const ModelAction *act = *rit;
 610                         if (!act->is_write())
 611                                 continue;
 612                         /* Reach synchronization -> this thread is complete */
 613                         if (act->happens_before(release))
 614                                 break;
 615                         if (rf->happens_before(act)) {
 616                                 future_ordered = true;
 617                                 continue;
 618                         }
 619
 620                         /* Check modification order */
 621                         if (mo_graph->checkReachable(rf, act)) {
 622                                 /* rf --mo--> act */
 623                                 future_ordered = true;
 624                                 continue;
 625                         }
 626                         if (mo_graph->checkReachable(act, release))
 627                                 /* act --mo--> release */
 628                                 break;
 629                         if (mo_graph->checkReachable(release, act) &&
 630                                       mo_graph->checkReachable(act, rf)) {
 631                                 /* release --mo-> act --mo--> rf */
 632                                 return true; /* complete */
 633                         }
 634                         certain = false;
 635                 }
 636                 if (!future_ordered)
 637                         return false; /* This thread is uncertain */
 638         }
 639
 640         if (certain)
 641                 release_heads->push_back(release);
 642         return certain;
 643 }
 644
 645 /**
 646  * A public interface for getting the release sequence head(s) with which a
 647  * given ModelAction must synchronize. This function only returns a non-empty
 648  * result when it can locate a release sequence head with certainty. Otherwise,
 649  * it may mark the internal state of the ModelChecker so that it will handle
 650  * the release sequence at a later time, causing @a act to update its
 651  * synchronization at some later point in execution.
 652  * @param act The 'acquire' action that may read from a release sequence
 653  * @param release_heads A pass-by-reference return parameter. Will be filled
 654  * with the head(s) of the release sequence(s), if they exists with certainty.
 655  * @see ModelChecker::release_seq_head
 656  */
 657 void ModelChecker::get_release_seq_heads(ModelAction *act,
 658                 std::vector<const ModelAction *> *release_heads)
 659 {
 660         const ModelAction *rf = act->get_reads_from();
 661         bool complete;
 662         complete = release_seq_head(rf, release_heads);
 663         if (!complete) {
 664                 /* add act to 'lazy checking' list */
 665                 std::list<ModelAction *> *list;
 666                 list = lazy_sync_with_release->get_safe_ptr(act->get_location());
 667                 list->push_back(act);
 668         }
 669 }
 670
 671 /**
 672  * Attempt to resolve all stashed operations that might synchronize with a
 673  * release sequence for a given location. This implements the "lazy" portion of
 674  * determining whether or not a release sequence was contiguous, since not all
 675  * modification order information is present at the time an action occurs.
 676  *
 677  * @param location The location/object that should be checked for release
 678  * sequence resolutions
 679  * @return True if any updates occurred (new synchronization, new mo_graph edges)
 680  */
 681 bool ModelChecker::resolve_release_sequences(void *location)
 682 {
 683         std::list<ModelAction *> *list;
 684         list = lazy_sync_with_release->getptr(location);
 685         if (!list)
 686                 return false;
 687
 688         bool updated = false;
 689         std::list<ModelAction *>::iterator it = list->begin();
 690         while (it != list->end()) {
 691                 ModelAction *act = *it;
 692                 const ModelAction *rf = act->get_reads_from();
 693                 std::vector<const ModelAction *> release_heads;
 694                 bool complete;
 695                 complete = release_seq_head(rf, &release_heads);
 696                 for (unsigned int i = 0; i < release_heads.size(); i++) {
 697                         if (!act->has_synchronized_with(release_heads[i])) {
 698                                 updated = true;
 699                                 act->synchronize_with(release_heads[i]);
 700                         }
 701                 }
 702
 703                 if (updated) {
 704                         /* propagate synchronization to later actions */
 705                         action_list_t::reverse_iterator it = action_trace->rbegin();
 706                         while ((*it) != act) {
 707                                 ModelAction *propagate = *it;
 708                                 if (act->happens_before(propagate))
 709                                         /** @todo new mo_graph edges along with
 710                                          * this synchronization? */
 711                                         propagate->synchronize_with(act);
 712                         }
 713                 }
 714                 if (complete)
 715                         it = list->erase(it);
 716                 else
 717                         it++;
 718         }
 719
 720         // If we resolved promises or data races, see if we have realized a data race.
 721         if (checkDataRaces()) {
 722                 set_assert();
 723         }
 724
 725         return updated;
 726 }
 727
 728 /**
 729  * Performs various bookkeeping operations for the current ModelAction. For
 730  * instance, adds action to the per-object, per-thread action vector and to the
 731  * action trace list of all thread actions.
 732  *
 733  * @param act is the ModelAction to add.
 734  */
 735 void ModelChecker::add_action_to_lists(ModelAction *act)
 736 {
 737         int tid = id_to_int(act->get_tid());
 738         action_trace->push_back(act);
 739
 740         obj_map->get_safe_ptr(act->get_location())->push_back(act);
 741
 742         std::vector<action_list_t> *vec = obj_thrd_map->get_safe_ptr(act->get_location());
 743         if (tid >= (int)vec->size())
 744                 vec->resize(priv->next_thread_id);
 745         (*vec)[tid].push_back(act);
 746
 747         if ((int)thrd_last_action->size() <= tid)
 748                 thrd_last_action->resize(get_num_threads());
 749         (*thrd_last_action)[tid] = act;
 750 }
 751
 752 ModelAction * ModelChecker::get_last_action(thread_id_t tid)
 753 {
 754         int nthreads = get_num_threads();
 755         if ((int)thrd_last_action->size() < nthreads)
 756                 thrd_last_action->resize(nthreads);
 757         return (*thrd_last_action)[id_to_int(tid)];
 758 }
 759
 760 /**
 761  * Gets the last memory_order_seq_cst action (in the total global sequence)
 762  * performed on a particular object (i.e., memory location).
 763  * @param location The object location to check
 764  * @return The last seq_cst action performed
 765  */
 766 ModelAction * ModelChecker::get_last_seq_cst(const void *location)
 767 {
 768         action_list_t *list = obj_map->get_safe_ptr(location);
 769         /* Find: max({i in dom(S) | seq_cst(t_i) && isWrite(t_i) && samevar(t_i, t)}) */
 770         action_list_t::reverse_iterator rit;
 771         for (rit = list->rbegin(); rit != list->rend(); rit++)
 772                 if ((*rit)->is_write() && (*rit)->is_seqcst())
 773                         return *rit;
 774         return NULL;
 775 }
 776
 777 ModelAction * ModelChecker::get_parent_action(thread_id_t tid)
 778 {
 779         ModelAction *parent = get_last_action(tid);
 780         if (!parent)
 781                 parent = get_thread(tid)->get_creation();
 782         return parent;
 783 }
 784
 785 /**
 786  * Returns the clock vector for a given thread.
 787  * @param tid The thread whose clock vector we want
 788  * @return Desired clock vector
 789  */
 790 ClockVector * ModelChecker::get_cv(thread_id_t tid)
 791 {
 792         return get_parent_action(tid)->get_cv();
 793 }
 794
 795 /**
 796  * Resolve a set of Promises with a current write. The set is provided in the
 797  * Node corresponding to @a write.
 798  * @param write The ModelAction that is fulfilling Promises
 799  * @return True if promises were resolved; false otherwise
 800  */
 801 bool ModelChecker::resolve_promises(ModelAction *write)
 802 {
 803         bool resolved = false;
 804         for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
 805                 Promise *promise = (*promises)[promise_index];
 806                 if (write->get_node()->get_promise(i)) {
 807                         ModelAction *read = promise->get_action();
 808                         read->read_from(write);
 809                         r_modification_order(read, write);
 810                         post_r_modification_order(read, write);
 811                         promises->erase(promises->begin() + promise_index);
 812                         resolved = true;
 813                 } else
 814                         promise_index++;
 815         }
 816
 817         return resolved;
 818 }
 819
 820 /**
 821  * Compute the set of promises that could potentially be satisfied by this
 822  * action. Note that the set computation actually appears in the Node, not in
 823  * ModelChecker.
 824  * @param curr The ModelAction that may satisfy promises
 825  */
 826 void ModelChecker::compute_promises(ModelAction *curr)
 827 {
 828         for (unsigned int i = 0; i < promises->size(); i++) {
 829                 Promise *promise = (*promises)[i];
 830                 const ModelAction *act = promise->get_action();
 831                 if (!act->happens_before(curr) &&
 832                                 act->is_read() &&
 833                                 !act->is_synchronizing(curr) &&
 834                                 !act->same_thread(curr) &&
 835                                 promise->get_value() == curr->get_value()) {
 836                         curr->get_node()->set_promise(i);
 837                 }
 838         }
 839 }
 840
 841 /** Checks promises in response to change in ClockVector Threads. */
 842 void ModelChecker::check_promises(ClockVector *old_cv, ClockVector *merge_cv)
 843 {
 844         for (unsigned int i = 0; i < promises->size(); i++) {
 845                 Promise *promise = (*promises)[i];
 846                 const ModelAction *act = promise->get_action();
 847                 if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
 848                                 merge_cv->synchronized_since(act)) {
 849                         //This thread is no longer able to send values back to satisfy the promise
 850                         int num_synchronized_threads = promise->increment_threads();
 851                         if (num_synchronized_threads == get_num_threads()) {
 852                                 //Promise has failed
 853                                 failed_promise = true;
 854                                 return;
 855                         }
 856                 }
 857         }
 858 }
 859
 860 /**
 861  * Build up an initial set of all past writes that this 'read' action may read
 862  * from. This set is determined by the clock vector's "happens before"
 863  * relationship.
 864  * @param curr is the current ModelAction that we are exploring; it must be a
 865  * 'read' operation.
 866  */
 867 void ModelChecker::build_reads_from_past(ModelAction *curr)
 868 {
 869         std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(curr->get_location());
 870         unsigned int i;
 871         ASSERT(curr->is_read());
 872
 873         ModelAction *last_seq_cst = NULL;
 874
 875         /* Track whether this object has been initialized */
 876         bool initialized = false;
 877
 878         if (curr->is_seqcst()) {
 879                 last_seq_cst = get_last_seq_cst(curr->get_location());
 880                 /* We have to at least see the last sequentially consistent write,
 881                          so we are initialized. */
 882                 if (last_seq_cst != NULL)
 883                         initialized = true;
 884         }
 885
 886         /* Iterate over all threads */
 887         for (i = 0; i < thrd_lists->size(); i++) {
 888                 /* Iterate over actions in thread, starting from most recent */
 889                 action_list_t *list = &(*thrd_lists)[i];
 890                 action_list_t::reverse_iterator rit;
 891                 for (rit = list->rbegin(); rit != list->rend(); rit++) {
 892                         ModelAction *act = *rit;
 893
 894                         /* Only consider 'write' actions */
 895                         if (!act->is_write())
 896                                 continue;
 897
 898                         /* Don't consider more than one seq_cst write if we are a seq_cst read. */
 899                         if (!act->is_seqcst() || !curr->is_seqcst() || act == last_seq_cst) {
 900                                 DEBUG("Adding action to may_read_from:\n");
 901                                 if (DBG_ENABLED()) {
 902                                         act->print();
 903                                         curr->print();
 904                                 }
 905                                 curr->get_node()->add_read_from(act);
 906                         }
 907
 908                         /* Include at most one act per-thread that "happens before" curr */
 909                         if (act->happens_before(curr)) {
 910                                 initialized = true;
 911                                 break;
 912                         }
 913                 }
 914         }
 915
 916         if (!initialized) {
 917                 /** @todo Need a more informative way of reporting errors. */
 918                 printf("ERROR: may read from uninitialized atomic\n");
 919         }
 920
 921         if (DBG_ENABLED() || !initialized) {
 922                 printf("Reached read action:\n");
 923                 curr->print();
 924                 printf("Printing may_read_from\n");
 925                 curr->get_node()->print_may_read_from();
 926                 printf("End printing may_read_from\n");
 927         }
 928
 929         ASSERT(initialized);
 930 }
 931
 932 static void print_list(action_list_t *list)
 933 {
 934         action_list_t::iterator it;
 935
 936         printf("---------------------------------------------------------------------\n");
 937         printf("Trace:\n");
 938
 939         for (it = list->begin(); it != list->end(); it++) {
 940                 (*it)->print();
 941         }
 942         printf("---------------------------------------------------------------------\n");
 943 }
 944
 945 void ModelChecker::print_summary()
 946 {
 947         printf("\n");
 948         printf("Number of executions: %d\n", num_executions);
 949         printf("Total nodes created: %d\n", node_stack->get_total_nodes());
 950
 951         scheduler->print();
 952
 953         if (!isfinalfeasible())
 954                 printf("INFEASIBLE EXECUTION!\n");
 955         print_list(action_trace);
 956         printf("\n");
 957 }
 958
 959 /**
 960  * Add a Thread to the system for the first time. Should only be called once
 961  * per thread.
 962  * @param t The Thread to add
 963  */
 964 void ModelChecker::add_thread(Thread *t)
 965 {
 966         thread_map->put(id_to_int(t->get_id()), t);
 967         scheduler->add_thread(t);
 968 }
 969
 970 void ModelChecker::remove_thread(Thread *t)
 971 {
 972         scheduler->remove_thread(t);
 973 }
 974
 975 /**
 976  * Switch from a user-context to the "master thread" context (a.k.a. system
 977  * context). This switch is made with the intention of exploring a particular
 978  * model-checking action (described by a ModelAction object). Must be called
 979  * from a user-thread context.
 980  * @param act The current action that will be explored. Must not be NULL.
 981  * @return Return status from the 'swap' call (i.e., success/fail, 0/-1)
 982  */
 983 int ModelChecker::switch_to_master(ModelAction *act)
 984 {
 985         DBG();
 986         Thread *old = thread_current();
 987         set_current_action(act);
 988         old->set_state(THREAD_READY);
 989         return Thread::swap(old, &system_context);
 990 }
 991
 992 /**
 993  * Takes the next step in the execution, if possible.
 994  * @return Returns true (success) if a step was taken and false otherwise.
 995  */
 996 bool ModelChecker::take_step() {
 997         Thread *curr, *next;
 998
 999         if (has_asserted())
1000                 return false;
1001
1002         curr = thread_current();
1003         if (curr) {
1004                 if (curr->get_state() == THREAD_READY) {
1005                         ASSERT(priv->current_action);
1006                         priv->nextThread = check_current_action(priv->current_action);
1007                         priv->current_action = NULL;
1008                         if (!curr->is_blocked() && !curr->is_complete())
1009                                 scheduler->add_thread(curr);
1010                 } else {
1011                         ASSERT(false);
1012                 }
1013         }
1014         next = scheduler->next_thread(priv->nextThread);
1015
1016         /* Infeasible -> don't take any more steps */
1017         if (!isfeasible())
1018                 return false;
1019
1020         if (next)
1021                 next->set_state(THREAD_RUNNING);
1022         DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
1023
1024         /* next == NULL -> don't take any more steps */
1025         if (!next)
1026                 return false;
1027         /* Return false only if swap fails with an error */
1028         return (Thread::swap(&system_context, next) == 0);
1029 }
1030
1031 /** Runs the current execution until threre are no more steps to take. */
1032 void ModelChecker::finish_execution() {
1033         DBG();
1034
1035         while (take_step());
1036 }