/* 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();
stats.num_buggy_executions++;
else if (is_complete_execution())
stats.num_complete++;
- else
+ else {
stats.num_redundant++;
+
+ /**
+ * @todo We can violate this ASSERT() when fairness/sleep sets
+ * conflict to cause an execution to terminate, e.g. with:
+ * Scheduler: [0: disabled][1: disabled][2: sleep][3: current, enabled]
+ */
+ //ASSERT(scheduler->all_threads_sleeping());
+ }
}
/** @brief Print execution stats */
*/
bool ModelChecker::process_read(ModelAction *curr)
{
+ Node *node = curr->get_node();
uint64_t value = VALUE_NONE;
bool updated = false;
while (true) {
- const ModelAction *reads_from = curr->get_node()->get_read_from_past();
- if (reads_from != NULL) {
- mo_graph->startChanges();
-
- value = reads_from->get_value();
+ switch (node->get_read_from_status()) {
+ case READ_FROM_PAST: {
+ const ModelAction *rf = node->get_read_from_past();
+ ASSERT(rf);
- check_recency(curr, reads_from);
- bool r_status = r_modification_order(curr, reads_from);
+ mo_graph->startChanges();
+ value = rf->get_value();
+ check_recency(curr, rf);
+ bool r_status = r_modification_order(curr, rf);
- if (is_infeasible() && (curr->get_node()->increment_read_from_past() || curr->get_node()->increment_future_value())) {
+ if (is_infeasible() && node->increment_read_from()) {
mo_graph->rollbackChanges();
priv->too_many_reads = false;
continue;
}
- read_from(curr, reads_from);
+ read_from(curr, rf);
mo_graph->commitChanges();
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 = curr->get_node()->get_future_value();
+ struct future_value fv = node->get_future_value();
Promise *promise = new Promise(curr, fv);
value = fv.value;
curr->set_read_from_promise(promise);
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;
write_thread = write_thread->get_parent();
struct future_value fv = {
- writer->get_value(),
+ writer->get_write_value(),
writer->get_seq_number() + params.maxfuturedelay,
write_thread->get_id(),
};
bool ModelChecker::process_write(ModelAction *curr)
{
bool updated_mod_order = w_modification_order(curr);
- bool updated_promises = resolve_promises(curr);
+ int promise_idx = get_promise_to_resolve(curr);
+ bool updated_promises = false;
+
+ if (promise_idx >= 0)
+ updated_promises = resolve_promise(curr, promise_idx);
if (promises->size() == 0) {
for (unsigned int i = 0; i < futurevalues->size(); i++) {
*/
bool ModelChecker::read_from(ModelAction *act, const ModelAction *rf)
{
+ ASSERT(rf);
act->set_read_from(rf);
- if (rf != NULL && act->is_acquire()) {
+ if (act->is_acquire()) {
rel_heads_list_t release_heads;
get_release_seq_heads(act, act, &release_heads);
int num_heads = release_heads.size();
{
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);
}
/**
- * Resolve a set of Promises with a current write. The set is provided in the
- * Node corresponding to @a write.
+ * @brief Find the promise, if any to resolve for the current action
+ * @param curr The current ModelAction. Should be a write.
+ * @return The (non-negative) index for the Promise to resolve, if any;
+ * otherwise -1
+ */
+int ModelChecker::get_promise_to_resolve(const ModelAction *curr) const
+{
+ for (unsigned int i = 0; i < promises->size(); i++)
+ if (curr->get_node()->get_promise(i))
+ return i;
+ return -1;
+}
+
+/**
+ * Resolve a Promise with a current write.
* @param write The ModelAction that is fulfilling Promises
- * @return True if promises were resolved; false otherwise
+ * @param promise_idx The index corresponding to the promise
+ * @return True if the Promise was successfully resolved; false otherwise
*/
-bool ModelChecker::resolve_promises(ModelAction *write)
+bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
{
- bool haveResolved = false;
std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
- promise_list_t mustResolve, resolved;
+ promise_list_t mustResolve;
+ Promise *promise = (*promises)[promise_idx];
- 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);
- //Make sure the promise's value matches the write's value
- ASSERT(promise->is_compatible(write));
- mo_graph->resolvePromise(promise, write, &mustResolve);
+ for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
+ ModelAction *read = promise->get_reader(i);
+ 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) && promise->same_value(write));
+ mo_graph->resolvePromise(promise, write, &mustResolve);
- resolved.push_back(promise);
- promises->erase(promises->begin() + promise_index);
- actions_to_check.push_back(read);
+ promises->erase(promises->begin() + promise_idx);
- haveResolved = true;
- } else
- promise_index++;
- }
+ /** @todo simplify the 'mustResolve' stuff */
+ ASSERT(mustResolve.size() <= 1);
+
+ if (!mustResolve.empty() && mustResolve[0] != promise)
+ priv->failed_promise = true;
+ delete promise;
- for (unsigned int i = 0; i < mustResolve.size(); i++) {
- if (std::find(resolved.begin(), resolved.end(), mustResolve[i])
- == resolved.end())
- priv->failed_promise = true;
- }
- for (unsigned int i = 0; i < resolved.size(); i++)
- delete resolved[i];
//Check whether reading these writes has made threads unable to
//resolve promises
mo_check_promises(read, true);
}
- return haveResolved;
+ return true;
}
/**
{
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->same_value(curr))
+ 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->same_location(write))
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();
}
ModelAction **thread_array = (ModelAction **)model_calloc(1, sizeof(ModelAction *) * get_num_threads());
for (action_list_t::iterator it = action_trace->begin(); it != action_trace->end(); it++) {
- ModelAction *action = *it;
- if (action->is_read()) {
- fprintf(file, "N%u [label=\"N%u, T%u\"];\n", action->get_seq_number(), action->get_seq_number(), action->get_tid());
- if (action->get_reads_from() != NULL)
- fprintf(file, "N%u -> N%u[label=\"rf\", color=red];\n", action->get_seq_number(), action->get_reads_from()->get_seq_number());
+ ModelAction *act = *it;
+ if (act->is_read()) {
+ mo_graph->dot_print_node(file, act);
+ if (act->get_reads_from())
+ mo_graph->dot_print_edge(file,
+ act->get_reads_from(),
+ act,
+ "label=\"rf\", color=red, weight=2");
+ else
+ mo_graph->dot_print_edge(file,
+ act->get_reads_from_promise(),
+ act,
+ "label=\"rf\", color=red");
}
- if (thread_array[action->get_tid()] != NULL) {
- fprintf(file, "N%u -> N%u[label=\"sb\", color=blue];\n", thread_array[action->get_tid()]->get_seq_number(), action->get_seq_number());
+ if (thread_array[act->get_tid()]) {
+ mo_graph->dot_print_edge(file,
+ thread_array[id_to_int(act->get_tid())],
+ act,
+ "label=\"sb\", color=blue, weight=400");
}
- thread_array[action->get_tid()] = action;
+ thread_array[act->get_tid()] = act;
}
fprintf(file, "}\n");
model_free(thread_array);
#endif
model_print("Execution %d:", stats.num_total);
- if (isfeasibleprefix())
+ if (isfeasibleprefix()) {
+ if (scheduler->all_threads_sleeping())
+ model_print(" SLEEP-SET REDUNDANT");
model_print("\n");
- else
+ } else
print_infeasibility(" INFEASIBLE");
print_list(action_trace);
model_print("\n");
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 / c11tester.git / blobdiff