action.cc

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