stats(),
failed_promise(false),
too_many_reads(false),
+ no_valid_reads(false),
bad_synchronization(false),
asserted(false)
{ }
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;
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();
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++) {
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;
* @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.
- *
- * 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.
+ * 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.
*
- * 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(const ModelAction *act, bool is_read_check)
{
- thread_id_t tid = act->get_tid();
const ModelAction *write = is_read_check ? act->get_reads_from() : act;
for (unsigned int i = 0; i < promises->size(); i++) {
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 (!is_read_check || (pread->happens_before(act))) {
- // 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);
if (Thread::swap(old, &system_context) < 0) {
perror("swap threads");
exit(EXIT_FAILURE);
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;
}
projects / model-checker.git / blobdiff