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;
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;
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:
- *
- * 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(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 *act = promise->get_action();
+ const ModelAction *pread = promise->get_action();
// Is this promise on the same location?
- if (!act->same_var(write))
+ if (!pread->same_var(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;
- }
- }
+ 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;
- 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;
}
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");
projects / c11tester.git / blobdiff