return false;
}
+void CycleGraph::startChanges() {
+ ASSERT(rollbackvector.size()==0);
+ ASSERT(rmwrollbackvector.size()==0);
+ ASSERT(oldCycles==hasCycles);
+}
+
/** Commit changes to the cyclegraph. */
void CycleGraph::commitChanges() {
rollbackvector.resize(0);
while(true) {
const ModelAction *reads_from = curr->get_node()->get_read_from();
if (reads_from != NULL) {
+ mo_graph->startChanges();
+
value = reads_from->get_value();
/* Assign reads_from, perform release/acquire synchronization */
curr->read_from(reads_from);
if (!second_part_of_rmw)
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() ||
- !currnode->promise_empty())
- && (!priv->next_backtrack ||
- *curr > *priv->next_backtrack)) {
+ !currnode->read_from_empty() ||
+ !currnode->future_value_empty() ||
+ !currnode->promise_empty())
+ && (!priv->next_backtrack ||
+ *curr > *priv->next_backtrack)) {
priv->next_backtrack = curr;
}
-
- set_backtracking(curr);
-
- return get_next_thread(curr);
}
+
bool ModelChecker::promises_expired() {
for (unsigned int promise_index = 0; promise_index < promises->size(); promise_index++) {
Promise *promise = (*promises)[promise_index];
continue;
/* Test to see whether this is a feasible write to read from*/
+ mo_graph->startChanges();
r_modification_order(curr, write);
bool feasiblereadfrom=isfeasible();
mo_graph->rollbackChanges();
bool resolve_promises(ModelAction *curr);
void compute_promises(ModelAction *curr);
+
+ void check_curr_backtracking(ModelAction * curr);
void add_action_to_lists(ModelAction *act);
ModelAction * get_last_action(thread_id_t tid);
ModelAction * get_last_seq_cst(const void *location);