bool ModelChecker::process_read(ModelAction *curr)
{
Node *node = curr->get_node();
- uint64_t value = VALUE_NONE;
- bool updated = false;
while (true) {
+ bool updated = false;
switch (node->get_read_from_status()) {
case READ_FROM_PAST: {
const ModelAction *rf = node->get_read_from_past();
ASSERT(rf);
mo_graph->startChanges();
- value = rf->get_value();
- check_recency(curr, rf);
- bool r_status = r_modification_order(curr, rf);
- if (is_infeasible() && node->increment_read_from()) {
- 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;
+ }
}
+ updated = r_modification_order(curr, rf);
read_from(curr, rf);
mo_graph->commitChanges();
mo_check_promises(curr, true);
-
- updated |= r_status;
break;
}
case READ_FROM_PROMISE: {
Promise *promise = curr->get_node()->get_read_from_promise();
- promise->add_reader(curr);
- value = promise->get_value();
+ if (promise->add_reader(curr))
+ priv->failed_promise = true;
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;
/* Read from future value */
struct future_value fv = node->get_future_value();
Promise *promise = new Promise(curr, fv);
- value = fv.value;
curr->set_read_from_promise(promise);
promises->push_back(promise);
mo_graph->startChanges();
default:
ASSERT(false);
}
- get_thread(curr)->set_return_value(value);
+ get_thread(curr)->set_return_value(curr->get_return_value());
return updated;
}
}
*/
bool ModelChecker::process_mutex(ModelAction *curr)
{
- std::mutex *mutex = NULL;
+ std::mutex *mutex = curr->get_mutex();
struct std::mutex_state *state = NULL;
- if (curr->is_trylock() || curr->is_lock() || curr->is_unlock()) {
- mutex = (std::mutex *)curr->get_location();
+ if (mutex)
state = mutex->get_state();
- } else if (curr->is_wait()) {
- mutex = (std::mutex *)curr->get_value();
- state = mutex->get_state();
- }
switch (curr->get_type()) {
case ATOMIC_TRYLOCK: {
*/
bool ModelChecker::process_write(ModelAction *curr)
{
- bool updated_mod_order = w_modification_order(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)
+ 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++) {
}
}
if (act->is_write()) {
- if (w_modification_order(act))
+ if (w_modification_order(act, NULL))
updated = true;
}
mo_graph->commitChanges();
}
/**
- * 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_past_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_past_size() <= 1)
- return;
- }
- for (int i = 0; i < curr->get_node()->get_read_from_past_size(); i++) {
- /* Get write */
- const ModelAction *write = curr->get_node()->get_read_from_past(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 */
- /** NOTE: all members of read-from set should be
- * feasible, so we no longer check it here **/
+ 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;
+}
- 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_past_size(); j++) {
- if (act->get_node()->get_read_from_past(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;
}
/**
* (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;
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);
}
bool ModelChecker::resolve_promise(ModelAction *write, unsigned int promise_idx)
{
std::vector< ModelAction *, ModelAlloc<ModelAction *> > actions_to_check;
- promise_list_t mustResolve;
Promise *promise = (*promises)[promise_idx];
for (unsigned int i = 0; i < promise->get_num_readers(); i++) {
}
/* 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);
+ if (!mo_graph->resolvePromise(promise, write))
+ priv->failed_promise = true;
promises->erase(promises->begin() + promise_idx);
-
- /** @todo simplify the 'mustResolve' stuff */
- ASSERT(mustResolve.size() <= 1);
-
- if (!mustResolve.empty() && mustResolve[0] != promise)
- priv->failed_promise = true;
- delete promise;
+ /**
+ * @todo It is possible to end up in an inconsistent state, where a
+ * "resolved" promise may still be referenced if
+ * CycleGraph::resolvePromise() failed, so don't delete 'promise'.
+ *
+ * Note that the inconsistency only matters when dumping mo_graph to
+ * file.
+ *
+ * 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, true);