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] [thread-next>] [day] [month] [year] [list]

Message-ID: <ZxuZ-wGccb3yhBAD@andrea>
Date: Fri, 25 Oct 2024 16:15:51 +0300
From: Andrea Parri <parri.andrea@...il.com>
To: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>
Cc: puranjay@...nel.org, paulmck@...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

> > 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