RMW atomicity is broken

[hernanponcedeleon]

We are getting some counter intuitive behaviors related to non-atomic accesses and rmw. Consider this example

// Both read-modify-write instructions read the value stored by a non-atomic write instruction preceding the barrier. NEWWG NEWSG NEWTHREAD st.av.scopewg.sc1 x = 1 cbar.acq.rel.scopewg.semsc1 0 rmw.scopewg.sc1 x = 1 2 NEWSG NEWTHREAD cbar.acq.rel.scopewg.semsc1 0 rmw.scopewg.sc1 x = 1 2 SATISFIABLE consistent[X] && #dr=0 NOSOLUTION consistent[X] && #dr>0

This clearly violates atomicity, but the current model allows the behavior.

We have tried to add more semantics, but it does not help

NEWWG NEWSG NEWTHREAD st.av.scopewg.sc1 x = 1 cbar.acq.rel.scopewg.semsc1.semav.semvis 0 rmw.acq.rel.scopewg.sc1.semsc1.semav.semvis x = 1 2 NEWSG NEWTHREAD cbar.acq.rel.scopewg.semsc1.semav.semvis 0 rmw.acq.rel.scopewg.sc1.semsc1.semav.semvis x = 1 2 SATISFIABLE consistent[X] && #dr=0 NOSOLUTION consistent[X] && #dr>0

If we make the store an atomic one, the behavior is forbidden.

@jeffbolznv any thoughts?

[jeffbolznv]

Hi,

I think this is a limitation/bug in how litmus.cpp is generating the alloy test. It looks at the read and write values to generate rf:

    (E0->E2) in X.rf
    (E0->E4) in X.rf

but it probably also needs to do something to restrict what's in asmo based on those values, e.g.:

    no ((E2->E4)+(E4->E2)) & X.asmo

[natgavrilenko]

Hi,

I think that adding "no ((E2->E4)+(E4->E2)) & X.asmo" will also forbid legal behaviors, because it disallows all "asmo" edges between E2 and E4. For example, if we modify the test such that E4 reads from E2 (legal behavior), then adding "no ((E2->E4)+(E4->E2)) & X.asmo" will make this test also unsatisfiable.

NEWWG NEWSG NEWTHREAD st.av.scopewg.sc1 x = 1 cbar.acq.rel.scopewg.semsc1.semav.semvis 0 rmw.acq.rel.scopewg.sc1.semsc1.semav.semvis x = 1 2 NEWSG NEWTHREAD cbar.acq.rel.scopewg.semsc1.semav.semvis 0 rmw.acq.rel.scopewg.sc1.semsc1.semav.semvis x = 2 3 SATISFIABLE consistent[X] && #dr=0 NOSOLUTION consistent[X] && #dr>0

We have an impression that it is a part of a bigger problem that non-atomic writes are not strong enough, when they are ordered by release-acquire synchronization or by a barrier. Here is another example that is allowed by the model, while we think that it should be forbidden.

NEWWG NEWSG NEWTHREAD st.av.scopedev.sc0 x = 1 st.atom.rel.scopedev.sc0.semsc0.semav x = 2 NEWSG NEWTHREAD ld.atom.acq.scopedev.sc0.semsc0.semvis x = 2 ld.atom.scopedev.sc0 x = 1 SATISFIABLE consistent[X]

We think that the problem might be that the definition of "fr" relation doesn't consider ordering of non-atomic writes.

Currently, the model defines "fr" as: fr = (~rf . asmo) + ((stor[RFINIT]) . sloc . (stor[W])) - iden

Adding locord: fr = (~rf . ((W -> W) & locord)) + (~rf . asmo) + ((stor[RFINIT]) . sloc . (stor[W])) - iden

With the new definition of "fr", we get expected results for all the three tests in this issue. We also get correct results for all other tests in the repo.

What is your opinion about this?

[hernanponcedeleon]

This is my reasoning of why the fix proposed by Natalia is correct.

Traditionally, whenever a load r gets its value from memory, and later a store w overrides this value, fr is used to model that r should be ordered before w. In the current model this is not guaranteed if any of the two stores (w or the previous one that put in memory the value in question) is non-atomic. The proposed change fixes this by also considering any case where both stores access the same location and are ordered (via locord).

[jeffbolznv]

I think I agree with the proposed change. Looking back at https://johnwickerson.github.io/papers/memalloy.pdf which the model is based on, from-read (definition 6) has fr = ~rf . co ... and I had translated co to asmo, but that's probably too strict and doesn't handle this situation of mixing atomics and non-atomics.

I've asked the group to review, but it being summertime it may be a while before we're all in the same meeting. It would be great to have a pull request with the change and these test cases.

[hernanponcedeleon]

@jeffbolznv I just noticed that the natural language spec also needs to be update since currently it states

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).

I am planning to open a PR the doc repo. Do you think the following wording would be appropriated based on the changes to the formal model (changes are in bold)?

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 location order (or the first operation reads from the initial value, and the second operation is any write to the same locations).

[jeffbolznv]

Hi,

Sorry for the delay. The Memory Model TSG has started meeting again after a summer break, and folks are going to look at this in more detail soon.

Do you think the following wording would be appropriated based on the changes to the formal model (changes are in bold)?

Yes, this LGTM.