return tid == act->tid;
}
-void ModelAction::upgrade_rmw(ModelAction * act) {
- ASSERT(is_read());
- ASSERT(act->is_rmw());
- //Upgrade our type to the act's type
+void ModelAction::copy_typeandorder(ModelAction * act) {
this->type=act->type;
this->order=act->order;
- this->value=act->value;
+}
+
+void ModelAction::process_rmw(ModelAction * act) {
+ this->order=act->order;
+ if (act->is_rmwc())
+ this->type=ATOMIC_READ;
+ else if (act->is_rmw()) {
+ this->type=ATOMIC_RMW;
+ this->value=act->value;
+ }
}
/** The is_synchronizing method should only explore interleavings if:
type_str = "unknown type";
}
- uint64_t valuetoprint=type==ATOMIC_READ?reads_from->value:value;
+ uint64_t valuetoprint=type==ATOMIC_READ?(reads_from!=NULL?reads_from->value:VALUE_NONE):value;
printf("(%3d) Thread: %-2d Action: %-13s MO: %d Loc: %14p Value: %-12" PRIu64,
seq_number, id_to_int(tid), type_str, order, location, valuetoprint);
return get_seq_number() > act.get_seq_number();
}
- void upgrade_rmw(ModelAction * act);
+ void process_rmw(ModelAction * act);
+ void copy_typeandorder(ModelAction * act);
MEMALLOC
private:
model->switch_to_master(new ModelAction(ATOMIC_INIT, memory_order_relaxed, obj, val));
}
+uint64_t model_rmwr_action(void *obj, memory_order ord) {
+ model->switch_to_master(new ModelAction(ATOMIC_RMWR, ord, obj));
+ return thread_current()->get_return_value();
+}
+
void model_rmw_action(void *obj, memory_order ord, uint64_t val) {
model->switch_to_master(new ModelAction(ATOMIC_RMW, ord, obj, val));
}
+
+void model_rmwc_action(void *obj, memory_order ord) {
+ model->switch_to_master(new ModelAction(ATOMIC_RMWC, ord, obj));
+}
uint64_t model_read_action(void * obj, memory_order ord);
void model_write_action(void * obj, memory_order ord, uint64_t val);
-void model_rmw_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);
+void model_rmw_action(void *obj, memory_order ord, uint64_t val);
+void model_rmwc_action(void *obj, memory_order ord);
+
#if __cplusplus
}
}
/** Adds an edge between two ModelActions. */
-void CycleGraph::addEdge(const ModelAction *from, const ModelAction *to) {
+
+//the event to happens after the event from
+
+void CycleGraph::addEdge(const ModelAction *to, const ModelAction *from) {
CycleNode *fromnode=getNode(from);
CycleNode *tonode=getNode(to);
+
if (!hasCycles) {
// Check for Cycles
hasCycles=checkReachable(tonode, fromnode);
}
fromnode->addEdge(tonode);
+
+ CycleNode * rmwnode=fromnode->getRMW();
+
+ //If the fromnode has a rmwnode that is not the tonode, we
+ //should add an edge between its rmwnode and the tonode
+
+ if (rmwnode!=NULL&&rmwnode!=tonode) {
+ if (!hasCycles) {
+ // Check for Cycles
+ hasCycles=checkReachable(tonode, rmwnode);
+ }
+ rmwnode->addEdge(tonode);
+ }
}
-void CycleGraph::addRMWEdge(const ModelAction *from, const ModelAction *rmw) {
+//event rmw that reads from the node from
+
+void CycleGraph::addRMWEdge(const ModelAction *rmw, const ModelAction * from) {
CycleNode *fromnode=getNode(from);
CycleNode *rmwnode=getNode(rmw);
/* Two RMW actions cannot read from the same write. */
- if (fromnode->setRMW())
+ if (fromnode->setRMW(rmwnode)) {
hasCycles=true;
+ }
/* Transfer all outgoing edges from the from node to the rmw node */
/* This process cannot add a cycle because rmw should not have any
incoming edges yet.*/
std::vector<CycleNode *> * edges=fromnode->getEdges();
- for(unsigned int i=0;edges->size();i++) {
+ for(unsigned int i=0;i<edges->size();i++) {
CycleNode * tonode=(*edges)[i];
rmwnode->addEdge(tonode);
}
- if (!hasCycles) {
- hasCycles=checkReachable(rmwnode, fromnode);
- }
+
fromnode->addEdge(rmwnode);
}
/** Constructor for a CycleNode. */
CycleNode::CycleNode(const ModelAction *modelaction) {
action=modelaction;
+ hasRMW=NULL;
}
/** Returns a vector of the edges from a CycleNode. */
edges.push_back(node);
}
-bool CycleNode::setRMW() {
- bool oldhasRMW=hasRMW;
- hasRMW=true;
- return oldhasRMW;
+CycleNode* CycleNode::getRMW() {
+ return hasRMW;
+}
+
+bool CycleNode::setRMW(CycleNode * node) {
+ CycleNode * oldhasRMW=hasRMW;
+ hasRMW=node;
+ return (oldhasRMW!=NULL);
}
CycleNode(const ModelAction *action);
void addEdge(CycleNode * node);
std::vector<CycleNode *> * getEdges();
- bool setRMW();
+ bool setRMW(CycleNode *);
+ CycleNode* getRMW();
private:
const ModelAction *action;
std::vector<CycleNode *> edges;
- bool hasRMW;
+ CycleNode * hasRMW;
};
#endif
bool atomic_flag_test_and_set_explicit ( volatile atomic_flag * __a__, memory_order __x__ ) {
volatile bool * __p__ = &((__a__)->__f__);
- model->switch_to_master(new ModelAction(ATOMIC_READ, __x__, (void *) __p__));
+ model->switch_to_master(new ModelAction(ATOMIC_RMWR, __x__, (void *) __p__));
bool result = (bool) thread_current()->get_return_value();
model->switch_to_master(new ModelAction(ATOMIC_RMW, __x__, (void *) __p__, true));
return result;
#define _ATOMIC_MODIFY_( __a__, __o__, __m__, __x__ ) \
({ volatile __typeof__((__a__)->__f__)* __p__ = & ((__a__)->__f__); \
- __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_read_action((void *)__p__, __x__); \
+ __typeof__((__a__)->__f__) __old__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__); \
__typeof__(__m__) __v__ = (__m__); \
__typeof__((__a__)->__f__) __copy__= __old__; \
__copy__ __o__ __v__; \
__typeof__(__e__) __q__ = (__e__); \
__typeof__(__m__) __v__ = (__m__); \
bool __r__; \
- __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_read_action((void *)__p__, __x__);\
+ __typeof__((__a__)->__f__) __t__=(__typeof__((__a__)->__f__)) model_rmwr_action((void *)__p__, __x__);\
if (__t__ == * __q__ ) { \
model_rmw_action((void *)__p__, __x__, (uint64_t) __v__); __r__ = true; } \
- else { *__q__ = __t__; __r__ = false;} \
+ else { model_rmwc_action((void *)__p__, __x__); *__q__ = __t__; __r__ = false;} \
__r__; })
//TODO
( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
{
void* volatile* __p__ = &((__a__)->__f__);
- void* __r__ = (void *) model_read_action((void *)__p__, __x__);
+ void* __r__ = (void *) model_rmwr_action((void *)__p__, __x__);
model_rmw_action((void *)__p__, __x__, (uint64_t) ((char*)(*__p__) + __m__));
return __r__; }
( volatile atomic_address* __a__, ptrdiff_t __m__, memory_order __x__ )
{
void* volatile* __p__ = &((__a__)->__f__);
- void* __r__ = (void *) model_read_action((void *)__p__, __x__);
+ void* __r__ = (void *) model_rmwr_action((void *)__p__, __x__);
model_rmw_action((void *)__p__, __x__, (uint64_t)((char*)(*__p__) - __m__));
return __r__; }
void ModelChecker::check_current_action(void)
{
ModelAction *curr = this->current_action;
- ModelAction *tmp;
- current_action = NULL;
+ bool already_added = false;
+ this->current_action = NULL;
if (!curr) {
DEBUG("trying to push NULL action...\n");
return;
}
- if (curr->is_rmw()) {
- //We have a RMW action
- process_rmw(curr);
- //Force the current thread to continue since the RMW should be atomic
- nextThread = thread_current()->get_id();
- delete curr;
- return;
- }
-
- tmp = node_stack->explore_action(curr);
- if (tmp) {
- /* Discard duplicate ModelAction; use action from NodeStack */
+ if (curr->is_rmwc()||curr->is_rmw()) {
+ ModelAction *tmp=process_rmw(curr);
+ already_added = true;
delete curr;
- curr = tmp;
+ curr=tmp;
} else {
- /*
- * Perform one-time actions when pushing new ModelAction onto
- * NodeStack
- */
- curr->create_cv(get_parent_action(curr->get_tid()));
- /* Build may_read_from set */
- if (curr->is_read())
- build_reads_from_past(curr);
+ ModelAction * tmp = node_stack->explore_action(curr);
+ if (tmp) {
+ /* Discard duplicate ModelAction; use action from NodeStack */
+ /* First restore type and order in case of RMW operation */
+ if (curr->is_rmwr())
+ tmp->copy_typeandorder(curr);
+ delete curr;
+ curr = tmp;
+ } else {
+ /*
+ * Perform one-time actions when pushing new ModelAction onto
+ * NodeStack
+ */
+ curr->create_cv(get_parent_action(curr->get_tid()));
+ /* Build may_read_from set */
+ if (curr->is_read())
+ build_reads_from_past(curr);
+ }
}
/* Assign 'creation' parent */
th->set_creation(curr);
}
- /* Is there a better interface for setting the next thread rather
- than this field/convoluted approach? Perhaps like just returning
- it or something? */
-
- nextThread = get_next_replay_thread();
-
- Node *currnode = curr->get_node();
- Node *parnode = currnode->get_parent();
-
- if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
- if (!next_backtrack || *curr > *next_backtrack)
- next_backtrack = curr;
-
- set_backtracking(curr);
-
/* Assign reads_from values */
Thread *th = get_thread(curr->get_tid());
uint64_t value = VALUE_NONE;
th->set_return_value(value);
- /* Add action to list last. */
- add_action_to_lists(curr);
+ /* Add action to list. */
+ if (!already_added)
+ add_action_to_lists(curr);
+
+ /* Do not split atomic actions. */
+ if (curr->is_rmwr()) {
+ nextThread = thread_current()->get_id();
+ return;
+ }
+
+ /* Is there a better interface for setting the next thread rather
+ than this field/convoluted approach? Perhaps like just returning
+ it or something? */
+
+ nextThread = get_next_replay_thread();
+
+ Node *currnode = curr->get_node();
+ Node *parnode = currnode->get_parent();
+
+ if (!parnode->backtrack_empty()||!currnode->readsfrom_empty())
+ if (!next_backtrack || *curr > *next_backtrack)
+ next_backtrack = curr;
+
+ set_backtracking(curr);
}
/** @returns whether the current trace is feasible. */
return !cyclegraph->checkForCycles();
}
-/** Process a RMW by converting previous read into a RMW. */
-void ModelChecker::process_rmw(ModelAction * act) {
+/** Close out a RMWR by converting previous RMWR into a RMW or READ. */
+ModelAction * ModelChecker::process_rmw(ModelAction * act) {
int tid = id_to_int(act->get_tid());
ModelAction *lastread=get_last_action(tid);
- lastread->upgrade_rmw(act);
- cyclegraph->addRMWEdge(lastread->get_reads_from(),lastread);
+ lastread->process_rmw(act);
+ if (act->is_rmw())
+ cyclegraph->addRMWEdge(lastread, lastread->get_reads_from());
+ return lastread;
}
/**
ModelAction * get_parent_action(thread_id_t tid);
ModelAction * get_last_seq_cst(const void *location);
void build_reads_from_past(ModelAction *curr);
- void process_rmw(ModelAction * curr);
+ ModelAction * process_rmw(ModelAction * curr);
void r_modification_order(ModelAction * curr, const ModelAction *rf);
void w_modification_order(ModelAction * curr);
projects / model-checker.git / commitdiff