Re: Some observations (results) on BPF acquire and release

[Hernan Ponce de Leon]

On 10/25/2024 3:15 PM, Andrea Parri wrote:
> > > BPF R+release+fence
> > > {
> > >    0:r2=x; 0:r4=y;
> > >    1:r2=y; 1:r4=x; 1:r6=l;
> > > }
> > >    P0                                 | P1                                         ;
> > >    r1 = 1                             | r1 = 2                                     ;
> > >    *(u32 *)(r2 + 0) = r1              | *(u32 *)(r2 + 0) = r1                      ;
> > >    r3 = 1                             | r5 = atomic_fetch_add((u32 *)(r6 + 0), r5) ;
> > >    store_release((u32 *)(r4 + 0), r3) | r3 = *(u32 *)(r4 + 0)                      ;
> > > exists ([y]=2 /\ 1:r3=0)
> > >
> > > This "exists" condition is not satisfiable according to the BPF model;
> > > however, if we adopt the "natural"/intended(?) PowerPC implementations
> > > of the synchronization primitives above (aka, with store_release() -->
> > > LWSYNC and atomic_fetch_add() --> SYNC ; [...] ), then we see that the
> > > condition in question becomes (architecturally) satisfiable on PowerPC
> > > (although I'm not aware of actual observations on PowerPC hardware).
> >
> > Are the resulting PPC tests available somewhere?
>
> My data go back to the LKMM paper, cf. e.g. the R+pooncerelease+fencembonceonce
> entry at https://diy.inria.fr/linux/hard.html#unseen .
>
>    Andrea

I guess I understood you wrong. I thought you had manually "compiled" 
those to PPC litmus format (i.e., doing exactly what the JIT compiler 
would do). I can obviously write them manually myself, but I find this 
painful and error prone (I am particularly bad at this task), so I 
wanted to avoid this if someone else had already done it.

Hernan