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()
{
delete cv; */
}
+int ModelAction::getSize() const {
+ return size;
+}
+
void ModelAction::copy_from_new(ModelAction *newaction)
{
seq_number = newaction->seq_number;
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
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
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";
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";
};
}
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.,
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;
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;
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);
/** @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;
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));
template <typename T, typename U>
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<const CycleNode *, const CycleNode *, uintptr_t, 4, model_malloc, model_calloc, model_free> *discovered;
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.
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();
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);
__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;} \
projects / c11tester.git / commitdiff