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: <8360f999-0d64-3b4f-e4b8-8c84f7311af2@huaweicloud.com>
Date: Fri, 25 Oct 2024 15:57:29 +0200
From: Hernan Ponce de Leon <hernan.poncedeleon@...weicloud.com>
To: Andrea Parri <parri.andrea@...il.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

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