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
