Does visible-to apply to atomic reads?

[RobinMorisset]

The spec just says: If X is visible-to Y, then Y reads the value written by X for locations M2. But the formal model has (in the predicate "consistent[X]"): // consistency: non-atomic reads must read-from a value that is still visible X.rf . (stor[X.R-X.A]) in imm[(stor[X.W]) . (X.locord)] which restricts this rule to only non-atomic reads.

Is there a reason for the discrepancy?

On a related note, the formal model defines: // visible to = location ordered W->R with no intervening write (W->W->R) visto = imm[(stor[W]) . locord] . (stor[R]) But then never uses it (except in AssertVisTo). Why not use it in the consistency predicate above?

[jeffbolznv]

This and issue #7 are intertwined. IIRC the "R-A" came from rule 30 in https://johnwickerson.github.io/papers/memalloy.pdf. If I try to change it to "R", things break because locord doesn't relate all atomic reads (because asmo doesn't relate atomic reads). I think it was intentional for asmo to only include writes (modifications), and we just need to clarify that in the spec. But I need more time to think about this.

[jeffbolznv]

Robin, it's not clear to me that anything is actually wrong here, or what edit to make to make things more clear.

The sentence "If X is visible-to Y, then Y reads the value written by X for locations M2" can apply to atomics, i.e. atomics can be location-ordered if they are explicitly synchronized by other operations, but atomics need not be location-ordered. And similarly the rule "X.rf . (stor[X.R-X.A]) in imm[(stor[X.W]) . (X.locord)]" excludes atomics because they need not be location-ordered.

Do you have any specific suggestions for how to clarify this?

Having thought about this, now I'm wondering if we should delete the "asmo + // mutually-atomic case" line from locord (and the corresponding line from the spec), since it only relates writes to writes and is unnecessary and possibly misleading. That would remove a possible source of confusion suggesting that atomic reads must be location ordered.

[RobinMorisset]

My problem is that I see nothing directly in the formal model that matches "If X is visible-to Y, then Y reads the value written by X for locations M2" for atomics. I think it is covered by your stronger consistency axiom: is_acyclic[X.locord + X.rf + X.fr + X.asmo], but am not entirely sure of it.

Ideally I would like this sentence in the spec to be explicitly only about non-atomics, and then to have a section about your consistency axiom (per https://github.com/KhronosGroup/Vulkan-MemoryModel/issues/13) replacing the Scoped Modification Order Coherence section.

Currently, I don't know if the spec is wrong, if the model is wrong or if both are right but the equivalence is merely hard to see.

About removing the "asmo + // mutually-atomic case" line from locord, I first thought it would be wrong because it would reduce locord in X.rf . (stor[X.R-X.A]) in imm[(stor[X.W]) . (X.locord)], but every attempt to build a counter-example hit your other consistency axiom, so I tentatively believe it safe now.

[jeffbolznv]

I've pushed the changes to remove asmo from locord at https://github.com/KhronosGroup/Vulkan-MemoryModel/pull/17 and https://github.com/KhronosGroup/Vulkan-Docs/pull/924. I've also started writing the consistency language in the spec (not yet pushed).

[jeffbolznv]

Closing as fixed by https://github.com/KhronosGroup/Vulkan-MemoryModel/pull/17 (and https://github.com/KhronosGroup/Vulkan-Docs/pull/924)