/* 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()) {
+ } else if (nextnode->increment_read_from_past()) {
/* The next node will read from a different value. */
tid = next->get_tid();
node_stack->pop_restofstack(2);
earliest_diverge = prevnode->get_action();
}
}
+ /* Start the round robin scheduler from this thread id */
+ scheduler->set_scheduler_thread(tid);
/* The correct sleep set is in the parent node. */
execute_sleep_set();
}
}
+/**
+ * @brief Should the current action wake up a given thread?
+ *
+ * @param curr The current action
+ * @param thread The thread that we might wake up
+ * @return True, if we should wake up the sleeping thread; false otherwise
+ */
+bool ModelChecker::should_wake_up(const ModelAction *curr, const Thread *thread) const
+{
+ const ModelAction *asleep = thread->get_pending();
+ /* Don't allow partial RMW to wake anyone up */
+ if (curr->is_rmwr())
+ return false;
+ /* Synchronizing actions may have been backtracked */
+ if (asleep->could_synchronize_with(curr))
+ return true;
+ /* All acquire/release fences and fence-acquire/store-release */
+ if (asleep->is_fence() && asleep->is_acquire() && curr->is_release())
+ return true;
+ /* Fence-release + store can awake load-acquire on the same location */
+ if (asleep->is_read() && asleep->is_acquire() && curr->same_var(asleep) && curr->is_write()) {
+ ModelAction *fence_release = get_last_fence_release(curr->get_tid());
+ if (fence_release && *(get_last_action(thread->get_id())) < *fence_release)
+ return true;
+ }
+ return false;
+}
+
void ModelChecker::wake_up_sleeping_actions(ModelAction *curr)
{
for (unsigned int i = 0; i < get_num_threads(); i++) {
Thread *thr = get_thread(int_to_id(i));
if (scheduler->is_sleep_set(thr)) {
- ModelAction *pending_act = thr->get_pending();
- if ((!curr->is_rmwr()) && pending_act->could_synchronize_with(curr))
- //Remove this thread from sleep set
+ if (should_wake_up(curr, thr))
+ /* Remove this thread from sleep set */
scheduler->remove_sleep(thr);
}
}
}
/**
- * Processes a read or rmw model action.
+ * Processes a read model action.
* @param curr is the read model action to process.
- * @param second_part_of_rmw is boolean that is true is this is the second action of a rmw.
* @return True if processing this read updates the mo_graph.
*/
-bool ModelChecker::process_read(ModelAction *curr, bool second_part_of_rmw)
+bool ModelChecker::process_read(ModelAction *curr)
{
uint64_t value = VALUE_NONE;
bool updated = false;
while (true) {
- const ModelAction *reads_from = curr->get_node()->get_read_from();
- if (reads_from != NULL) {
+ const ModelAction *rf = curr->get_node()->get_read_from_past();
+ if (rf != NULL) {
mo_graph->startChanges();
- value = reads_from->get_value();
- bool r_status = false;
+ value = rf->get_value();
- if (!second_part_of_rmw) {
- check_recency(curr, reads_from);
- r_status = r_modification_order(curr, reads_from);
- }
+ check_recency(curr, rf);
+ bool r_status = r_modification_order(curr, rf);
- if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
+ if (is_infeasible() && (curr->get_node()->increment_read_from_past() || curr->get_node()->increment_future_value())) {
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 if (!second_part_of_rmw) {
+ } else {
/* Read from future value */
struct future_value fv = curr->get_node()->get_future_value();
Promise *promise = new Promise(curr, fv);
case THREAD_CREATE: {
thrd_t *thrd = (thrd_t *)curr->get_location();
struct thread_params *params = (struct thread_params *)curr->get_value();
- Thread *th = new Thread(thrd, params->func, params->arg);
+ Thread *th = new Thread(thrd, params->func, params->arg, get_thread(curr));
add_thread(th);
th->set_creation(curr);
/* Promises can be satisfied by children */
return false;
}
+/**
+ * Check promises and eliminate potentially-satisfying threads when a thread is
+ * blocked (e.g., join, lock). A thread which is waiting on another thread can
+ * no longer satisfy a promise generated from that thread.
+ *
+ * @param blocker The thread on which a thread is waiting
+ * @param waiting The waiting thread
+ */
+void ModelChecker::thread_blocking_check_promises(Thread *blocker, Thread *waiting)
+{
+ 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;
+ }
+ }
+}
+
/**
* @brief Check whether a model action is enabled.
*
Thread *blocking = (Thread *)curr->get_location();
if (!blocking->is_complete()) {
blocking->push_wait_list(curr);
+ thread_blocking_check_promises(blocking, get_thread(curr));
return false;
}
}
/* Build may_read_from set for newly-created actions */
if (newly_explored && curr->is_read())
- build_reads_from_past(curr);
+ build_may_read_from(curr);
/* Initialize work_queue with the "current action" work */
work_queue_t work_queue(1, CheckCurrWorkEntry(curr));
if (process_thread_action(curr))
update_all = true;
- if (act->is_read() && process_read(act, second_part_of_rmw))
+ if (act->is_read() && !second_part_of_rmw && process_read(act))
update = true;
if (act->is_write() && process_write(act))
if ((parnode && !parnode->backtrack_empty()) ||
!currnode->misc_empty() ||
- !currnode->read_from_empty() ||
+ !currnode->read_from_past_empty() ||
!currnode->future_value_empty() ||
!currnode->promise_empty() ||
!currnode->relseq_break_empty()) {
void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
{
if (params.maxreads != 0) {
- if (curr->get_node()->get_read_from_size() <= 1)
+ if (curr->get_node()->get_read_from_past_size() <= 1)
return;
//Must make sure that execution is currently feasible... We could
//accidentally clear by rolling back
if (act->get_reads_from() != rf)
return;
- if (act->get_node()->get_read_from_size() <= 1)
+ if (act->get_node()->get_read_from_past_size() <= 1)
return;
}
- for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
+ for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
/* Get write */
- const ModelAction *write = curr->get_node()->get_read_from_at(i);
+ const ModelAction *write = curr->get_node()->get_read_from_past(i);
/* Need a different write */
if (write == rf)
for (int loop = count; loop > 0; loop--, rit++) {
ModelAction *act = *rit;
bool foundvalue = false;
- for (int j = 0; j < act->get_node()->get_read_from_size(); j++) {
- if (act->get_node()->get_read_from_at(j) == write) {
+ for (int j = 0; j < act->get_node()->get_read_from_past_size(); j++) {
+ if (act->get_node()->get_read_from_past(j) == write) {
foundvalue = true;
break;
}
added = mo_graph->addEdge(act, rf) || added;
}
} else {
- const ModelAction *prevreadfrom = act->get_reads_from();
- //if the previous read is unresolved, keep going...
- if (prevreadfrom == NULL)
- continue;
-
- if (!prevreadfrom->equals(rf)) {
- added = mo_graph->addEdge(prevreadfrom, rf) || added;
+ const ModelAction *prevrf = act->get_reads_from();
+ const Promise *prevrf_promise = act->get_reads_from_promise();
+ if (prevrf) {
+ if (!prevrf->equals(rf))
+ added = mo_graph->addEdge(prevrf, rf) || added;
+ } else if (!prevrf_promise->equals(rf)) {
+ added = mo_graph->addEdge(prevrf_promise, rf) || added;
}
}
break;
read_from(read, write);
//Make sure the promise's value matches the write's value
ASSERT(promise->is_compatible(write));
- mo_graph->resolvePromise(read, write, &mustResolve);
+ mo_graph->resolvePromise(promise, write, &mustResolve);
resolved.push_back(promise);
promises->erase(promises->begin() + promise_index);
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->is_read() &&
!act->could_synchronize_with(curr) &&
- !act->same_thread(curr) &&
- act->get_location() == curr->get_location() &&
+ promise->is_compatible(curr) &&
promise->get_value() == curr->get_value()) {
curr->get_node()->set_promise(i, act->is_rmw());
}
/**
* Build up an initial set of all past writes that this 'read' action may read
- * from. This set is determined by the clock vector's "happens before"
- * relationship.
+ * from, as well as any previously-observed future values that must still be valid.
+ *
* @param curr is the current ModelAction that we are exploring; it must be a
* 'read' operation.
*/
-void ModelChecker::build_reads_from_past(ModelAction *curr)
+void ModelChecker::build_may_read_from(ModelAction *curr)
{
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
mo_graph->startChanges();
r_modification_order(curr, act);
if (!is_infeasible())
- curr->get_node()->add_read_from(act);
+ curr->get_node()->add_read_from_past(act);
mo_graph->rollbackChanges();
}
break;
}
}
+
+ /* Inherit existing, promised future values */
+ for (i = 0; i < promises->size(); i++) {
+ const Promise *promise = (*promises)[i];
+ const ModelAction *promise_read = promise->get_action();
+ 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);
+ }
+ mo_graph->rollbackChanges();
+ }
+ }
+
/* We may find no valid may-read-from only if the execution is doomed */
- if (!curr->get_node()->get_read_from_size()) {
+ if (!curr->get_node()->get_read_from_past_size() && curr->get_node()->future_value_empty()) {
priv->no_valid_reads = true;
set_assert();
}
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
curr->print();
- model_print("Printing may_read_from\n");
- curr->get_node()->print_may_read_from();
- model_print("End printing may_read_from\n");
+ model_print("Printing read_from_past\n");
+ curr->get_node()->print_read_from_past();
+ model_print("End printing read_from_past\n");
}
}
{
do {
thrd_t user_thread;
- Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL);
+ Thread *t = new Thread(&user_thread, &user_main_wrapper, NULL, NULL);
add_thread(t);
do {
projects / c11tester.git / blobdiff