*/
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);
}
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();
}
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();
}
}
}
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;
read_from(curr, reads_from);
mo_graph->commitChanges();
- mo_check_promises(curr->get_tid(), reads_from, NULL);
+ mo_check_promises(curr, true);
updated |= r_status;
} else if (!second_part_of_rmw) {
}
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);
+ add_thread(th);
th->set_creation(curr);
/* Promises can be satisfied by children */
for (unsigned int i = 0; i < promises->size(); i++) {
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
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 ||
continue;
/* 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();
+ /** NOTE: all members of read-from set should be
+ * feasible, so we no longer check it here **/
- if (!feasiblereadfrom)
- continue;
rit = ritcopy;
bool feasiblewrite = true;
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);
+ mo_check_promises(read, true);
}
return haveResolved;
* @brief Checks promises in response to addition to modification order for
* threads.
*
- * Definitions:
+ * 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.
*
- * 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.
- *
- * 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)
{
+ 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 *pread = promise->get_action();
if (!pread->same_var(write))
continue;
- // same thread as pread
- if (pread->get_tid() == tid) {
- // make sure that the reader of this write happens after the promise
- if ((read == NULL) || (pread->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 pread
- if (write->happens_before(pread) && (write != pread)) {
- priv->failed_promise = true;
- return;
- }
- }
-
- if (mo_graph->checkPromise(write, promise)) {
- priv->failed_promise = true;
- return;
- }
- }
+ if (pread->happens_before(act) && mo_graph->checkPromise(write, promise)) {
+ priv->failed_promise = true;
+ return;
}
// 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;
- const ModelAction *pwrite = promise->get_write();
- if (pwrite && mo_graph->checkReachable(pwrite, write)) {
- if (promise->eliminate_thread(tid)) {
+ if (mo_graph->checkReachable(promise, write)) {
+ if (mo_graph->checkPromise(write, promise)) {
priv->failed_promise = true;
return;
}
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(act);
+ mo_graph->rollbackChanges();
+ }
/* Include at most one act per-thread that "happens before" curr */
if (act->happens_before(curr))
break;
}
}
+ /* We may find no valid may-read-from only if the execution is doomed */
+ if (!curr->get_node()->get_read_from_size()) {
+ priv->no_valid_reads = true;
+ set_assert();
+ }
if (DBG_ENABLED()) {
model_print("Reached read action:\n");
{
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);
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;
+ model_thread->set_pending(fixup);
+ return model_thread;
}
- /* 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);
-
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()) {
+ scheduler->next_thread(thr);
+ Thread::swap(&system_context, thr);
+ }
+ }
+
+ /* Catch assertions from prior take_step or from
+ * between-ModelAction bugs (e.g., data races) */
+ if (has_asserted())
+ break;
- /* Wait for all threads to complete */
- while (take_step(priv->current_action));
+ /* 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());
+ /** @TODO Re-write release sequence fixups here */
} while (next_execution());
print_stats();
projects / c11tester.git / blobdiff