action.cc

   1 #include <stdio.h>
   2 #define __STDC_FORMAT_MACROS
   3 #include <inttypes.h>
   4
   5 #include "model.h"
   6 #include "action.h"
   7 #include "clockvector.h"
   8 #include "common.h"
   9 #include "threads-model.h"
  10 #include "nodestack.h"
  11
  12 #define ACTION_INITIAL_CLOCK 0
  13
  14 /** A special value to represent a successful trylock */
  15 #define VALUE_TRYSUCCESS 1
  16
  17 /** A special value to represent a failed trylock */
  18 #define VALUE_TRYFAILED 0
  19
  20 /**
  21  * @brief Construct a new ModelAction
  22  *
  23  * @param type The type of action
  24  * @param order The memory order of this action. A "don't care" for non-ATOMIC
  25  * actions (e.g., THREAD_* or MODEL_* actions).
  26  * @param loc The location that this action acts upon
  27  * @param value (optional) A value associated with the action (e.g., the value
  28  * read or written). Defaults to a given macro constant, for debugging purposes.
  29  * @param thread (optional) The Thread in which this action occurred. If NULL
  30  * (default), then a Thread is assigned according to the scheduler.
  31  */
  32 ModelAction::ModelAction(action_type_t type, memory_order order, void *loc,
  33                 uint64_t value, Thread *thread) :
  34         type(type),
  35         order(order),
  36         location(loc),
  37         value(value),
  38         reads_from(NULL),
  39         reads_from_promise(NULL),
  40         last_fence_release(NULL),
  41         node(NULL),
  42         seq_number(ACTION_INITIAL_CLOCK),
  43         cv(NULL),
  44         sleep_flag(false)
  45 {
  46         /* References to NULL atomic variables can end up here */
  47         ASSERT(loc || type == ATOMIC_FENCE || type == MODEL_FIXUP_RELSEQ);
  48
  49         Thread *t = thread ? thread : thread_current();
  50         this->tid = t->get_id();
  51 }
  52
  53 /** @brief ModelAction destructor */
  54 ModelAction::~ModelAction()
  55 {
  56         /**
  57          * We can't free the clock vector:
  58          * Clock vectors are snapshotting state. When we delete model actions,
  59          * they are at the end of the node list and have invalid old clock
  60          * vectors which have already been rolled back to an unallocated state.
  61          */
  62
  63         /*
  64          if (cv)
  65                 delete cv; */
  66 }
  67
  68 void ModelAction::copy_from_new(ModelAction *newaction)
  69 {
  70         seq_number = newaction->seq_number;
  71 }
  72
  73 void ModelAction::set_seq_number(modelclock_t num)
  74 {
  75         /* ATOMIC_UNINIT actions should never have non-zero clock */
  76         ASSERT(!is_uninitialized());
  77         ASSERT(seq_number == ACTION_INITIAL_CLOCK);
  78         seq_number = num;
  79 }
  80
  81 bool ModelAction::is_thread_start() const
  82 {
  83         return type == THREAD_START;
  84 }
  85
  86 bool ModelAction::is_thread_join() const
  87 {
  88         return type == THREAD_JOIN;
  89 }
  90
  91 bool ModelAction::is_relseq_fixup() const
  92 {
  93         return type == MODEL_FIXUP_RELSEQ;
  94 }
  95
  96 bool ModelAction::is_mutex_op() const
  97 {
  98         return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK || type == ATOMIC_WAIT || type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
  99 }
 100
 101 bool ModelAction::is_lock() const
 102 {
 103         return type == ATOMIC_LOCK;
 104 }
 105
 106 bool ModelAction::is_wait() const {
 107         return type == ATOMIC_WAIT;
 108 }
 109
 110 bool ModelAction::is_notify() const {
 111         return type == ATOMIC_NOTIFY_ONE || type == ATOMIC_NOTIFY_ALL;
 112 }
 113
 114 bool ModelAction::is_notify_one() const {
 115         return type == ATOMIC_NOTIFY_ONE;
 116 }
 117
 118 bool ModelAction::is_unlock() const
 119 {
 120         return type == ATOMIC_UNLOCK;
 121 }
 122
 123 bool ModelAction::is_trylock() const
 124 {
 125         return type == ATOMIC_TRYLOCK;
 126 }
 127
 128 bool ModelAction::is_success_lock() const
 129 {
 130         return type == ATOMIC_LOCK || (type == ATOMIC_TRYLOCK && value == VALUE_TRYSUCCESS);
 131 }
 132
 133 bool ModelAction::is_failed_trylock() const
 134 {
 135         return (type == ATOMIC_TRYLOCK && value == VALUE_TRYFAILED);
 136 }
 137
 138 /** @return True if this operation is performed on a C/C++ atomic variable */
 139 bool ModelAction::is_atomic_var() const
 140 {
 141         return is_read() || could_be_write();
 142 }
 143
 144 bool ModelAction::is_uninitialized() const
 145 {
 146         return type == ATOMIC_UNINIT;
 147 }
 148
 149 bool ModelAction::is_read() const
 150 {
 151         return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW;
 152 }
 153
 154 bool ModelAction::is_write() const
 155 {
 156         return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT || type == ATOMIC_UNINIT;
 157 }
 158
 159 bool ModelAction::could_be_write() const
 160 {
 161         return is_write() || is_rmwr();
 162 }
 163
 164 bool ModelAction::is_yield() const
 165 {
 166         return type == THREAD_YIELD;
 167 }
 168
 169 bool ModelAction::is_rmwr() const
 170 {
 171         return type == ATOMIC_RMWR;
 172 }
 173
 174 bool ModelAction::is_rmw() const
 175 {
 176         return type == ATOMIC_RMW;
 177 }
 178
 179 bool ModelAction::is_rmwc() const
 180 {
 181         return type == ATOMIC_RMWC;
 182 }
 183
 184 bool ModelAction::is_fence() const
 185 {
 186         return type == ATOMIC_FENCE;
 187 }
 188
 189 bool ModelAction::is_initialization() const
 190 {
 191         return type == ATOMIC_INIT;
 192 }
 193
 194 bool ModelAction::is_relaxed() const
 195 {
 196         return order == std::memory_order_relaxed;
 197 }
 198
 199 bool ModelAction::is_acquire() const
 200 {
 201         switch (order) {
 202         case std::memory_order_acquire:
 203         case std::memory_order_acq_rel:
 204         case std::memory_order_seq_cst:
 205                 return true;
 206         default:
 207                 return false;
 208         }
 209 }
 210
 211 bool ModelAction::is_release() const
 212 {
 213         switch (order) {
 214         case std::memory_order_release:
 215         case std::memory_order_acq_rel:
 216         case std::memory_order_seq_cst:
 217                 return true;
 218         default:
 219                 return false;
 220         }
 221 }
 222
 223 bool ModelAction::is_seqcst() const
 224 {
 225         return order == std::memory_order_seq_cst;
 226 }
 227
 228 bool ModelAction::same_var(const ModelAction *act) const
 229 {
 230         if (act->is_wait() || is_wait()) {
 231                 if (act->is_wait() && is_wait()) {
 232                         if (((void *)value) == ((void *)act->value))
 233                                 return true;
 234                 } else if (is_wait()) {
 235                         if (((void *)value) == act->location)
 236                                 return true;
 237                 } else if (act->is_wait()) {
 238                         if (location == ((void *)act->value))
 239                                 return true;
 240                 }
 241         }
 242
 243         return location == act->location;
 244 }
 245
 246 bool ModelAction::same_thread(const ModelAction *act) const
 247 {
 248         return tid == act->tid;
 249 }
 250
 251 void ModelAction::copy_typeandorder(ModelAction * act)
 252 {
 253         this->type = act->type;
 254         this->order = act->order;
 255 }
 256
 257 /**
 258  * Get the Thread which is the operand of this action. This is only valid for
 259  * THREAD_* operations (currently only for THREAD_CREATE and THREAD_JOIN). Note
 260  * that this provides a central place for determining the conventions of Thread
 261  * storage in ModelAction, where we generally aren't very type-safe (e.g., we
 262  * store object references in a (void *) address.
 263  *
 264  * For THREAD_CREATE, this yields the Thread which is created.
 265  * For THREAD_JOIN, this yields the Thread we are joining with.
 266  *
 267  * @return The Thread which this action acts on, if exists; otherwise NULL
 268  */
 269 Thread * ModelAction::get_thread_operand() const
 270 {
 271         if (type == THREAD_CREATE) {
 272                 /* THREAD_CREATE stores its (Thread *) in a thrd_t::priv */
 273                 thrd_t *thrd = (thrd_t *)get_location();
 274                 return thrd->priv;
 275         } else if (type == THREAD_JOIN)
 276                 /* THREAD_JOIN uses (Thread *) for location */
 277                 return (Thread *)get_location();
 278         else
 279                 return NULL;
 280 }
 281
 282 /** This method changes an existing read part of an RMW action into either:
 283  *  (1) a full RMW action in case of the completed write or
 284  *  (2) a READ action in case a failed action.
 285  * @todo  If the memory_order changes, we may potentially need to update our
 286  * clock vector.
 287  */
 288 void ModelAction::process_rmw(ModelAction *act)
 289 {
 290         this->order = act->order;
 291         if (act->is_rmwc())
 292                 this->type = ATOMIC_READ;
 293         else if (act->is_rmw()) {
 294                 this->type = ATOMIC_RMW;
 295                 this->value = act->value;
 296         }
 297 }
 298
 299 /** The is_synchronizing method should only explore interleavings if:
 300  *  (1) the operations are seq_cst and don't commute or
 301  *  (2) the reordering may establish or break a synchronization relation.
 302  *  Other memory operations will be dealt with by using the reads_from
 303  *  relation.
 304  *
 305  *  @param act is the action to consider exploring a reordering.
 306  *  @return tells whether we have to explore a reordering.
 307  */
 308 bool ModelAction::could_synchronize_with(const ModelAction *act) const
 309 {
 310         // Same thread can't be reordered
 311         if (same_thread(act))
 312                 return false;
 313
 314         // Different locations commute
 315         if (!same_var(act))
 316                 return false;
 317
 318         // Explore interleavings of seqcst writes/fences to guarantee total
 319         // order of seq_cst operations that don't commute
 320         if ((could_be_write() || act->could_be_write() || is_fence() || act->is_fence()) && is_seqcst() && act->is_seqcst())
 321                 return true;
 322
 323         // Explore synchronizing read/write pairs
 324         if (is_acquire() && act->is_release() && is_read() && act->could_be_write())
 325                 return true;
 326
 327         // lock just released...we can grab lock
 328         if ((is_lock() || is_trylock()) && (act->is_unlock() || act->is_wait()))
 329                 return true;
 330
 331         // lock just acquired...we can fail to grab lock
 332         if (is_trylock() && act->is_success_lock())
 333                 return true;
 334
 335         // other thread stalling on lock...we can release lock
 336         if (is_unlock() && (act->is_trylock() || act->is_lock()))
 337                 return true;
 338
 339         if (is_trylock() && (act->is_unlock() || act->is_wait()))
 340                 return true;
 341
 342         if (is_notify() && act->is_wait())
 343                 return true;
 344
 345         if (is_wait() && act->is_notify())
 346                 return true;
 347
 348         // Otherwise handle by reads_from relation
 349         return false;
 350 }
 351
 352 bool ModelAction::is_conflicting_lock(const ModelAction *act) const
 353 {
 354         // Must be different threads to reorder
 355         if (same_thread(act))
 356                 return false;
 357
 358         // Try to reorder a lock past a successful lock
 359         if (act->is_success_lock())
 360                 return true;
 361
 362         // Try to push a successful trylock past an unlock
 363         if (act->is_unlock() && is_trylock() && value == VALUE_TRYSUCCESS)
 364                 return true;
 365
 366         // Try to push a successful trylock past a wait
 367         if (act->is_wait() && is_trylock() && value == VALUE_TRYSUCCESS)
 368                 return true;
 369
 370         return false;
 371 }
 372
 373 /**
 374  * Create a new clock vector for this action. Note that this function allows a
 375  * user to clobber (and leak) a ModelAction's existing clock vector. A user
 376  * should ensure that the vector has already either been rolled back
 377  * (effectively "freed") or freed.
 378  *
 379  * @param parent A ModelAction from which to inherit a ClockVector
 380  */
 381 void ModelAction::create_cv(const ModelAction *parent)
 382 {
 383         if (parent)
 384                 cv = new ClockVector(parent->cv, this);
 385         else
 386                 cv = new ClockVector(NULL, this);
 387 }
 388
 389 void ModelAction::set_try_lock(bool obtainedlock)
 390 {
 391         value = obtainedlock ? VALUE_TRYSUCCESS : VALUE_TRYFAILED;
 392 }
 393
 394 /**
 395  * @brief Get the value read by this load
 396  *
 397  * We differentiate this function from ModelAction::get_write_value and
 398  * ModelAction::get_value for the purpose of RMW's, which may have both a
 399  * 'read' and a 'write' value.
 400  *
 401  * Note: 'this' must be a load.
 402  *
 403  * @return The value read by this load
 404  */
 405 uint64_t ModelAction::get_reads_from_value() const
 406 {
 407         ASSERT(is_read());
 408         if (reads_from)
 409                 return reads_from->get_write_value();
 410         else if (reads_from_promise)
 411                 return reads_from_promise->get_value();
 412         return VALUE_NONE; /* Only for new actions with no reads-from */
 413 }
 414
 415 /**
 416  * @brief Get the value written by this store
 417  *
 418  * We differentiate this function from ModelAction::get_reads_from_value and
 419  * ModelAction::get_value for the purpose of RMW's, which may have both a
 420  * 'read' and a 'write' value.
 421  *
 422  * Note: 'this' must be a store.
 423  *
 424  * @return The value written by this store
 425  */
 426 uint64_t ModelAction::get_write_value() const
 427 {
 428         ASSERT(is_write());
 429         return value;
 430 }
 431
 432 /**
 433  * @brief Get the value returned by this action
 434  *
 435  * For atomic reads (including RMW), an operation returns the value it read.
 436  * For atomic writes, an operation returns the value it wrote. For other
 437  * operations, the return value varies (sometimes is a "don't care"), but the
 438  * value is simply stored in the "value" field.
 439  *
 440  * @return This action's return value
 441  */
 442 uint64_t ModelAction::get_return_value() const
 443 {
 444         if (is_read())
 445                 return get_reads_from_value();
 446         else if (is_write())
 447                 return get_write_value();
 448         else
 449                 return value;
 450 }
 451
 452 /** @return The Node associated with this ModelAction */
 453 Node * ModelAction::get_node() const
 454 {
 455         /* UNINIT actions do not have a Node */
 456         ASSERT(!is_uninitialized());
 457         return node;
 458 }
 459
 460 /**
 461  * Update the model action's read_from action
 462  * @param act The action to read from; should be a write
 463  */
 464 void ModelAction::set_read_from(const ModelAction *act)
 465 {
 466         ASSERT(act);
 467         reads_from = act;
 468         reads_from_promise = NULL;
 469         if (act->is_uninitialized())
 470                 model->assert_bug("May read from uninitialized atomic\n");
 471 }
 472
 473 /**
 474  * Set this action's read-from promise
 475  * @param promise The promise to read from
 476  */
 477 void ModelAction::set_read_from_promise(Promise *promise)
 478 {
 479         ASSERT(is_read());
 480         reads_from_promise = promise;
 481         reads_from = NULL;
 482 }
 483
 484 /**
 485  * Synchronize the current thread with the thread corresponding to the
 486  * ModelAction parameter.
 487  * @param act The ModelAction to synchronize with
 488  * @return True if this is a valid synchronization; false otherwise
 489  */
 490 bool ModelAction::synchronize_with(const ModelAction *act)
 491 {
 492         if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK)
 493                 return false;
 494         model->check_promises(act->get_tid(), cv, act->cv);
 495         cv->merge(act->cv);
 496         return true;
 497 }
 498
 499 bool ModelAction::has_synchronized_with(const ModelAction *act) const
 500 {
 501         return cv->synchronized_since(act);
 502 }
 503
 504 /**
 505  * Check whether 'this' happens before act, according to the memory-model's
 506  * happens before relation. This is checked via the ClockVector constructs.
 507  * @return true if this action's thread has synchronized with act's thread
 508  * since the execution of act, false otherwise.
 509  */
 510 bool ModelAction::happens_before(const ModelAction *act) const
 511 {
 512         return act->cv->synchronized_since(this);
 513 }
 514
 515 /** @brief Print nicely-formatted info about this ModelAction */
 516 void ModelAction::print() const
 517 {
 518         const char *type_str, *mo_str;
 519         switch (this->type) {
 520         case MODEL_FIXUP_RELSEQ:
 521                 type_str = "relseq fixup";
 522                 break;
 523         case THREAD_CREATE:
 524                 type_str = "thread create";
 525                 break;
 526         case THREAD_START:
 527                 type_str = "thread start";
 528                 break;
 529         case THREAD_YIELD:
 530                 type_str = "thread yield";
 531                 break;
 532         case THREAD_JOIN:
 533                 type_str = "thread join";
 534                 break;
 535         case THREAD_FINISH:
 536                 type_str = "thread finish";
 537                 break;
 538         case ATOMIC_UNINIT:
 539                 type_str = "uninitialized";
 540                 break;
 541         case ATOMIC_READ:
 542                 type_str = "atomic read";
 543                 break;
 544         case ATOMIC_WRITE:
 545                 type_str = "atomic write";
 546                 break;
 547         case ATOMIC_RMW:
 548                 type_str = "atomic rmw";
 549                 break;
 550         case ATOMIC_FENCE:
 551                 type_str = "fence";
 552                 break;
 553         case ATOMIC_RMWR:
 554                 type_str = "atomic rmwr";
 555                 break;
 556         case ATOMIC_RMWC:
 557                 type_str = "atomic rmwc";
 558                 break;
 559         case ATOMIC_INIT:
 560                 type_str = "init atomic";
 561                 break;
 562         case ATOMIC_LOCK:
 563                 type_str = "lock";
 564                 break;
 565         case ATOMIC_UNLOCK:
 566                 type_str = "unlock";
 567                 break;
 568         case ATOMIC_TRYLOCK:
 569                 type_str = "trylock";
 570                 break;
 571         case ATOMIC_WAIT:
 572                 type_str = "wait";
 573                 break;
 574         case ATOMIC_NOTIFY_ONE:
 575                 type_str = "notify one";
 576                 break;
 577         case ATOMIC_NOTIFY_ALL:
 578                 type_str = "notify all";
 579                 break;
 580         default:
 581                 type_str = "unknown type";
 582         }
 583
 584         switch (this->order) {
 585         case std::memory_order_relaxed:
 586                 mo_str = "relaxed";
 587                 break;
 588         case std::memory_order_acquire:
 589                 mo_str = "acquire";
 590                 break;
 591         case std::memory_order_release:
 592                 mo_str = "release";
 593                 break;
 594         case std::memory_order_acq_rel:
 595                 mo_str = "acq_rel";
 596                 break;
 597         case std::memory_order_seq_cst:
 598                 mo_str = "seq_cst";
 599                 break;
 600         default:
 601                 mo_str = "unknown";
 602                 break;
 603         }
 604
 605         model_print("(%4d) Thread: %-2d   Action: %-13s   MO: %7s  Loc: %14p   Value: %-#18" PRIx64,
 606                         seq_number, id_to_int(tid), type_str, mo_str, location, get_return_value());
 607         if (is_read()) {
 608                 if (reads_from)
 609                         model_print("  Rf: %-3d", reads_from->get_seq_number());
 610                 else if (reads_from_promise) {
 611                         int idx = model->get_promise_number(reads_from_promise);
 612                         if (idx >= 0)
 613                                 model_print("  Rf: P%-2d", idx);
 614                         else
 615                                 model_print("  Rf: P? ");
 616                 } else
 617                         model_print("  Rf: ?  ");
 618         }
 619         if (cv) {
 620                 if (is_read())
 621                         model_print(" ");
 622                 else
 623                         model_print("          ");
 624                 cv->print();
 625         } else
 626                 model_print("\n");
 627 }
 628
 629 /** @brief Get a (likely) unique hash for this ModelAction */
 630 unsigned int ModelAction::hash() const
 631 {
 632         unsigned int hash = (unsigned int)this->type;
 633         hash ^= ((unsigned int)this->order) << 3;
 634         hash ^= seq_number << 5;
 635         hash ^= id_to_int(tid) << 6;
 636
 637         if (is_read()) {
 638                if (reads_from)
 639                        hash ^= reads_from->get_seq_number();
 640                else if (reads_from_promise)
 641                        hash ^= model->get_promise_number(reads_from_promise);
 642                hash ^= get_reads_from_value();
 643         }
 644         return hash;
 645 }
 646
 647 /**
 648  * @brief Checks the NodeStack to see if a ModelAction is in our may-read-from set
 649  * @param write The ModelAction to check for
 650  * @return True if the ModelAction is found; false otherwise
 651  */
 652 bool ModelAction::may_read_from(const ModelAction *write) const
 653 {
 654         for (int i = 0; i < node->get_read_from_past_size(); i++)
 655                 if (node->get_read_from_past(i) == write)
 656                         return true;
 657         return false;
 658 }
 659
 660 /**
 661  * @brief Checks the NodeStack to see if a Promise is in our may-read-from set
 662  * @param promise The Promise to check for
 663  * @return True if the Promise is found; false otherwise
 664  */
 665 bool ModelAction::may_read_from(const Promise *promise) const
 666 {
 667         for (int i = 0; i < node->get_read_from_promise_size(); i++)
 668                 if (node->get_read_from_promise(i) == promise)
 669                         return true;
 670         return false;
 671 }
 672
 673 /**
 674  * Only valid for LOCK, TRY_LOCK, UNLOCK, and WAIT operations.
 675  * @return The mutex operated on by this action, if any; otherwise NULL
 676  */
 677 std::mutex * ModelAction::get_mutex() const
 678 {
 679         if (is_trylock() || is_lock() || is_unlock())
 680                 return (std::mutex *)get_location();
 681         else if (is_wait())
 682                 return (std::mutex *)get_value();
 683         else
 684                 return NULL;
 685 }