From a1b119052d16810d6289855635c2b0e66a6b93b8 Mon Sep 17 00:00:00 2001
From: Brian Demsky <bdemsky@uci.edu>
Date: Wed, 12 Sep 2012 21:03:37 -0700
Subject: [PATCH] another bug fix...
---
model.cc | 41 ++++++++++++++++++++++++++++++++++++-----
model.h | 4 ++++
2 files changed, 40 insertions(+), 5 deletions(-)
diff --git a/model.cc b/model.cc
index bd4ade2..c3a8c84 100644
--- a/model.cc
+++ b/model.cc
@@ -34,7 +34,8 @@ ModelChecker::ModelChecker(struct model_params params) :
mo_graph(new CycleGraph()),
failed_promise(false),
too_many_reads(false),
- asserted(false)
+ asserted(false),
+ rmw_cycle(false)
{
/* Allocate this "size" on the snapshotting heap */
priv = (struct model_snapshot_members *)calloc(1, sizeof(*priv));
@@ -77,6 +78,7 @@ void ModelChecker::reset_to_initial_state()
node_stack->reset_execution();
failed_promise = false;
too_many_reads = false;
+ rmw_cycle=false;
reset_asserted();
snapshotObject->backTrackBeforeStep(0);
}
@@ -258,6 +260,30 @@ ModelAction * ModelChecker::get_next_backtrack()
return next;
}
+
+/** Checks whether making the ModelAction read read_from the
+ ModelAction write will introduce a cycle in the reads_from
+ relation.
+
+@return true if making it read from will be fine, false otherwise.
+
+*/
+
+bool ModelChecker::ensure_rmw_acyclic(const ModelAction * read, const ModelAction *write) {
+ if (!read->is_rmw())
+ return true;
+ if (!write->is_rmw())
+ return true;
+ while(write!=NULL) {
+ if (write==read) {
+ rmw_cycle=true;
+ return false;
+ }
+ write=write->get_reads_from();
+ }
+ return true;
+}
+
/**
* Processes a read or rmw model action.
* @param curr is the read model action to process.
@@ -276,7 +302,8 @@ bool ModelChecker::process_read(ModelAction *curr, Thread * th, bool second_part
value = reads_from->get_value();
/* Assign reads_from, perform release/acquire synchronization */
- curr->read_from(reads_from);
+ if (ensure_rmw_acyclic(curr, reads_from))
+ curr->read_from(reads_from);
if (!second_part_of_rmw) {
check_recency(curr,false);
}
@@ -457,9 +484,10 @@ bool ModelChecker::isfeasible() {
return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
}
-/** @returns whether the current partial trace is feasible. */
+/** @returns whether the current partial trace is feasible other than
+ * multiple RMW reading from the same store. */
bool ModelChecker::isfeasibleotherthanRMW() {
- return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !promises_expired();
+ return !mo_graph->checkForCycles() && !failed_promise && !too_many_reads && !rmw_cycle && !promises_expired();
}
/** Returns whether the current completed trace is feasible. */
@@ -1026,7 +1054,8 @@ bool ModelChecker::resolve_promises(ModelAction *write)
Promise *promise = (*promises)[promise_index];
if (write->get_node()->get_promise(i)) {
ModelAction *read = promise->get_action();
- read->read_from(write);
+ if (ensure_rmw_acyclic(read, write))
+ read->read_from(write);
if (read->is_rmw()) {
mo_graph->addRMWEdge(write, read);
}
@@ -1040,6 +1069,8 @@ bool ModelChecker::resolve_promises(ModelAction *write)
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
diff --git a/model.h b/model.h
index fec8d1f..d47fe96 100644
--- a/model.h
+++ b/model.h
@@ -89,6 +89,9 @@ private:
/** The scheduler to use: tracks the running/ready Threads */
Scheduler *scheduler;
+ bool ensure_rmw_acyclic(const ModelAction * read, const ModelAction *write);
+
+
bool thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader);
bool has_asserted() {return asserted;}
void reset_asserted() {asserted=false;}
@@ -186,6 +189,7 @@ private:
bool failed_promise;
bool too_many_reads;
bool asserted;
+ bool rmw_cycle;
};
extern ModelChecker *model;
--
2.34.1