Am 5/2/2024 um 1:21 AM schrieb Paul E. McKenney:
This commit adds four litmus tests showing that a failing cmpxchg()
operation is unordered unless followed by an smp_mb__after_atomic()
operation.
So far, my understanding was that all RMW operations without suffix
(xchg(), cmpxchg(), ...) will be interpreted as F[Mb];...;F[Mb].
I guess this shows again how important it is to model these full
barriers explicitly inside the cat model, instead of relying on implicit
conversions internal to herd.
I'd like to propose a patch to this effect.
What is the intended behavior of a failed cmpxchg()? Is it the same as a
relaxed one?
My suggestion would be in the direction of marking read and write events
of these operations as Mb, and then defining
(* full barrier events that appear in non-failing RMW *)
let RMW_MB = Mb & (dom(rmw) | range(rmw))
let mb =
[M] ; fencerel(Mb) ; [M]
| [M] ; (po \ si ; rmw) ; [RMW_MB] ; po^? ; [M]
| [M] ; po^? ; [RMW_MB] ; (po \ rmw ; si) ; [M]
| ...
The po \ si;rmw is because ordering is not provided internally of the
rmw, although I suspect that after we added release sequences it could
perhaps be simplified to
let mb =
[M] ; fencerel(Mb) ; [M]
| [M] ; po ; [RMW_MB] ; po^? ; [M]
| [M] ; po^? ; [RMW_MB] ; po ; [M]
| ...
or
let mb =
[M] ; fencerel(Mb) ; [M]
| [M] ; po & (po^? ; [RMW_MB] ; po^?) ; [M]
| ...
(the po & is necessary to avoid trivial hb cycles of an RMW event
happening before itself)
Any interest?
Have fun,
jonas
