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: <d8aa61a8-e2fc-7668-9845-81664c9d181f@huaweicloud.com>
Date: Fri, 25 Oct 2024 15:28:17 +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: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.

Hernan