From: Brian Norris <banorris@uci.edu>
Date: Wed, 27 Feb 2013 23:13:17 +0000 (-0800)
Subject: promise: record multiple readers in the same Promise
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=8c9713418515a44e0a96cadabca0feececf962b3;p=cdsspec-compiler.git
promise: record multiple readers in the same Promise
This requires more adjustments throughout ModelChecker.
---
diff --git a/cyclegraph.cc b/cyclegraph.cc
index 1dbb12d..67552e0 100644
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -320,7 +320,7 @@ static void print_node(const CycleNode *node, FILE *file, int label)
modelclock_t idx;
if (node->is_promise()) {
const Promise *promise = node->getPromise();
- idx = promise->get_action()->get_seq_number();
+ idx = promise->get_reader(0)->get_seq_number();
fprintf(file, "P%u", idx);
if (label) {
int first = 1;
diff --git a/model.cc b/model.cc
index 44fba7e..38d63a2 100644
--- a/model.cc
+++ b/model.cc
@@ -873,6 +873,7 @@ bool ModelChecker::process_read(ModelAction *curr)
}
case READ_FROM_PROMISE: {
Promise *promise = curr->get_node()->get_read_from_promise();
+ promise->add_reader(curr);
value = promise->get_value();
curr->set_read_from_promise(promise);
mo_graph->startChanges();
@@ -1348,14 +1349,19 @@ void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiti
{
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
- ModelAction *reader = promise->get_action();
- if (reader->get_tid() != blocker->get_id())
- continue;
if (!promise->thread_is_available(waiting->get_id()))
continue;
- if (promise->eliminate_thread(waiting->get_id())) {
- /* Promise has failed */
- priv->failed_promise = true;
+ for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+ ModelAction *reader = promise->get_reader(j);
+ if (reader->get_tid() != blocker->get_id())
+ continue;
+ if (promise->eliminate_thread(waiting->get_id())) {
+ /* Promise has failed */
+ priv->failed_promise = true;
+ } else {
+ /* Only eliminate the 'waiting' thread once */
+ return;
+ }
}
}
}
@@ -2451,15 +2457,17 @@ bool ModelChecker::resolve_promises(ModelAction *write)
for (unsigned int i = 0, promise_index = 0; promise_index < promises->size(); i++) {
Promise *promise = (*promises)[promise_index];
if (write->get_node()->get_promise(i)) {
- ModelAction *read = promise->get_action();
- read_from(read, write);
+ for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+ ModelAction *read = promise->get_reader(j);
+ read_from(read, write);
+ actions_to_check.push_back(read);
+ }
//Make sure the promise's value matches the write's value
ASSERT(promise->is_compatible(write));
mo_graph->resolvePromise(promise, write, &mustResolve);
resolved.push_back(promise);
promises->erase(promises->begin() + promise_index);
- actions_to_check.push_back(read);
haveResolved = true;
} else
@@ -2494,14 +2502,20 @@ void ModelChecker::compute_promises(ModelAction *curr)
{
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
- const ModelAction *act = promise->get_action();
- ASSERT(act->is_read());
- if (!act->happens_before(curr) &&
- !act->could_synchronize_with(curr) &&
- promise->is_compatible(curr) &&
- promise->get_value() == curr->get_value()) {
- curr->get_node()->set_promise(i);
+ if (!promise->is_compatible(curr) || promise->get_value() != curr->get_value())
+ continue;
+
+ bool satisfy = true;
+ for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+ const ModelAction *act = promise->get_reader(j);
+ if (act->happens_before(curr) ||
+ act->could_synchronize_with(curr)) {
+ satisfy = false;
+ break;
+ }
}
+ if (satisfy)
+ curr->get_node()->set_promise(i);
}
}
@@ -2510,13 +2524,17 @@ void ModelChecker::check_promises(thread_id_t tid, ClockVector *old_cv, ClockVec
{
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
- const ModelAction *act = promise->get_action();
- if ((old_cv == NULL || !old_cv->synchronized_since(act)) &&
- merge_cv->synchronized_since(act)) {
- if (promise->eliminate_thread(tid)) {
- //Promise has failed
- priv->failed_promise = true;
- return;
+ if (!promise->thread_is_available(tid))
+ continue;
+ for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+ const ModelAction *act = promise->get_reader(j);
+ if ((!old_cv || !old_cv->synchronized_since(act)) &&
+ merge_cv->synchronized_since(act)) {
+ if (promise->eliminate_thread(tid)) {
+ /* Promise has failed */
+ priv->failed_promise = true;
+ return;
+ }
}
}
}
@@ -2553,15 +2571,20 @@ void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
- const ModelAction *pread = promise->get_action();
// Is this promise on the same location?
- if (!pread->same_var(write))
+ if (promise->get_value() != write->get_value())
continue;
- if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
- priv->failed_promise = true;
- return;
+ for (unsigned int j = 0; j < promise->get_num_readers(); j++) {
+ const ModelAction *pread = promise->get_reader(j);
+ if (!pread->happens_before(act))
+ continue;
+ if (mo_graph->checkPromise(write, promise)) {
+ priv->failed_promise = true;
+ return;
+ }
+ break;
}
// Don't do any lookups twice for the same thread
@@ -2656,7 +2679,7 @@ void ModelChecker::build_may_read_from(ModelAction *curr)
/* Inherit existing, promised future values */
for (i = 0; i < promises->size(); i++) {
const Promise *promise = (*promises)[i];
- const ModelAction *promise_read = promise->get_action();
+ const ModelAction *promise_read = promise->get_reader(0);
if (promise_read->same_var(curr)) {
/* Only add feasible future-values */
mo_graph->startChanges();
diff --git a/promise.cc b/promise.cc
index 86c3c58..23b92cd 100644
--- a/promise.cc
+++ b/promise.cc
@@ -15,13 +15,38 @@
Promise::Promise(ModelAction *read, struct future_value fv) :
num_available_threads(0),
fv(fv),
- read(read),
+ readers(1, read),
write(NULL)
{
add_thread(fv.tid);
eliminate_thread(read->get_tid());
}
+/**
+ * Add a reader that reads from this Promise. Must be added in an order
+ * consistent with execution order.
+ *
+ * @param reader The ModelAction that reads from this promise. Must be a read.
+ * @return True if this new reader has invalidated the promise; false otherwise
+ */
+bool Promise::add_reader(ModelAction *reader)
+{
+ readers.push_back(reader);
+ return eliminate_thread(reader->get_tid());
+}
+
+/**
+ * Access a reader that read from this Promise. Readers must be inserted in
+ * order by execution order, so they can be returned in this order.
+ *
+ * @param i The index of the reader to return
+ * @return The i'th reader of this Promise
+ */
+ModelAction * Promise::get_reader(unsigned int i) const
+{
+ return i < readers.size() ? readers[i] : NULL;
+}
+
/**
* Eliminate a thread which no longer can satisfy this promise. Once all
* enabled threads have been eliminated, this promise is unresolvable.
@@ -76,7 +101,7 @@ bool Promise::thread_is_available(thread_id_t tid) const
/** @brief Print debug info about the Promise */
void Promise::print() const
{
- model_print("Promised value %#" PRIx64 ", read from thread %d, available threads to resolve: ", fv.value, id_to_int(read->get_tid()));
+ model_print("Promised value %#" PRIx64 ", first read from thread %d, available threads to resolve: ", fv.value, id_to_int(get_reader(0)->get_tid()));
for (unsigned int i = 0; i < available_thread.size(); i++)
if (available_thread[i])
model_print("[%d]", i);
@@ -102,7 +127,7 @@ bool Promise::has_failed() const
*/
bool Promise::is_compatible(const ModelAction *act) const
{
- return thread_is_available(act->get_tid()) && read->same_var(act);
+ return thread_is_available(act->get_tid()) && get_reader(0)->same_var(act);
}
/**
diff --git a/promise.h b/promise.h
index c131d74..5ea7dc5 100644
--- a/promise.h
+++ b/promise.h
@@ -24,7 +24,9 @@ struct future_value {
class Promise {
public:
Promise(ModelAction *read, struct future_value fv);
- ModelAction * get_action() const { return read; }
+ bool add_reader(ModelAction *reader);
+ ModelAction * get_reader(unsigned int i) const;
+ unsigned int get_num_readers() const { return readers.size(); }
bool eliminate_thread(thread_id_t tid);
void add_thread(thread_id_t tid);
bool thread_is_available(thread_id_t tid) const;
@@ -54,8 +56,8 @@ class Promise {
const future_value fv;
- /** @brief The action which reads a promised value */
- ModelAction * const read;
+ /** @brief The action(s) which read the promised future value */
+ std::vector< ModelAction *, SnapshotAlloc<ModelAction *> > readers;
const ModelAction *write;
};