/* The next node will try to satisfy a different set of promises. */
tid = next->get_tid();
node_stack->pop_restofstack(2);
- } else if (nextnode->increment_read_from_past()) {
+ } else if (nextnode->increment_read_from()) {
/* The next node will read from a different value. */
tid = next->get_tid();
node_stack->pop_restofstack(2);
- } else if (nextnode->increment_future_value()) {
- /* The next node will try to read from a different future value. */
- tid = next->get_tid();
- node_stack->pop_restofstack(2);
} else if (nextnode->increment_relseq_break()) {
/* The next node will try to resolve a release sequence differently */
tid = next->get_tid();
uint64_t value = VALUE_NONE;
bool updated = false;
while (true) {
- const ModelAction *rf = node->get_read_from_past();
- if (rf != NULL) {
- mo_graph->startChanges();
+ switch (node->get_read_from_status()) {
+ case READ_FROM_PAST: {
+ const ModelAction *rf = node->get_read_from_past();
+ ASSERT(rf);
+ mo_graph->startChanges();
value = rf->get_value();
-
check_recency(curr, rf);
bool r_status = r_modification_order(curr, rf);
- if (is_infeasible() && (node->increment_read_from_past() || node->increment_future_value())) {
+ if (is_infeasible() && node->increment_read_from()) {
mo_graph->rollbackChanges();
priv->too_many_reads = false;
continue;
mo_check_promises(curr, true);
updated |= r_status;
- } else {
+ break;
+ }
+ 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();
+ updated = r_modification_order(curr, promise);
+ mo_graph->commitChanges();
+ break;
+ }
+ case READ_FROM_FUTURE: {
/* Read from future value */
struct future_value fv = node->get_future_value();
Promise *promise = new Promise(curr, fv);
mo_graph->startChanges();
updated = r_modification_order(curr, promise);
mo_graph->commitChanges();
+ break;
+ }
+ default:
+ ASSERT(false);
}
get_thread(curr)->set_return_value(value);
return updated;
{
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;
+ }
}
}
}
if ((parnode && !parnode->backtrack_empty()) ||
!currnode->misc_empty() ||
- !currnode->read_from_past_empty() ||
- !currnode->future_value_empty() ||
+ !currnode->read_from_empty() ||
!currnode->promise_empty() ||
!currnode->relseq_break_empty()) {
set_latest_backtrack(curr);
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
{
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, act->is_rmw());
+ 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);
}
}
{
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;
+ }
}
}
}
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
/* 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();
r_modification_order(curr, promise);
- if (!is_infeasible()) {
- const struct future_value fv = promise->get_fv();
- curr->get_node()->add_future_value(fv);
- }
+ if (!is_infeasible())
+ curr->get_node()->add_read_from_promise(promise_read);
mo_graph->rollbackChanges();
}
}
/* We may find no valid may-read-from only if the execution is doomed */
- if (!curr->get_node()->get_read_from_past_size() && curr->get_node()->future_value_empty()) {
+ if (!curr->get_node()->read_from_size()) {
priv->no_valid_reads = true;
set_assert();
}
return get_thread(act->get_tid());
}
+/**
+ * @brief Get a Promise's "promise number"
+ *
+ * A "promise number" is an index number that is unique to a promise, valid
+ * only for a specific snapshot of an execution trace. Promises may come and go
+ * as they are generated an resolved, so an index only retains meaning for the
+ * current snapshot.
+ *
+ * @param promise The Promise to check
+ * @return The promise index, if the promise still is valid; otherwise -1
+ */
+int ModelChecker::get_promise_number(const Promise *promise) const
+{
+ for (unsigned int i = 0; i < promises->size(); i++)
+ if ((*promises)[i] == promise)
+ return i;
+ /* Not found */
+ return -1;
+}
+
/**
* @brief Check if a Thread is currently enabled
* @param t The Thread to check
projects / model-checker.git / blobdiff