X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=action.cc;h=5e050810e7526408828b27c74cad76fcdef95a4b;hb=e60d8c23d30a0dfe66b8426f7f2ecf576e812028;hp=b4f4e434934cfd0d68adf06ba54bd2b5ada102a0;hpb=80ab61e4168b993a319788c70fd41e63a34ba627;p=model-checker.git diff --git a/action.cc b/action.cc index b4f4e43..5e05081 100644 --- a/action.cc +++ b/action.cc @@ -7,20 +7,36 @@ #include "action.h" #include "clockvector.h" #include "common.h" -#include "threads.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(); } @@ -50,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; @@ -305,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; @@ -391,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; +}