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

lists.openwall.net		lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC
Open Source and information security mailing list archives

Hash Suite: Windows password security audit tool. GUI, reports in PDF.

[<prev] [next>] [<thread-prev] [day] [month] [year] [list]

Message-ID: <43ecbb1e-7710-45ab-891e-575b6f562794@paulmck-laptop>
Date: Fri, 25 Oct 2024 16:26:49 -0700
From: "Paul E. McKenney" <paulmck@...nel.org>
To: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>
Cc: Andrea Parri <parri.andrea@...il.com>, puranjay@...nel.org,
	bpf@...r.kernel.org, lkmm@...ts.linux.dev,
	linux-kernel@...r.kernel.org
Subject: Re: Some observations (results) on BPF acquire and release

On Fri, Oct 25, 2024 at 03:57:29PM +0200, Hernan Ponce de Leon wrote:
> 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

Please see attached for a tarball of random PPC litmus tests.

You asked for this!  ;-)

							Thanx, Paul