+/**
+ * Arbitrary reads from the future are not allowed. Section 29.3 part 9 places
+ * some constraints. This method checks one the following constraint (others
+ * require compiler support):
+ *
+ * If X --hb-> Y --mo-> Z, then X should not read from Z.
+ */
+bool ModelChecker::mo_may_allow(const ModelAction *writer, const ModelAction *reader)
+{
+ std::vector<action_list_t> *thrd_lists = obj_thrd_map->get_safe_ptr(reader->get_location());
+ unsigned int i;
+
+ /* Iterate over all threads */
+ for (i = 0; i < thrd_lists->size(); i++) {
+ const ModelAction *write_after_read = NULL;
+
+ /* Iterate over actions in thread, starting from most recent */
+ action_list_t *list = &(*thrd_lists)[i];
+ action_list_t::reverse_iterator rit;
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+
+ if (!reader->happens_before(act))
+ break;
+ else if (act->is_write())
+ write_after_read = act;
+ else if (act->is_read()&&act->get_reads_from()!=NULL) {
+ write_after_read = act->get_reads_from();
+ }
+ }
+
+ if (write_after_read && write_after_read!=writer && mo_graph->checkReachable(write_after_read, writer))
+ return false;
+ }
+
+ return true;
+}
+