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

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