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
