*/
struct model_snapshot_members {
model_snapshot_members() :
- current_action(NULL),
/* First thread created will have id INITIAL_THREAD_ID */
next_thread_id(INITIAL_THREAD_ID),
used_sequence_numbers(0),
stats(),
failed_promise(false),
too_many_reads(false),
+ no_valid_reads(false),
bad_synchronization(false),
asserted(false)
{ }
bugs.clear();
}
- ModelAction *current_action;
unsigned int next_thread_id;
modelclock_t used_sequence_numbers;
ModelAction *next_backtrack;
struct execution_stats stats;
bool failed_promise;
bool too_many_reads;
+ bool no_valid_reads;
/** @brief Incorrectly-ordered synchronization was made */
bool bad_synchronization;
bool asserted;
/* Print all model-checker output before rollback */
fflush(model_out);
+ /**
+ * FIXME: if we utilize partial rollback, we will need to free only
+ * those pending actions which were NOT pending before the rollback
+ * point
+ */
+ for (unsigned int i = 0; i < get_num_threads(); i++)
+ delete get_thread(int_to_id(i))->get_pending();
+
snapshot_backtrack_before(0);
}
* adjacency of read/write portions of a RMW action, force THREAD_CREATE to be
* followed by a THREAD_START, or it can enforce execution replay/backtracking.
* The model-checker may have no preference regarding the next thread (i.e.,
- * when exploring a new execution ordering), in which case this will return
- * NULL.
- * @param curr The current ModelAction. This action might guide the choice of
- * next thread.
- * @return The next thread to run. If the model-checker has no preference, NULL.
+ * when exploring a new execution ordering), in which case we defer to the
+ * scheduler.
+ *
+ * @param curr Optional: The current ModelAction. Only used if non-NULL and it
+ * might guide the choice of next thread (i.e., THREAD_CREATE should be
+ * followed by THREAD_START, or ATOMIC_RMWR followed by ATOMIC_{RMW,RMWC})
+ * @return The next chosen thread to run, if any exist. Or else if no threads
+ * remain to be executed, return NULL.
*/
Thread * ModelChecker::get_next_thread(ModelAction *curr)
{
if (curr != NULL) {
/* Do not split atomic actions. */
if (curr->is_rmwr())
- return thread_current();
+ return get_thread(curr);
else if (curr->get_type() == THREAD_CREATE)
return curr->get_thread_operand();
}
- /* Have we completed exploring the preselected path? */
+ /*
+ * Have we completed exploring the preselected path? Then let the
+ * scheduler decide
+ */
if (diverge == NULL)
- return NULL;
+ return scheduler->select_next_thread();
/* Else, we are trying to replay an execution */
ModelAction *next = node_stack->get_next()->get_action();
/* 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();
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();
for (unsigned int i = 0; i < get_num_threads(); i++) {
thread_id_t tid = int_to_id(i);
Thread *thr = get_thread(tid);
- if (scheduler->is_sleep_set(thr) && thr->get_pending() == NULL) {
- thr->set_state(THREAD_RUNNING);
- scheduler->next_thread(thr);
- Thread::swap(&system_context, thr);
- priv->current_action->set_sleep_flag();
- thr->set_pending(priv->current_action);
+ if (scheduler->is_sleep_set(thr) && thr->get_pending()) {
+ thr->get_pending()->set_sleep_flag();
}
}
}
+/**
+ * @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);
}
}
priv->bad_synchronization = true;
}
+/**
+ * Check whether the current trace has triggered an assertion which should halt
+ * its execution.
+ *
+ * @return True, if the execution should be aborted; false otherwise
+ */
bool ModelChecker::has_asserted() const
{
return priv->asserted;
}
+/**
+ * Trigger a trace assertion which should cause this execution to be halted.
+ * This can be due to a detected bug or due to an infeasibility that should
+ * halt ASAP.
+ */
void ModelChecker::set_assert()
{
priv->asserted = true;
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 */
return true;
}
-ModelAction * ModelChecker::get_last_conflict(ModelAction *act)
+/**
+ * @brief Find the last fence-related backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking, as affected by fence
+ * operations. This includes pairs of potentially-synchronizing actions which
+ * occur due to fence-acquire or fence-release, and hence should be explored in
+ * the opposite execution order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act due to fences
+ */
+ModelAction * ModelChecker::get_last_fence_conflict(ModelAction *act) const
+{
+ /* Only perform release/acquire fence backtracking for stores */
+ if (!act->is_write())
+ return NULL;
+
+ /* Find a fence-release (or, act is a release) */
+ ModelAction *last_release;
+ if (act->is_release())
+ last_release = act;
+ else
+ last_release = get_last_fence_release(act->get_tid());
+ if (!last_release)
+ return NULL;
+
+ /* 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 */
+ 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;
+
+ int tid = id_to_int(prev->get_tid());
+
+ if (prev->is_read() && act->same_var(prev)) {
+ if (prev->is_acquire()) {
+ /* Found most recent load-acquire, don't need
+ * to search for more fences */
+ if (!found_acquire_fences)
+ return NULL;
+ } else {
+ prior_loads[tid] = prev;
+ }
+ }
+ if (prev->is_acquire() && prev->is_fence() && !acquire_fences[tid]) {
+ found_acquire_fences = true;
+ acquire_fences[tid] = prev;
+ }
+ }
+
+ ModelAction *latest_backtrack = NULL;
+ for (unsigned int i = 0; i < acquire_fences.size(); i++)
+ if (acquire_fences[i] && prior_loads[i])
+ if (!latest_backtrack || *latest_backtrack < *acquire_fences[i])
+ latest_backtrack = acquire_fences[i];
+ return latest_backtrack;
+}
+
+/**
+ * @brief Find the last backtracking conflict for a ModelAction
+ *
+ * This function performs the search for the most recent conflicting action
+ * against which we should perform backtracking. This primary includes pairs of
+ * synchronizing actions which should be explored in the opposite execution
+ * order.
+ *
+ * @param act The current action
+ * @return The most recent action which conflicts with act
+ */
+ModelAction * ModelChecker::get_last_conflict(ModelAction *act) const
{
switch (act->get_type()) {
- case ATOMIC_FENCE:
+ /* case ATOMIC_FENCE: fences don't directly cause backtracking */
case ATOMIC_READ:
case ATOMIC_WRITE:
case ATOMIC_RMW: {
- /* Optimization: relaxed operations don't need backtracking */
- if (act->is_relaxed())
- return NULL;
+ ModelAction *ret = NULL;
+
/* linear search: from most recent to oldest */
action_list_t *list = get_safe_ptr_action(obj_map, act->get_location());
action_list_t::reverse_iterator rit;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *prev = *rit;
- if (prev->could_synchronize_with(act))
- return prev;
+ if (prev->could_synchronize_with(act)) {
+ ret = prev;
+ break;
+ }
}
- break;
+
+ ModelAction *ret2 = get_last_fence_conflict(act);
+ if (!ret2)
+ return ret;
+ if (!ret)
+ return ret2;
+ if (*ret < *ret2)
+ return ret2;
+ return ret;
}
case ATOMIC_LOCK:
case ATOMIC_TRYLOCK: {
}
/**
- * 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)
{
+ 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();
- if (reads_from != NULL) {
- mo_graph->startChanges();
-
- value = reads_from->get_value();
- bool r_status = false;
+ bool updated = false;
+ switch (node->get_read_from_status()) {
+ case READ_FROM_PAST: {
+ const ModelAction *rf = node->get_read_from_past();
+ ASSERT(rf);
- if (!second_part_of_rmw) {
- check_recency(curr, reads_from);
- r_status = r_modification_order(curr, reads_from);
- }
+ mo_graph->startChanges();
- if (!second_part_of_rmw && is_infeasible() && (curr->get_node()->increment_read_from() || curr->get_node()->increment_future_value())) {
- mo_graph->rollbackChanges();
- priv->too_many_reads = false;
- continue;
+ ASSERT(!is_infeasible());
+ if (!check_recency(curr, rf)) {
+ if (node->increment_read_from()) {
+ mo_graph->rollbackChanges();
+ continue;
+ } else {
+ priv->too_many_reads = true;
+ }
}
- read_from(curr, reads_from);
+ updated = r_modification_order(curr, rf);
+ value = rf->get_value();
+ read_from(curr, rf);
mo_graph->commitChanges();
- mo_check_promises(curr->get_tid(), reads_from, NULL);
-
- updated |= r_status;
- } else if (!second_part_of_rmw) {
+ mo_check_promises(curr, true);
+ 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();
+ if (!check_recency(curr, promise))
+ priv->too_many_reads = true;
+ 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_value(fv.value);
- curr->set_read_from(NULL);
- promises->push_back(new Promise(curr, fv));
+ curr->set_read_from_promise(promise);
+ promises->push_back(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);
+ /* Readers to which we may send our future value */
+ std::vector< ModelAction *, ModelAlloc<ModelAction *> > send_fv;
+
+ bool updated_mod_order = w_modification_order(curr, &send_fv);
+ int promise_idx = get_promise_to_resolve(curr);
+ const ModelAction *earliest_promise_reader;
+ bool updated_promises = false;
+
+ if (promise_idx >= 0) {
+ earliest_promise_reader = (*promises)[promise_idx]->get_reader(0);
+ updated_promises = resolve_promise(curr, promise_idx);
+ } else
+ earliest_promise_reader = NULL;
+
+ /* Don't send future values to reads after the Promise we resolve */
+ for (unsigned int i = 0; i < send_fv.size(); i++) {
+ ModelAction *read = send_fv[i];
+ if (!earliest_promise_reader || *read < *earliest_promise_reader)
+ futurevalues->push_back(PendingFutureValue(curr, read));
+ }
if (promises->size() == 0) {
for (unsigned int i = 0; i < futurevalues->size(); i++) {
}
mo_graph->commitChanges();
- mo_check_promises(curr->get_tid(), curr, NULL);
+ mo_check_promises(curr, false);
get_thread(curr)->set_return_value(VALUE_NONE);
return updated_mod_order || updated_promises;
switch (curr->get_type()) {
case THREAD_CREATE: {
- Thread *th = curr->get_thread_operand();
+ 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, get_thread(curr));
+ add_thread(th);
th->set_creation(curr);
/* Promises can be satisfied by children */
for (unsigned int i = 0; i < promises->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();
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];
+ if (!promise->thread_is_available(waiting->get_id()))
+ continue;
+ 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;
+ }
+ }
+ }
+}
+
/**
* @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;
}
}
return true;
}
-/**
- * Stores the ModelAction for the current thread action. Call this
- * immediately before switching from user- to system-context to pass
- * data between them.
- * @param act The ModelAction created by the user-thread action
- */
-void ModelChecker::set_current_action(ModelAction *act) {
- priv->current_action = act;
-}
-
/**
* This is the heart of the model checker routine. It performs model-checking
* actions corresponding to a given "current action." Among other processes, it
/* 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 (act->is_read()) {
const ModelAction *rf = act->get_reads_from();
- if (rf != NULL && r_modification_order(act, rf))
- updated = true;
+ const Promise *promise = act->get_reads_from_promise();
+ if (rf) {
+ if (r_modification_order(act, rf))
+ updated = true;
+ } else if (promise) {
+ if (r_modification_order(act, promise))
+ updated = true;
+ }
}
if (act->is_write()) {
- if (w_modification_order(act))
+ if (w_modification_order(act, NULL))
updated = true;
}
mo_graph->commitChanges();
if ((parnode && !parnode->backtrack_empty()) ||
!currnode->misc_empty() ||
!currnode->read_from_empty() ||
- !currnode->future_value_empty() ||
!currnode->promise_empty() ||
!currnode->relseq_break_empty()) {
set_latest_backtrack(curr);
ptr += sprintf(ptr, "[failed promise]");
if (priv->too_many_reads)
ptr += sprintf(ptr, "[too many reads]");
+ if (priv->no_valid_reads)
+ ptr += sprintf(ptr, "[no valid reads-from]");
if (priv->bad_synchronization)
ptr += sprintf(ptr, "[bad sw ordering]");
if (promises_expired())
bool ModelChecker::is_infeasible() const
{
return mo_graph->checkForCycles() ||
+ priv->no_valid_reads ||
priv->failed_promise ||
priv->too_many_reads ||
priv->bad_synchronization ||
ModelAction * ModelChecker::process_rmw(ModelAction *act) {
ModelAction *lastread = get_last_action(act->get_tid());
lastread->process_rmw(act);
- if (act->is_rmw() && lastread->get_reads_from() != NULL) {
- mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+ if (act->is_rmw()) {
+ if (lastread->get_reads_from())
+ mo_graph->addRMWEdge(lastread->get_reads_from(), lastread);
+ else
+ mo_graph->addRMWEdge(lastread->get_reads_from_promise(), lastread);
mo_graph->commitChanges();
}
return lastread;
}
/**
- * Checks whether a thread has read from the same write for too many times
- * without seeing the effects of a later write.
- *
- * Basic idea:
- * 1) there must a different write that we could read from that would satisfy the modification order,
- * 2) we must have read from the same value in excess of maxreads times, and
- * 3) that other write must have been in the reads_from set for maxreads times.
+ * A helper function for ModelChecker::check_recency, to check if the current
+ * thread is able to read from a different write/promise for 'params.maxreads'
+ * number of steps and if that write/promise should become visible (i.e., is
+ * ordered later in the modification order). This helps model memory liveness.
*
- * If so, we decide that the execution is no longer feasible.
+ * @param curr The current action. Must be a read.
+ * @param rf The write/promise from which we plan to read
+ * @param other_rf The write/promise from which we may read
+ * @return True if we were able to read from other_rf for params.maxreads steps
*/
-void ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf)
+template <typename T, typename U>
+bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const
{
- if (params.maxreads != 0) {
- if (curr->get_node()->get_read_from_size() <= 1)
- return;
- //Must make sure that execution is currently feasible... We could
- //accidentally clear by rolling back
- if (is_infeasible())
- return;
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
- int tid = id_to_int(curr->get_tid());
-
- /* Skip checks */
- if ((int)thrd_lists->size() <= tid)
- return;
- action_list_t *list = &(*thrd_lists)[tid];
-
- action_list_t::reverse_iterator rit = list->rbegin();
- /* Skip past curr */
- for (; (*rit) != curr; rit++)
- ;
- /* go past curr now */
- rit++;
-
- action_list_t::reverse_iterator ritcopy = rit;
- //See if we have enough reads from the same value
- int count = 0;
- for (; count < params.maxreads; rit++, count++) {
- if (rit == list->rend())
- return;
- ModelAction *act = *rit;
- if (!act->is_read())
- return;
-
- if (act->get_reads_from() != rf)
- return;
- if (act->get_node()->get_read_from_size() <= 1)
- return;
- }
- for (int i = 0; i < curr->get_node()->get_read_from_size(); i++) {
- /* Get write */
- const ModelAction *write = curr->get_node()->get_read_from_at(i);
+ /* Need a different write/promise */
+ if (other_rf->equals(rf))
+ return false;
- /* Need a different write */
- if (write == rf)
- continue;
+ /* Only look for "newer" writes/promises */
+ if (!mo_graph->checkReachable(rf, other_rf))
+ return false;
- /* Test to see whether this is a feasible write to read from */
- mo_graph->startChanges();
- r_modification_order(curr, write);
- bool feasiblereadfrom = !is_infeasible();
- mo_graph->rollbackChanges();
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ action_list_t *list = &(*thrd_lists)[id_to_int(curr->get_tid())];
+ action_list_t::reverse_iterator rit = list->rbegin();
+ ASSERT((*rit) == curr);
+ /* Skip past curr */
+ rit++;
+
+ /* Does this write/promise work for everyone? */
+ for (int i = 0; i < params.maxreads; i++, rit++) {
+ ModelAction *act = *rit;
+ if (!act->may_read_from(other_rf))
+ return false;
+ }
+ return true;
+}
- if (!feasiblereadfrom)
- continue;
- rit = ritcopy;
+/**
+ * Checks whether a thread has read from the same write or Promise for too many
+ * times without seeing the effects of a later write/Promise.
+ *
+ * Basic idea:
+ * 1) there must a different write/promise that we could read from,
+ * 2) we must have read from the same write/promise in excess of maxreads times,
+ * 3) that other write/promise must have been in the reads_from set for maxreads times, and
+ * 4) that other write/promise must be mod-ordered after the write/promise we are reading.
+ *
+ * If so, we decide that the execution is no longer feasible.
+ *
+ * @param curr The current action. Must be a read.
+ * @param rf The ModelAction/Promise from which we might read.
+ * @return True if the read should succeed; false otherwise
+ */
+template <typename T>
+bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
+{
+ if (!params.maxreads)
+ return true;
- bool feasiblewrite = true;
- //new we need to see if this write works for everyone
+ //NOTE: Next check is just optimization, not really necessary....
+ if (curr->get_node()->get_read_from_past_size() +
+ curr->get_node()->get_read_from_promise_size() <= 1)
+ return true;
- 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) {
- foundvalue = true;
- break;
- }
- }
- if (!foundvalue) {
- feasiblewrite = false;
- break;
- }
- }
- if (feasiblewrite) {
- priv->too_many_reads = true;
- return;
- }
- }
+ std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
+ int tid = id_to_int(curr->get_tid());
+ ASSERT(tid < (int)thrd_lists->size());
+ action_list_t *list = &(*thrd_lists)[tid];
+ action_list_t::reverse_iterator rit = list->rbegin();
+ ASSERT((*rit) == curr);
+ /* Skip past curr */
+ rit++;
+
+ action_list_t::reverse_iterator ritcopy = rit;
+ /* See if we have enough reads from the same value */
+ for (int count = 0; count < params.maxreads; ritcopy++, count++) {
+ if (ritcopy == list->rend())
+ return true;
+ ModelAction *act = *ritcopy;
+ if (!act->is_read())
+ return true;
+ if (act->get_reads_from_promise() && !act->get_reads_from_promise()->equals(rf))
+ return true;
+ if (act->get_reads_from() && !act->get_reads_from()->equals(rf))
+ return true;
+ if (act->get_node()->get_read_from_past_size() +
+ act->get_node()->get_read_from_promise_size() <= 1)
+ return true;
+ }
+ for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
+ const ModelAction *write = curr->get_node()->get_read_from_past(i);
+ if (should_read_instead(curr, rf, write))
+ return false; /* liveness failure */
+ }
+ for (int i = 0; i < curr->get_node()->get_read_from_promise_size(); i++) {
+ const Promise *promise = curr->get_node()->get_read_from_promise(i);
+ if (should_read_instead(curr, rf, promise))
+ return false; /* liveness failure */
}
+ return true;
}
/**
* read.
*
* Basic idea is the following: Go through each other thread and find
- * the lastest action that happened before our read. Two cases:
+ * the last action that happened before our read. Two cases:
*
* (1) The action is a write => that write must either occur before
* the write we read from or be the write we read from.
* must occur before the write we read from or be the same write.
*
* @param curr The current action. Must be a read.
- * @param rf The action that curr reads from. Must be a write.
+ * @param rf The ModelAction or Promise that curr reads from. Must be a write.
* @return True if modification order edges were added; false otherwise
*/
-bool ModelChecker::r_modification_order(ModelAction *curr, const ModelAction *rf)
+template <typename rf_type>
+bool ModelChecker::r_modification_order(ModelAction *curr, const rf_type *rf)
{
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
for (rit = list->rbegin(); rit != list->rend(); rit++) {
ModelAction *act = *rit;
- if (act->is_write() && act != rf && act != curr) {
+ if (act->is_write() && !act->equals(rf) && act != curr) {
/* C++, Section 29.3 statement 5 */
if (curr->is_seqcst() && last_sc_fence_thread_local &&
*act < *last_sc_fence_thread_local) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
/* C++, Section 29.3 statement 4 */
else if (act->is_seqcst() && last_sc_fence_local &&
*act < *last_sc_fence_local) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
/* C++, Section 29.3 statement 6 */
else if (last_sc_fence_thread_before &&
*act < *last_sc_fence_thread_before) {
- mo_graph->addEdge(act, rf);
- added = true;
+ added = mo_graph->addEdge(act, rf) || added;
break;
}
}
*/
if (act->happens_before(curr) && act != curr) {
if (act->is_write()) {
- if (rf != act) {
- mo_graph->addEdge(act, rf);
- added = true;
+ if (!act->equals(rf)) {
+ 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 (rf != prevreadfrom) {
- mo_graph->addEdge(prevreadfrom, rf);
- added = true;
+ 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;
}
}
- return added;
-}
-
-/** This method fixes up the modification order when we resolve a
- * promises. The basic problem is that actions that occur after the
- * read curr could not property add items to the modification order
- * for our read.
- *
- * So for each thread, we find the earliest item that happens after
- * the read curr. This is the item we have to fix up with additional
- * constraints. If that action is write, we add a MO edge between
- * the Action rf and that action. If the action is a read, we add a
- * MO edge between the Action rf, and whatever the read accessed.
- *
- * @param curr is the read ModelAction that we are fixing up MO edges for.
- * @param rf is the write ModelAction that curr reads from.
- *
- */
-void ModelChecker::post_r_modification_order(ModelAction *curr, const ModelAction *rf)
-{
- std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
- unsigned int i;
- ASSERT(curr->is_read());
-
- /* Iterate over all threads */
- for (i = 0; i < thrd_lists->size(); i++) {
- /* Iterate over actions in thread, starting from most recent */
- action_list_t *list = &(*thrd_lists)[i];
- action_list_t::reverse_iterator rit;
- ModelAction *lastact = NULL;
-
- /* Find last action that happens after curr that is either not curr or a rmw */
- for (rit = list->rbegin(); rit != list->rend(); rit++) {
- ModelAction *act = *rit;
- if (curr->happens_before(act) && (curr != act || curr->is_rmw())) {
- lastact = act;
- } else
- break;
- }
+ /*
+ * All compatible, thread-exclusive promises must be ordered after any
+ * concrete loads from the same thread
+ */
+ for (unsigned int i = 0; i < promises->size(); i++)
+ if ((*promises)[i]->is_compatible_exclusive(curr))
+ added = mo_graph->addEdge(rf, (*promises)[i]) || added;
- /* Include at most one act per-thread that "happens before" curr */
- if (lastact != NULL) {
- if (lastact == curr) {
- //Case 1: The resolved read is a RMW, and we need to make sure
- //that the write portion of the RMW mod order after rf
-
- mo_graph->addEdge(rf, lastact);
- } else if (lastact->is_read()) {
- //Case 2: The resolved read is a normal read and the next
- //operation is a read, and we need to make sure the value read
- //is mod ordered after rf
-
- const ModelAction *postreadfrom = lastact->get_reads_from();
- if (postreadfrom != NULL && rf != postreadfrom)
- mo_graph->addEdge(rf, postreadfrom);
- } else {
- //Case 3: The resolved read is a normal read and the next
- //operation is a write, and we need to make sure that the
- //write is mod ordered after rf
- if (lastact != rf)
- mo_graph->addEdge(rf, lastact);
- }
- break;
- }
- }
+ return added;
}
/**
* (II) Sending the write back to non-synchronizing reads.
*
* @param curr The current action. Must be a write.
+ * @param send_fv A vector for stashing reads to which we may pass our future
+ * value. If NULL, then don't record any future values.
* @return True if modification order edges were added; false otherwise
*/
-bool ModelChecker::w_modification_order(ModelAction *curr)
+bool ModelChecker::w_modification_order(ModelAction *curr, std::vector< ModelAction *, ModelAlloc<ModelAction *> > *send_fv)
{
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
unsigned int i;
so we are initialized. */
ModelAction *last_seq_cst = get_last_seq_cst_write(curr);
if (last_seq_cst != NULL) {
- mo_graph->addEdge(last_seq_cst, curr);
- added = true;
+ added = mo_graph->addEdge(last_seq_cst, curr) || added;
}
}
/* C++, Section 29.3 statement 7 */
if (last_sc_fence_thread_before && act->is_write() &&
*act < *last_sc_fence_thread_before) {
- mo_graph->addEdge(act, curr);
- added = true;
+ added = mo_graph->addEdge(act, curr) || added;
break;
}
* readfrom(act) --mo--> act
*/
if (act->is_write())
- mo_graph->addEdge(act, curr);
+ added = mo_graph->addEdge(act, curr) || added;
else if (act->is_read()) {
//if previous read accessed a null, just keep going
if (act->get_reads_from() == NULL)
continue;
- mo_graph->addEdge(act->get_reads_from(), curr);
+ added = mo_graph->addEdge(act->get_reads_from(), curr) || added;
}
- added = true;
break;
} else if (act->is_read() && !act->could_synchronize_with(curr) &&
!act->same_thread(curr)) {
pendingfuturevalue.
*/
- if (thin_air_constraint_may_allow(curr, act)) {
+ if (send_fv && thin_air_constraint_may_allow(curr, act)) {
if (!is_infeasible())
- futurevalues->push_back(PendingFutureValue(curr, act));
+ send_fv->push_back(act);
else if (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() && curr->get_reads_from() == act->get_reads_from())
add_future_value(curr, act);
}
}
}
+ /*
+ * All compatible, thread-exclusive promises must be ordered after any
+ * concrete stores to the same thread, or else they can be merged with
+ * this store later
+ */
+ for (unsigned int i = 0; i < promises->size(); i++)
+ if ((*promises)[i]->is_compatible_exclusive(curr))
+ added = mo_graph->addEdge(curr, (*promises)[i]) || added;
+
return added;
}
if (mo_graph->checkForCycles())
return false;
- while (rf) {
+ for ( ; rf != NULL; rf = rf->get_reads_from()) {
ASSERT(rf->is_write());
if (rf->is_release())
/* acq_rel RMW is a sufficient stopping condition */
if (rf->is_acquire() && rf->is_release())
return true; /* complete */
-
- rf = rf->get_reads_from();
};
if (!rf) {
/* read from future: need to settle this later */
}
/**
- * 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 resolved = false;
std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
+ 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();
- if (read->is_rmw()) {
- mo_graph->addRMWEdge(write, read);
- }
- read_from(read, write);
- //First fix up the modification order for actions that happened
- //before the read
- r_modification_order(read, write);
- //Next fix up the modification order for actions that happened
- //after the read.
- post_r_modification_order(read, write);
- //Make sure the promise's value matches the write's value
- ASSERT(promise->get_value() == write->get_value());
- delete promise;
+ 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);
- promises->erase(promises->begin() + promise_index);
- actions_to_check.push_back(read);
+ promises->erase(promises->begin() + promise_idx);
- resolved = 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;
//Check whether reading these writes has made threads unable to
//resolve promises
for (unsigned int i = 0; i < actions_to_check.size(); i++) {
- ModelAction *read=actions_to_check[i];
- mo_check_promises(read->get_tid(), write, read);
+ ModelAction *read = actions_to_check[i];
+ mo_check_promises(read, true);
}
- return resolved;
+ return true;
}
/**
{
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
- const ModelAction *act = promise->get_action();
- if (!act->happens_before(curr) &&
- act->is_read() &&
- !act->could_synchronize_with(curr) &&
- !act->same_thread(curr) &&
- act->get_location() == curr->get_location() &&
- 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;
+ }
}
}
}
* @brief Checks promises in response to addition to modification order for
* threads.
*
- * Definitions:
- *
- * pthread is the thread that performed the read that created the promise
- *
- * pread is the read that created the promise
- *
- * pwrite is either the first write to same location as pread by
- * pthread that is sequenced after pread or the write read by the
- * first read to the same location as pread by pthread that is
- * sequenced after pread.
+ * We test whether threads are still available for satisfying promises after an
+ * addition to our modification order constraints. Those that are unavailable
+ * are "eliminated". Once all threads are eliminated from satisfying a promise,
+ * that promise has failed.
*
- * 1. If tid=pthread, then we check what other threads are reachable
- * through the mod order starting with pwrite. Those threads cannot
- * perform a write that will resolve the promise due to modification
- * order constraints.
- *
- * 2. If the tid is not pthread, we check whether pwrite can reach the
- * action write through the modification order. If so, that thread
- * cannot perform a future write that will resolve the promise due to
- * modificatin order constraints.
- *
- * @param tid The thread that either read from the model action write, or
- * actually did the model action write.
- *
- * @param write The ModelAction representing the relevant write.
- * @param read The ModelAction that reads a promised write, or NULL otherwise.
+ * @param act The ModelAction which updated the modification order
+ * @param is_read_check Should be true if act is a read and we must check for
+ * updates to the store from which it read (there is a distinction here for
+ * RMW's, which are both a load and a store)
*/
-void ModelChecker::mo_check_promises(thread_id_t tid, const ModelAction *write, const ModelAction *read)
+void ModelChecker::mo_check_promises(const ModelAction *act, bool is_read_check)
{
- void *location = write->get_location();
+ const ModelAction *write = is_read_check ? act->get_reads_from() : act;
+
for (unsigned int i = 0; i < promises->size(); i++) {
Promise *promise = (*promises)[i];
- const ModelAction *act = promise->get_action();
// Is this promise on the same location?
- if (act->get_location() != location)
+ if (!promise->same_location(write))
continue;
- // same thread as the promise
- if (act->get_tid() == tid) {
- // make sure that the reader of this write happens after the promise
- if ((read == NULL) || (promise->get_action()->happens_before(read))) {
- // do we have a pwrite for the promise, if not, set it
- if (promise->get_write() == NULL) {
- promise->set_write(write);
- // The pwrite cannot happen before the promise
- if (write->happens_before(act) && (write != act)) {
- priv->failed_promise = true;
- return;
- }
- }
-
- if (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
- if (!promise->thread_is_available(tid))
+ if (!promise->thread_is_available(act->get_tid()))
continue;
- if (promise->get_write() && mo_graph->checkReachable(promise->get_write(), write)) {
- if (promise->eliminate_thread(tid)) {
+ if (mo_graph->checkReachable(promise, write)) {
+ if (mo_graph->checkPromise(write, promise)) {
priv->failed_promise = true;
return;
}
/**
* 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;
else if (curr->get_sleep_flag() && !curr->is_seqcst() && !sleep_can_read_from(curr, act))
allow_read = false;
- if (allow_read)
- curr->get_node()->add_read_from(act);
+ if (allow_read) {
+ /* Only add feasible reads */
+ mo_graph->startChanges();
+ r_modification_order(curr, act);
+ if (!is_infeasible())
+ curr->get_node()->add_read_from_past(act);
+ mo_graph->rollbackChanges();
+ }
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr))
}
}
+ /* Inherit existing, promised future values */
+ for (i = 0; i < promises->size(); i++) {
+ const Promise *promise = (*promises)[i];
+ 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())
+ 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()->read_from_size()) {
+ 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");
}
}
bool ModelChecker::sleep_can_read_from(ModelAction *curr, const ModelAction *write)
{
- while (true) {
+ for ( ; write != NULL; write = write->get_reads_from()) {
/* UNINIT actions don't have a Node, and they never sleep */
if (write->is_uninitialized())
return true;
bool thread_sleep = prevnode->enabled_status(curr->get_tid()) == THREAD_SLEEP_SET;
if (write->is_release() && thread_sleep)
return true;
- if (!write->is_rmw()) {
+ if (!write->is_rmw())
return false;
- }
- if (write->get_reads_from() == NULL)
- return true;
- write = write->get_reads_from();
}
+ return true;
}
/**
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=\"%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
return scheduler->is_enabled(tid);
}
+/**
+ * Switch from a model-checker context to a user-thread context. This is the
+ * complement of ModelChecker::switch_to_master and must be called from the
+ * model-checker context
+ *
+ * @param thread The user-thread to switch to
+ */
+void ModelChecker::switch_from_master(Thread *thread)
+{
+ scheduler->set_current_thread(thread);
+ Thread::swap(&system_context, thread);
+}
+
/**
* Switch from a user-context to the "master thread" context (a.k.a. system
* context). This switch is made with the intention of exploring a particular
{
DBG();
Thread *old = thread_current();
- set_current_action(act);
- old->set_state(THREAD_READY);
+ ASSERT(!old->get_pending());
+ old->set_pending(act);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
exit(EXIT_FAILURE);
/**
* Takes the next step in the execution, if possible.
* @param curr The current step to take
- * @return Returns true (success) if a step was taken and false otherwise.
+ * @return Returns the next Thread to run, if any; NULL if this execution
+ * should terminate
*/
-bool ModelChecker::take_step(ModelAction *curr)
+Thread * ModelChecker::take_step(ModelAction *curr)
{
- if (has_asserted())
- return false;
-
Thread *curr_thrd = get_thread(curr);
ASSERT(curr_thrd->get_state() == THREAD_READY);
/* Infeasible -> don't take any more steps */
if (is_infeasible())
- return false;
+ return NULL;
else if (isfeasibleprefix() && have_bug_reports()) {
set_assert();
- return false;
+ return NULL;
}
- if (params.bound != 0)
- if (priv->used_sequence_numbers > params.bound)
- return false;
+ if (params.bound != 0 && priv->used_sequence_numbers > params.bound)
+ return NULL;
if (curr_thrd->is_blocked() || curr_thrd->is_complete())
scheduler->remove_thread(curr_thrd);
Thread *next_thrd = get_next_thread(curr);
- next_thrd = scheduler->next_thread(next_thrd);
DEBUG("(%d, %d)\n", curr_thrd ? id_to_int(curr_thrd->get_id()) : -1,
next_thrd ? id_to_int(next_thrd->get_id()) : -1);
- /*
- * Launch end-of-execution release sequence fixups only when there are:
- *
- * (1) no more user threads to run (or when execution replay chooses
- * the 'model_thread')
- * (2) pending release sequences
- * (3) pending assertions (i.e., data races)
- * (4) no pending promises
- */
- if (!pending_rel_seqs->empty() && (!next_thrd || next_thrd->is_model_thread()) &&
- is_feasible_prefix_ignore_relseq() && !unrealizedraces.empty()) {
- model_print("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
- pending_rel_seqs->size());
- ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
- std::memory_order_seq_cst, NULL, VALUE_NONE,
- model_thread);
- set_current_action(fixup);
- return true;
- }
-
- /* next_thrd == NULL -> don't take any more steps */
- if (!next_thrd)
- return false;
-
- next_thrd->set_state(THREAD_RUNNING);
-
- if (next_thrd->get_pending() != NULL) {
- /* restart a pending action */
- set_current_action(next_thrd->get_pending());
- next_thrd->set_pending(NULL);
- next_thrd->set_state(THREAD_READY);
- return true;
- }
-
- /* Return false only if swap fails with an error */
- return (Thread::swap(&system_context, next_thrd) == 0);
+ return next_thrd;
}
/** Wrapper to run the user's main function, with appropriate arguments */
{
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);
- /* Run user thread up to its first action */
- scheduler->next_thread(t);
- Thread::swap(&system_context, t);
+ do {
+ /*
+ * Stash next pending action(s) for thread(s). There
+ * should only need to stash one thread's action--the
+ * thread which just took a step--plus the first step
+ * for any newly-created thread
+ */
+ for (unsigned int i = 0; i < get_num_threads(); i++) {
+ thread_id_t tid = int_to_id(i);
+ Thread *thr = get_thread(tid);
+ if (!thr->is_model_thread() && !thr->is_complete() && !thr->get_pending()) {
+ switch_from_master(thr);
+ }
+ }
+
+ /* Catch assertions from prior take_step or from
+ * between-ModelAction bugs (e.g., data races) */
+ if (has_asserted())
+ break;
+
+ /* Consume the next action for a Thread */
+ ModelAction *curr = t->get_pending();
+ t->set_pending(NULL);
+ t = take_step(curr);
+ } while (t && !t->is_model_thread());
- /* Wait for all threads to complete */
- while (take_step(priv->current_action));
+ /*
+ * Launch end-of-execution release sequence fixups only when
+ * the execution is otherwise feasible AND there are:
+ *
+ * (1) pending release sequences
+ * (2) pending assertions that could be invalidated by a change
+ * in clock vectors (i.e., data races)
+ * (3) no pending promises
+ */
+ while (!pending_rel_seqs->empty() &&
+ is_feasible_prefix_ignore_relseq() &&
+ !unrealizedraces.empty()) {
+ model_print("*** WARNING: release sequence fixup action "
+ "(%zu pending release seuqence(s)) ***\n",
+ pending_rel_seqs->size());
+ ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,
+ std::memory_order_seq_cst, NULL, VALUE_NONE,
+ model_thread);
+ take_step(fixup);
+ };
} while (next_execution());
+ model_print("******* Model-checking complete: *******\n");
print_stats();
}
projects / c11tester.git / blobdiff