On 10/25/2024 3:44 PM, Andrea Parri wrote:
On Fri, Oct 25, 2024 at 03:28:17PM +0200, Hernan Ponce de Leon wrote:
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.
FWIW, a comprehensive collection of PPC litmus tests could be found at
https://www.cl.cam.ac.uk/~pes20/ppc-supplemental/ppc002.html
(just follow the link on the test pattern/variants to see the sources);
be aware the results of those tables date back to the PPC paper though.
Alternatively, remind that PPC is well supported by the herdtools7 diy7
generator; I see no reason for having to (re)write such tests manually.
Andrea
I am particularly interested in tests using lwarx and stwcx instructions
(this is what I understood would be used if one follows [1] to compile
the tests in this thread).
I have not yet check the cambridge website, but due to the timeline, I
don't expect to find tests with those instructions. The same is true
with [2].
I have limited experience with diy7, but I remember that it had some
limitations to generate RMW instructions, at least for C [3].
Hernan
[1]
https://github.com/torvalds/linux/blob/master/arch/powerpc/net/bpf_jit_comp32.c
[2]
https://github.com/herd/herdtools7/tree/master/catalogue/herding-cats/ppc/tests/campaign
[3] https://github.com/herd/herdtools7/issues/905
