}
}
+/**
+ * @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);
}
}
if (!last_release)
return NULL;
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
- std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
- bool found_acquire_fences = false;
+ /* Skip past the release */
+ action_list_t *list = action_trace;
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++)
+ if (*rit == last_release)
+ break;
+ ASSERT(rit != list->rend());
+
/* Find a prior:
* load-acquire
* or
* load --sb-> fence-acquire */
- action_list_t *list = action_trace;
- action_list_t::reverse_iterator rit;
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ std::vector< ModelAction *, ModelAlloc<ModelAction *> > acquire_fences(get_num_threads(), NULL);
+ std::vector< ModelAction *, ModelAlloc<ModelAction *> > prior_loads(get_num_threads(), NULL);
+ bool found_acquire_fences = false;
+ for ( ; rit != list->rend(); rit++) {
ModelAction *prev = *rit;
if (act->same_thread(prev))
continue;
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 */
/* 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));
/**
* 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;
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_size() && curr->get_node()->future_value_empty()) {
priv->no_valid_reads = true;
set_assert();
}
projects / model-checker.git / blobdiff