Memory Model: Add acyclicity (consistency) axiom and rephrase Scoped Modification Order Coherence section as a consequence of it (#927)

appendices/memorymodel.txt

@@ -786,21 +786,53 @@ NOTE: It is possible for there to be a write between X and Y that overwrites
 a subset of the memory locations, but the remaining memory locations (M~2~)
 will still be visible-to Y.
 
+[[memory-model-acyclicity]]
+== Acyclicity
+
+_Reads-from_ is a relation between operations, where the first operation is a
+write, the second operation is a read, and the second operation reads the
+value written by the first operation.
+_From-reads_ is a relation between operations, where the first operation is a
+read, the second operation is a write, and the first operation reads a value
+written earlier than the second operation in the second operation's scoped
+modification order (or the first operation reads from the initial value, and
+the second operation is any write to the same locations).
+
+Then the implementation must: guarantee that no cycles exist in the union of
+the following relations:
+
+  * location-ordered
+  * scoped modification order (over all atomic writes)
+  * reads-from
+  * from-reads
+
+NOTE: This is a "consistency" axiom, which informally guarantees that
+sequences of operations can't violate causality.
+
 [[memory-model-scoped-modification-order-coherence]]
-== Scoped Modification Order Coherence
+=== Scoped Modification Order Coherence
 
-Let A and B be mutually-ordered atomic operations, where A happens-before B,
-and let O be A's scoped modification order.
-Then:
+Let A and B be mutually-ordered atomic operations, where A is
+location-ordered before B.
+Then the following rules are a consequence of acyclicity:
 
-  * If A and B are both writes, then A must: be earlier than B in O
-  * If A and B are both reads, then the write that A takes its value from
-    must: be earlier in O than (or the same as) the write that B takes its
-    value from
+  * If A and B are both reads and A does not read the initial value, then the
+    write that A takes its value from must: be earlier in its own scoped
+    modification order than (or the same as) the write that B takes its value
+    from (no cycles between location-order, reads-from, and from-reads).
+  * If A is a read and B is a write and A does not read the initial value,
+    then A must: take its value from a write earlier than B in B's scoped
+    modification order (no cycles between location-order, scope modification
+    order, and reads-from).
   * If A is a write and B is a read, then B must: take its value from A or a
-    write later than A in O
-  * If A is a read and B is a write, then A must: take its value from a
-    write earlier than B in O
+    write later than A in A's scoped modification order (no cycles between
+    location-order, scoped modification order, and from-reads).
+  * If A and B are both writes, then A must: be earlier than B in A's scoped
+    modification order (no cycles between location-order and scoped
+    modification order).
+  * If A is a write and B is a read-modify-write and B reads the value
+    written by A, then B comes immediately after A in A's scoped modification
+    order (no cycles between scoped modification order and from-reads).
 
 [[memory-model-shader-io]]
 == Shader I/O