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