mo_graph->startChanges();
ASSERT(!is_infeasible());
- if (!check_recency(curr, rf))
- priv->too_many_reads = true;
- updated = r_modification_order(curr, rf);
-
- if (is_infeasible() && node->increment_read_from()) {
- mo_graph->rollbackChanges();
- priv->too_many_reads = false;
- continue;
+ 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);
value = rf->get_value();
read_from(curr, rf);
mo_graph->commitChanges();
mo_check_promises(curr, true);
-
break;
}
case READ_FROM_PROMISE: {
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;
}
/**
- * Checks whether a thread has read from the same write for too many times
- * without seeing the effects of a later write.
+ * 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.
+ *
+ * @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
+ */
+template <typename T, typename U>
+bool ModelChecker::should_read_instead(const ModelAction *curr, const T *rf, const U *other_rf) const
+{
+ /* Need a different write/promise */
+ if (other_rf->equals(rf))
+ return false;
+
+ /* Only look for "newer" writes/promises */
+ if (!mo_graph->checkReachable(rf, other_rf))
+ return false;
+
+ 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;
+}
+
+/**
+ * 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 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.
+ * 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 store from which we might read.
+ * @param rf The ModelAction/Promise from which we might read.
* @return True if the read should succeed; false otherwise
*/
-bool ModelChecker::check_recency(ModelAction *curr, const ModelAction *rf) const
+template <typename T>
+bool ModelChecker::check_recency(ModelAction *curr, const T *rf) const
{
if (!params.maxreads)
return true;
//NOTE: Next check is just optimization, not really necessary....
- if (curr->get_node()->get_read_from_past_size() <= 1)
+ if (curr->get_node()->get_read_from_past_size() +
+ curr->get_node()->get_read_from_promise_size() <= 1)
return true;
std::vector<action_list_t> *thrd_lists = get_safe_ptr_vect_action(obj_thrd_map, curr->get_location());
ModelAction *act = *ritcopy;
if (!act->is_read())
return true;
- if (act->get_reads_from() != rf)
+ if (act->get_reads_from_promise() && !act->get_reads_from_promise()->equals(rf))
return true;
- if (act->get_node()->get_read_from_past_size() <= 1)
+ 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++) {
- /* Get write */
const ModelAction *write = curr->get_node()->get_read_from_past(i);
-
- /* Need a different write */
- if (write == rf)
- continue;
-
- /* Only look for "newer" writes */
- if (!mo_graph->checkReachable(rf, write))
- continue;
-
- ritcopy = rit;
-
- bool feasiblewrite = true;
- /* now we need to see if this write works for everyone */
- for (int loop = params.maxreads; loop > 0; loop--, ritcopy++) {
- ModelAction *act = *ritcopy;
- if (!act->may_read_from(write)) {
- feasiblewrite = false;
- break;
- }
- }
- if (feasiblewrite)
- return false;
+ 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;
}