Re: [PATCH memory-model 2/4] Documentation/litmus-tests: Demonstrate unordered failing cmpxchg

[Jonas Oberhauser <jonas.oberhauser@huaweicloud.com>]

Am 5/6/2024 um 12:05 PM schrieb Jonas Oberhauser:
> 
> 
> 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 \ rmw) ; [RMW_MB] ; po^? ; [M]
>    | [M] ; po^? ; [RMW_MB] ; (po \ rmw) ; [M]
>    | ...
> 
> The po \ rmw is because ordering is not provided internally of the 
> rmw

(removed the unnecessary si since LKMM is still non-mixed-accesses)


This could also be written with a single rule:

      | [M] ; (po \ rmw) & (po^?; [RMW_MB] ; po^?) ; [M]


> I suspect that after we added [rmw] sequences it could 
> perhaps be simplified [...]
> 

No, my suspicion is wrong - this would incorrectly let full-barrier RMWs
act like strong fences when they appear in an rmw sequence.

  if (z==1)  ||  x = 2;     ||  xchg(&y,2)  || if (y==2)
    x = 1;   ||  y =_rel 1; ||              ||    z=1;


right now, we allow x=2 overwriting x=1 (in case the last thread does 
not propagate x=2 along with z=1) because on power, the xchg might be
implemented with a sync that doesn't get executed until the very end
of the program run.


Instead of its negative form (everything other than inside the rmw),
it could also be rewritten positively. Here's a somewhat short form:

let mb =
      [M] ; fencerel(Mb) ; [M]
    (* everything across a full barrier RMW is ordered. This includes up 
to one event inside the RMW. *)
    | [M] ; po ; [RMW_MB] ; po ; [M]
    (* full barrier RMW writes are ordered with everything behind the RMW *)
    | [W & RMW_MB] ; po ; [M]
    (* full barrier RMW reads are ordered with everything before the RMW *)
    | [M] ; po ; [R & RMW_MB]
    | ...



Good luck,
jonas