//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 tonode is also a rmw, don't do this check as the execution is
+ //doomed and we'll catch the problem elsewhere, but we want to allow
+ //for the possibility of sending to's write value to rmwnode
+
+ if (rmwnode!=NULL&&!to->is_rmw()) {
if (!hasCycles) {
// Check for Cycles
hasCycles=checkReachable(tonode, rmwnode);
}
/* Transfer all outgoing edges from the from node to the rmw node */
- /* This process should not add a cycle because either:
+ /* This process should not add a cycle because either:
* (1) The rmw should not have any incoming edges yet if it is the
* new node or
- * (2) the fromnode is the new node and therefore it should not
+ * (2) the fromnode is the new node and therefore it should not
* have any outgoing edges.
*/
std::vector<CycleNode *> * edges=fromnode->getEdges();
for(unsigned int i=0;i<edges->size();i++) {
CycleNode * tonode=(*edges)[i];
- rollbackvector.push_back(rmwnode);
- rmwnode->addEdge(tonode);
+ if (tonode!=rmwnode) {
+ rollbackvector.push_back(rmwnode);
+ rmwnode->addEdge(tonode);
+ }
}
rollbackvector.push_back(fromnode);
return next;
}
-
/**
* Processes a read or rmw model action.
* @param curr is the read model action to process.
* @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
* @return True if processing this read updates the mo_graph.
*/
-
bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part_of_rmw) {
uint64_t value;
bool updated=false;
mo_graph->startChanges();
value = reads_from->get_value();
+ bool r_status=false;
if (!second_part_of_rmw) {
check_recency(curr,false);
+ r_status=r_modification_order(curr, reads_from);
}
- bool r_status=r_modification_order(curr,reads_from);
- if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||!curr->get_node()->future_value_empty())) {
+ if (!second_part_of_rmw&&!isfeasible()&&(curr->get_node()->increment_read_from()||curr->get_node()->increment_future_value())) {
mo_graph->rollbackChanges();
too_many_reads=false;
continue;
add_action_to_lists(curr);
check_curr_backtracking(curr);
-
+
set_backtracking(curr);
return get_next_thread(curr);
void ModelChecker::check_curr_backtracking(ModelAction * curr) {
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
-
+
if ((!parnode->backtrack_empty() ||
!currnode->read_from_empty() ||
!currnode->future_value_empty() ||
}
}
-
bool ModelChecker::promises_expired() {
for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
Promise *promise = (*promises)[promise_index];
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr)) {
- if (act->is_read()) {
+ if (act->is_write()) {
+ if (rf != act && act != curr) {
+ mo_graph->addEdge(act, rf);
+ added = true;
+ }
+ } else {
const ModelAction *prevreadfrom = act->get_reads_from();
if (prevreadfrom != NULL && rf != prevreadfrom) {
mo_graph->addEdge(prevreadfrom, rf);
added = true;
}
- } else if (rf != act) {
- mo_graph->addEdge(act, rf);
- added = true;
- }
+ }
+
break;
}
}
return true;
}
-
/**
* Finds the head(s) of the release sequence(s) containing a given ModelAction.
* The ModelAction under consideration is expected to be taking part in
return resolved;
}
-
-
/**
* Compute the set of promises that could potentially be satisfied by this
* action. Note that the set computation actually appears in the Node, not in