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;
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];
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