X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=action.cc;h=1a819eaf5584f1e97e88fca439104392c07b7f1b;hp=383be230aaea3f4b505266688fde98ce7a6a8640;hb=4546308ab989c074f83d8607e16f13ffbcff494a;hpb=0ebd310446ea2a5675ee33eb6f9d75e311af7d36 diff --git a/action.cc b/action.cc index 383be23..1a819ea 100644 --- a/action.cc +++ b/action.cc @@ -7,26 +7,52 @@ #include "action.h" #include "clockvector.h" #include "common.h" +#include "threads-model.h" +#include "nodestack.h" #define ACTION_INITIAL_CLOCK 0 -ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value) : +/** + * @brief Construct a new ModelAction + * + * @param type The type of action + * @param order The memory order of this action. A "don't care" for non-ATOMIC + * actions (e.g., THREAD_* or MODEL_* actions). + * @param loc The location that this action acts upon + * @param value (optional) A value associated with the action (e.g., the value + * read or written). Defaults to a given macro constant, for debugging purposes. + * @param thread (optional) The Thread in which this action occurred. If NULL + * (default), then a Thread is assigned according to the scheduler. + */ +ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, + uint64_t value, Thread *thread) : type(type), order(order), location(loc), value(value), reads_from(NULL), + node(NULL), seq_number(ACTION_INITIAL_CLOCK), - cv(NULL) + cv(NULL), + sleep_flag(false) { - Thread *t = thread_current(); + Thread *t = thread ? thread : thread_current(); this->tid = t->get_id(); } +/** @brief ModelAction destructor */ ModelAction::~ModelAction() { - if (cv) - delete cv; + /** + * We can't free the clock vector: + * Clock vectors are snapshotting state. When we delete model actions, + * they are at the end of the node list and have invalid old clock + * vectors which have already been rolled back to an unallocated state. + */ + + /* + if (cv) + delete cv; */ } void ModelAction::copy_from_new(ModelAction *newaction) @@ -40,6 +66,11 @@ void ModelAction::set_seq_number(modelclock_t num) seq_number = num; } +bool ModelAction::is_relseq_fixup() const +{ + return type == MODEL_FIXUP_RELSEQ; +} + bool ModelAction::is_mutex_op() const { return type == ATOMIC_LOCK || type == ATOMIC_TRYLOCK || type == ATOMIC_UNLOCK; @@ -80,6 +111,11 @@ bool ModelAction::is_write() const return type == ATOMIC_WRITE || type == ATOMIC_RMW || type == ATOMIC_INIT; } +bool ModelAction::could_be_write() const +{ + return is_write() || is_rmwr(); +} + bool ModelAction::is_rmwr() const { return type == ATOMIC_RMWR; @@ -174,7 +210,7 @@ void ModelAction::process_rmw(ModelAction * act) { * @param act is the action to consider exploring a reordering. * @return tells whether we have to explore a reordering. */ -bool ModelAction::is_synchronizing(const ModelAction *act) const +bool ModelAction::could_synchronize_with(const ModelAction *act) const { //Same thread can't be reordered if (same_thread(act)) @@ -186,13 +222,11 @@ bool ModelAction::is_synchronizing(const ModelAction *act) const // Explore interleavings of seqcst writes to guarantee total order // of seq_cst operations that don't commute - if (is_write() && is_seqcst() && act->is_write() && act->is_seqcst()) + if ((could_be_write() || act->could_be_write()) && is_seqcst() && act->is_seqcst()) return true; // Explore synchronizing read/write pairs - if (is_read() && is_acquire() && act->is_write() && act->is_release()) - return true; - if (is_write() && is_release() && act->is_read() && act->is_acquire()) + if (is_read() && is_acquire() && act->could_be_write() && act->is_release()) return true; // Otherwise handle by reads_from relation @@ -239,18 +273,27 @@ void ModelAction::set_try_lock(bool obtainedlock) { value=VALUE_TRYFAILED; } -/** Update the model action's read_from action */ -void ModelAction::read_from(const ModelAction *act) +/** + * Update the model action's read_from action + * @param act The action to read from; should be a write + * @return True if this read established synchronization + */ +bool ModelAction::read_from(const ModelAction *act) { ASSERT(cv); reads_from = act; if (act != NULL && this->is_acquire()) { rel_heads_list_t release_heads; model->get_release_seq_heads(this, &release_heads); + int num_heads = release_heads.size(); for (unsigned int i = 0; i < release_heads.size(); i++) - if (!synchronize_with(release_heads[i])) + if (!synchronize_with(release_heads[i])) { model->set_bad_synchronization(); + num_heads--; + } + return num_heads > 0; } + return false; } /** @@ -262,7 +305,7 @@ void ModelAction::read_from(const ModelAction *act) bool ModelAction::synchronize_with(const ModelAction *act) { if (*this < *act && type != THREAD_JOIN && type != ATOMIC_LOCK) return false; - model->check_promises(cv, act->cv); + model->check_promises(act->get_tid(), cv, act->cv); cv->merge(act->cv); return true; } @@ -283,16 +326,14 @@ bool ModelAction::happens_before(const ModelAction *act) const return act->cv->synchronized_since(this); } -/** - * Print nicely-formatted info about this ModelAction - * - * @param print_cv True if we want to print clock vector data. Might be false, - * for instance, in situations where the clock vector might be invalid - */ -void ModelAction::print(bool print_cv) const +/** @brief Print nicely-formatted info about this ModelAction */ +void ModelAction::print() const { const char *type_str, *mo_str; switch (this->type) { + case MODEL_FIXUP_RELSEQ: + type_str = "relseq fixup"; + break; case THREAD_CREATE: type_str = "thread create"; break; @@ -373,9 +414,24 @@ void ModelAction::print(bool print_cv) const else printf(" Rf: ?"); } - if (cv && print_cv) { + if (cv) { printf("\t"); cv->print(); } else printf("\n"); } + +/** @brief Print nicely-formatted info about this ModelAction */ +unsigned int ModelAction::hash() const +{ + unsigned int hash=(unsigned int) this->type; + hash^=((unsigned int)this->order)<<3; + hash^=seq_number<<5; + hash^=tid<<6; + + if (is_read()) { + if (reads_from) + hash^=reads_from->get_seq_number(); + } + return hash; +}