From f750120c93252f2b677c4b07d003fc71fcdaaa00 Mon Sep 17 00:00:00 2001 From: bdemsky Date: Mon, 10 Jun 2019 20:43:00 -0700 Subject: [PATCH 1/1] Fix RMW bug --- action.cc | 51 +++++++++++++++++++++++++++++++++++++++++---- action.h | 12 ++++++++--- cmodelint.cc | 9 ++++++++ cyclegraph.h | 3 +-- execution.cc | 30 ++++++++++++++++++++++++++ include/cmodelint.h | 1 + include/impatomic.h | 2 +- 7 files changed, 98 insertions(+), 10 deletions(-) diff --git a/action.cc b/action.cc index b9f3d07d..8c29c533 100644 --- a/action.cc +++ b/action.cc @@ -51,6 +51,39 @@ ModelAction::ModelAction(action_type_t type, memory_order order, void *loc, this->tid = t->get_id(); } + +/** + * @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 size (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, int size) : + type(type), + order(order), + original_order(order), + location(loc), + value(value), + reads_from(NULL), + last_fence_release(NULL), + node(NULL), + seq_number(ACTION_INITIAL_CLOCK), + cv(NULL) +{ + /* References to NULL atomic variables can end up here */ + ASSERT(loc); + this->size = size; + Thread *t = thread_current(); + this->tid = t->get_id(); +} + /** @brief ModelAction destructor */ ModelAction::~ModelAction() { @@ -66,6 +99,10 @@ ModelAction::~ModelAction() delete cv; */ } +int ModelAction::getSize() const { + return size; +} + void ModelAction::copy_from_new(ModelAction *newaction) { seq_number = newaction->seq_number; @@ -144,7 +181,7 @@ bool ModelAction::is_uninitialized() const bool ModelAction::is_read() const { - return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMW; + return type == ATOMIC_READ || type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS || type == ATOMIC_RMW; } bool ModelAction::is_write() const @@ -164,7 +201,12 @@ bool ModelAction::is_yield() const bool ModelAction::is_rmwr() const { - return type == ATOMIC_RMWR; + return type == ATOMIC_RMWR || type == ATOMIC_RMWRCAS; +} + +bool ModelAction::is_rmwrcas() const +{ + return type == ATOMIC_RMWRCAS; } bool ModelAction::is_rmw() const @@ -544,6 +586,7 @@ const char * ModelAction::get_type_str() const case ATOMIC_RMW: return "atomic rmw"; case ATOMIC_FENCE: return "fence"; case ATOMIC_RMWR: return "atomic rmwr"; + case ATOMIC_RMWRCAS: return "atomic rmwrcas"; case ATOMIC_RMWC: return "atomic rmwc"; case ATOMIC_INIT: return "init atomic"; case ATOMIC_LOCK: return "lock"; @@ -551,8 +594,8 @@ const char * ModelAction::get_type_str() const case ATOMIC_TRYLOCK: return "trylock"; case ATOMIC_WAIT: return "wait"; case ATOMIC_NOTIFY_ONE: return "notify one"; - case ATOMIC_NOTIFY_ALL: return "notify all"; - case ATOMIC_ANNOTATION: return "annotation"; + case ATOMIC_NOTIFY_ALL: return "notify all"; + case ATOMIC_ANNOTATION: return "annotation"; default: return "unknown type"; }; } diff --git a/action.h b/action.h index e78bb9c5..760e9fb0 100644 --- a/action.h +++ b/action.h @@ -59,6 +59,7 @@ typedef enum action_type { ATOMIC_READ, /**< An atomic read action */ ATOMIC_WRITE, /**< An atomic write action */ ATOMIC_RMWR, /**< The read part of an atomic RMW action */ + ATOMIC_RMWRCAS, /**< The read part of an atomic RMW action */ ATOMIC_RMW, /**< The write part of an atomic RMW action */ ATOMIC_RMWC, /**< Convert an atomic RMW action into a READ */ ATOMIC_INIT, /**< Initialization of an atomic object (e.g., @@ -87,6 +88,7 @@ typedef enum action_type { class ModelAction { public: ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value = VALUE_NONE, Thread *thread = NULL); + ModelAction(action_type_t type, memory_order order, void *loc, uint64_t value, int size); ~ModelAction(); void print() const; @@ -136,6 +138,7 @@ public: bool is_yield() const; bool could_be_write() const; bool is_rmwr() const; + bool is_rmwrcas() const; bool is_rmwc() const; bool is_rmw() const; bool is_fence() const; @@ -149,7 +152,8 @@ public: bool same_thread(const ModelAction *act) const; bool is_conflicting_lock(const ModelAction *act) const; bool could_synchronize_with(const ModelAction *act) const; - + int getSize() const; + Thread * get_thread_operand() const; void create_cv(const ModelAction *parent = NULL); @@ -203,13 +207,15 @@ private: /** @brief The value written (for write or RMW; undefined for read) */ uint64_t value; - /** + union { + /** * @brief The store that this action reads from * * Only valid for reads */ const ModelAction *reads_from; - + int size; + }; /** @brief The last fence release from the same thread */ const ModelAction *last_fence_release; diff --git a/cmodelint.cc b/cmodelint.cc index 15d6151b..fc80b299 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -33,6 +33,15 @@ uint64_t model_rmwr_action(void *obj, memory_order ord) { return model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj)); } +/** + * Performs the read part of a RMW CAS action. The next action must + * either be the write part of the RMW action or an explicit close out + * of the RMW action w/o a write. + */ +uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oldval, int size) { + return model->switch_to_master(new ModelAction(ATOMIC_RMWRCAS, ord, obj, oldval, size)); +} + /** Performs the write part of a RMW action. */ void model_rmw_action(void *obj, memory_order ord, uint64_t val) { model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val)); diff --git a/cyclegraph.h b/cyclegraph.h index b9807fca..556af1cf 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -46,14 +46,13 @@ class CycleGraph { template void dot_print_edge(FILE *file, const T *from, const U *to, const char *prop); #endif - + CycleNode * getNode_noCreate(const ModelAction *act) const; SNAPSHOTALLOC private: bool addNodeEdge(CycleNode *fromnode, CycleNode *tonode); void putNode(const ModelAction *act, CycleNode *node); CycleNode * getNode(const ModelAction *act); - CycleNode * getNode_noCreate(const ModelAction *act) const; bool mergeNodes(CycleNode *node1, CycleNode *node2); HashTable *discovered; diff --git a/execution.cc b/execution.cc index a6ed9d68..b08bbcf9 100644 --- a/execution.cc +++ b/execution.cc @@ -1294,6 +1294,22 @@ ClockVector * ModelExecution::get_cv(thread_id_t tid) const return get_parent_action(tid)->get_cv(); } +bool valequals(uint64_t val1, uint64_t val2, int size) { + switch(size) { + case 1: + return ((uint8_t)val1) == ((uint8_t)val2); + case 2: + return ((uint16_t)val1) == ((uint16_t)val2); + case 4: + return ((uint32_t)val1) == ((uint32_t)val2); + case 8: + return val1==val2; + default: + ASSERT(0); + return false; + } +} + /** * Build up an initial set of all past writes that this 'read' action may read * from, as well as any previously-observed future values that must still be valid. @@ -1332,6 +1348,20 @@ ModelVector * ModelExecution::build_may_read_from(ModelAction *c if (curr->is_seqcst() && (act->is_seqcst() || (last_sc_write != NULL && act->happens_before(last_sc_write))) && act != last_sc_write) allow_read = false; + /* Need to check whether we will have two RMW reading from the same value */ + if (curr->is_rmwr()) { + /* It is okay if we have a failing CAS */ + if (!curr->is_rmwrcas() || + valequals(curr->get_value(), act->get_value(), curr->getSize())) { + //Need to make sure we aren't the second RMW + CycleNode * node = mo_graph->getNode_noCreate(act); + if (node != NULL && node->getRMW() != NULL) { + //we are the second RMW + allow_read = false; + } + } + } + if (allow_read) { /* Only add feasible reads */ mo_graph->startChanges(); diff --git a/include/cmodelint.h b/include/cmodelint.h index 1c456b89..d5a04867 100644 --- a/include/cmodelint.h +++ b/include/cmodelint.h @@ -16,6 +16,7 @@ uint64_t model_read_action(void * obj, memory_order ord); void model_write_action(void * obj, memory_order ord, uint64_t val); void model_init_action(void * obj, uint64_t val); uint64_t model_rmwr_action(void *obj, memory_order ord); +uint64_t model_rmwrcas_action(void *obj, memory_order ord, uint64_t oval, int size); void model_rmw_action(void *obj, memory_order ord, uint64_t val); void model_rmwc_action(void *obj, memory_order ord); void model_fence_action(memory_order ord); diff --git a/include/impatomic.h b/include/impatomic.h index 100ad0d6..70b77de2 100644 --- a/include/impatomic.h +++ b/include/impatomic.h @@ -118,7 +118,7 @@ inline void atomic_flag::clear( memory_order __x__ ) volatile __typeof__(__e__) __q__ = (__e__); \ __typeof__(__m__) __v__ = (__m__); \ bool __r__; \ - __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \ + __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwrcas_action((void *)__p__, __x__, (uint64_t) * __q__, sizeof((__a__)->__f__)); \ if (__t__ == * __q__ ) {; \ model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \ else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \ -- 2.34.1