X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=3aeb7377e2b328fad8b24748744274ab1386e25d;hb=5d87d23f622d396fd2e1c94d61f901429c5f35ac;hp=8dba82f3a8ff7d97967410cfa75b33a84394de98;hpb=59eb730e1d19a0825008c40eb521bfc5c29df5f9;p=model-checker.git diff --git a/action.cc b/action.cc index 8dba82f..3aeb737 100644 --- a/action.cc +++ b/action.cc @@ -12,7 +12,20 @@ #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), @@ -20,9 +33,10 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, uint 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(); } @@ -52,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; @@ -307,6 +326,9 @@ 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; @@ -393,3 +415,18 @@ void ModelAction::print() const } 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; +}