Discrepancy in the coherency/consistency predicates

[RobinMorisset]

The specification has the following section:

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:

• 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 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

while the formal model has the following:

// consistency: locord, rf, fr, asmo must not form cycles is_acyclic[X.locord + X.rf + X.fr + X.asmo]

These two things appear to be intended to match each other, but it is not obvious at all that they do.

I actually believe that they don't, in that the consistency predicate seems significantly stronger, especially considering that hb is not transitive in this model (contrary to C11 without consume whose formalization in https://johnwickerson.github.io/papers/memalloy.pdf inspired this rule) so preventing cycles in hb + asmo is for example stronger than the first bullet in the spec. However, I have not yet managed to find a litmus test that makes the difference between the two clear. I plan on updating this issue once I find one. I am posting now as suggested in https://github.com/KhronosGroup/Vulkan-MemoryModel/issues/1 in case anyone has some insight in this problem.

[jeffbolznv]

Hmm, the consistency rule is essentially an axiom, so maybe the right thing to do is to state it as such in the spec text, and then maybe(?) the Scoped Modification Order Coherence rules could be treated as a consequence of that axiom? Just a thought, I haven't fully digested this issue yet. It's not clear to me that the Scoped Modification Order Coherence rules on their own are useful, I had included them mostly because they are in the C++ spec.

Also, I had started writing litmus tests for the Scoped Modification Order Coherence rules a few weeks ago but haven't had time to finish. I'll try to wrap that up soon.

[RobinMorisset]

Quick update: There are two equivalent ways of presenting the C++ coherency rules, either as a group of 7 axioms (4 of which are similar to the Scoped Modification Order Coherence), or as a single acyclicity condition similar to the one in the consistency axiom (I had forgotten this equivalence and had to look it up).

However, I still think the formal model and the spec should be brought in sync, for two reasons:

• First, the spec does not have all of the requisites axiom from C++, most noticeably missing the requirement that RMW be atomic: "∀(a, b)∈rf . is atomic rmw b → adjacent_less_than mo actions a b" (in Mark Batty's Lem model of C++11). This causes the test releaseseq1.test to fail when the acyclicity axiom is replaced by a straightforward translation of the Scoped Memory Order Coherency section of the spec.
• Second it is not obvious that the equivalence proof which was written for C++ without consume applies to Vulkhan. Two points that make me doubt it are the fact that asmo is significantly more restricted than mo, in particular not being a total order on all writes to a location, and the fact hb is not transitive in Vulkhan (to the best of my knowledge, the proof was only done for C++ without consume, precisely because this is what makes hb transitive).

[jeffbolznv]

I've created https://github.com/KhronosGroup/Vulkan-Docs/pull/927 for this. This is all subtle enough that I'd appreciate some detailed review, and no need to rush this into the spec.

[jeffbolznv]

Closing as fixed now that https://github.com/KhronosGroup/Vulkan-Docs/pull/927 is merged.