X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=317c6a7cd87d9a94fbb695ecb95615ed5bae5613;hb=09c3eb5539455e82dcb357fbce82bf5974c3a37c;hp=6a545d82a0badac66c25eb58cd124de6d8f892f0;hpb=6144dd79c2f94591ffdb10655322900629bb1b1e;p=model-checker.git diff --git a/action.cc b/action.cc index 6a545d8..317c6a7 100644 --- a/action.cc +++ b/action.cc @@ -31,6 +31,7 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, location(loc), value(value), reads_from(NULL), + reads_from_promise(NULL), last_fence_release(NULL), node(NULL), seq_number(ACTION_INITIAL_CLOCK), @@ -252,10 +253,11 @@ void ModelAction::copy_typeandorder(ModelAction * act) */ Thread * ModelAction::get_thread_operand() const { - if (type == THREAD_CREATE) - /* THREAD_CREATE uses (Thread *) for location */ - return (Thread *)get_location(); - else if (type == THREAD_JOIN) + if (type == THREAD_CREATE) { + /* THREAD_CREATE stores its (Thread *) in a thrd_t::priv */ + thrd_t *thrd = (thrd_t *)get_location(); + return thrd->priv; + } else if (type == THREAD_JOIN) /* THREAD_JOIN uses (Thread *) for location */ return (Thread *)get_location(); else @@ -391,10 +393,22 @@ Node * ModelAction::get_node() const void ModelAction::set_read_from(const ModelAction *act) { reads_from = act; + reads_from_promise = NULL; if (act && act->is_uninitialized()) model->assert_bug("May read from uninitialized atomic\n"); } +/** + * Set this action's read-from promise + * @param promise The promise to read from + */ +void ModelAction::set_read_from_promise(const Promise *promise) +{ + ASSERT(is_read()); + reads_from_promise = promise; + reads_from = NULL; +} + /** * Synchronize the current thread with the thread corresponding to the * ModelAction parameter. @@ -496,8 +510,10 @@ void ModelAction::print() const } uint64_t valuetoprint; - if (type == ATOMIC_READ && reads_from != NULL) + if (is_read() && reads_from) valuetoprint = reads_from->value; + else if (is_read() && reads_from_promise) + valuetoprint = reads_from_promise->get_value(); else valuetoprint = value; @@ -540,7 +556,7 @@ void ModelAction::print() const model_print("\n"); } -/** @brief Print nicely-formatted info about this ModelAction */ +/** @brief Get a (likely) unique hash for this ModelAction */ unsigned int ModelAction::hash() const { unsigned int hash = (unsigned int)this->type;