From a0562e0739fd643fdb2108f784f4722482ea5a4f Mon Sep 17 00:00:00 2001 From: Brian Demsky Date: Wed, 12 Sep 2012 16:24:07 -0700 Subject: [PATCH] (1) structure code a little better (2) add startChanges to cyclegraph... This is just to check some assertions that rollback is being used correctly and doesn't rollback unintended changes --- cyclegraph.cc | 6 ++++++ cyclegraph.h | 1 + model.cc | 28 ++++++++++++++++++---------- model.h | 2 ++ 4 files changed, 27 insertions(+), 10 deletions(-) diff --git a/cyclegraph.cc b/cyclegraph.cc index 9256deb..f519dac 100644 --- a/cyclegraph.cc +++ b/cyclegraph.cc @@ -140,6 +140,12 @@ bool CycleGraph::checkReachable(CycleNode *from, CycleNode *to) { 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); diff --git a/cyclegraph.h b/cyclegraph.h index 0bb01c4..8a9bf7c 100644 --- a/cyclegraph.h +++ b/cyclegraph.h @@ -22,6 +22,7 @@ class CycleGraph { void addRMWEdge(const ModelAction *from, const ModelAction *rmw); bool checkReachable(const ModelAction *from, const ModelAction *to); + void startChanges(); void commitChanges(); void rollbackChanges(); diff --git a/model.cc b/model.cc index 9611f2f..cc464a2 100644 --- a/model.cc +++ b/model.cc @@ -272,6 +272,8 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part 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); @@ -412,23 +414,28 @@ Thread * ModelChecker::check_current_action(ModelAction *curr) 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]; @@ -529,6 +536,7 @@ void ModelChecker::check_recency(ModelAction *curr, bool already_added) { 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(); diff --git a/model.h b/model.h index 1a2f6a1..bcb9d61 100644 --- a/model.h +++ b/model.h @@ -116,6 +116,8 @@ private: 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); -- 2.34.1