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