+/** Arbitrary reads from the future are not allowed. Section 29.3
+ * part 9 places some constraints. This method checks one result of constraint
+ * constraint. Others require compiler support. */
+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());
+
+ //Get write that follows reader action
+ action_list_t *list = &(*thrd_lists)[id_to_int(reader->get_tid())];
+ action_list_t::reverse_iterator rit;
+ ModelAction *first_write_after_read=NULL;
+
+ for (rit = list->rbegin(); rit != list->rend(); rit++) {
+ ModelAction *act = *rit;
+ if (act==reader)
+ break;
+ if (act->is_write())
+ first_write_after_read=act;
+ }
+
+ if (first_write_after_read==NULL)
+ return true;
+
+ return !mo_graph->checkReachable(first_write_after_read, writer);
+}
+
+
+