+/** 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::thin_air_constraint_may_allow(const ModelAction * writer, const ModelAction *reader) {
+ if (!writer->is_rmw())
+ return true;
+
+ if (!reader->is_rmw())
+ return true;
+
+ for(const ModelAction *search=writer->get_reads_from();search!=NULL;search=search->get_reads_from()) {
+ if (search==reader)
+ return false;
+ if (search->get_tid()==reader->get_tid()&&
+ search->happens_before(reader))
+ break;
+ }
+
+ return true;
+}
+
+