From: Brian Demsky Date: Fri, 20 Jul 2012 19:32:42 +0000 (-0700) Subject: towards making rmw work... X-Git-Url: http://plrg.eecs.uci.edu/git/?p=c11tester.git;a=commitdiff_plain;h=247e28f81f258c3c380be00a89430186f8ac11ed towards making rmw work... [Split by Brian Norris] --- diff --git a/action.cc b/action.cc index 74ba5aab..1fb3b769 100644 --- a/action.cc +++ b/action.cc @@ -95,13 +95,19 @@ bool ModelAction::same_thread(const ModelAction *act) const 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: @@ -206,7 +212,7 @@ void ModelAction::print(void) const 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); diff --git a/action.h b/action.h index 5ab36b36..8d06aa49 100644 --- a/action.h +++ b/action.h @@ -91,7 +91,8 @@ public: 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: diff --git a/cmodelint.cc b/cmodelint.cc index 20f257c3..4754a826 100644 --- a/cmodelint.cc +++ b/cmodelint.cc @@ -14,6 +14,15 @@ void model_init_action(void * obj, uint64_t val) { 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)); +} diff --git a/cmodelint.h b/cmodelint.h index 0f653279..5e762f80 100644 --- a/cmodelint.h +++ b/cmodelint.h @@ -9,8 +9,11 @@ extern "C" { 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 } diff --git a/cyclegraph.cc b/cyclegraph.cc index 6676f2f0..c0e8e2af 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -20,35 +20,53 @@ CycleNode * CycleGraph::getNode(const ModelAction * action) { } /** 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 * edges=fromnode->getEdges(); - for(unsigned int i=0;edges->size();i++) { + for(unsigned int i=0;isize();i++) { CycleNode * tonode=(*edges)[i]; rmwnode->addEdge(tonode); } - if (!hasCycles) { - hasCycles=checkReachable(rmwnode, fromnode); - } + fromnode->addEdge(rmwnode); } @@ -85,6 +103,7 @@ bool CycleGraph::checkForCycles() { /** Constructor for a CycleNode. */ CycleNode::CycleNode(const ModelAction *modelaction) { action=modelaction; + hasRMW=NULL; } /** Returns a vector of the edges from a CycleNode. */ @@ -97,8 +116,12 @@ void CycleNode::addEdge(CycleNode * node) { 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); } diff --git a/cyclegraph.h b/cyclegraph.h index 69017002..3ed4e4a2 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -29,12 +29,13 @@ class CycleNode { CycleNode(const ModelAction *action); void addEdge(CycleNode * node); std::vector * getEdges(); - bool setRMW(); + bool setRMW(CycleNode *); + CycleNode* getRMW(); private: const ModelAction *action; std::vector edges; - bool hasRMW; + CycleNode * hasRMW; }; #endif diff --git a/impatomic.cc b/impatomic.cc index 8642bee2..df11202d 100644 --- a/impatomic.cc +++ b/impatomic.cc @@ -6,7 +6,7 @@ namespace std { 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; diff --git a/include/impatomic.h b/include/impatomic.h index 4d842d6f..808dc122 100644 --- a/include/impatomic.h +++ b/include/impatomic.h @@ -92,7 +92,7 @@ inline void atomic_flag::fence( memory_order __x__ ) const volatile #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__; \ @@ -104,10 +104,10 @@ inline void atomic_flag::fence( memory_order __x__ ) const volatile __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 @@ -2121,7 +2121,7 @@ inline void* atomic_fetch_add_explicit ( 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__; } @@ -2134,7 +2134,7 @@ inline void* atomic_fetch_sub_explicit ( 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__; } diff --git a/model.cc b/model.cc index 726901b2..59f148ef 100644 --- a/model.cc +++ b/model.cc @@ -250,36 +250,37 @@ ModelAction * ModelChecker::get_next_backtrack() 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 */ @@ -288,21 +289,6 @@ void ModelChecker::check_current_action(void) 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; @@ -318,8 +304,30 @@ void ModelChecker::check_current_action(void) 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. */ @@ -327,12 +335,14 @@ bool ModelChecker::isfeasible() { 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; } /** diff --git a/model.h b/model.h index 76ded6c1..8593b98f 100644 --- a/model.h +++ b/model.h @@ -82,7 +82,7 @@ private: 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);