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