From: Hernan Ponce de Leon <hernan.poncedeleon@huaweicloud.com>
To: Andrea Parri <parri.andrea@gmail.com>
Cc: puranjay@kernel.org, paulmck@kernel.org, bpf@vger.kernel.org,
lkmm@lists.linux.dev, linux-kernel@vger.kernel.org
Subject: Re: Some observations (results) on BPF acquire and release
Date: Fri, 25 Oct 2024 15:57:29 +0200 [thread overview]
Message-ID: <8360f999-0d64-3b4f-e4b8-8c84f7311af2@huaweicloud.com> (raw)
In-Reply-To: <ZxugzP0yB3zeqKSn@andrea>
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
next prev parent reply other threads:[~2024-10-25 13:57 UTC|newest]
Thread overview: 19+ messages / expand[flat|nested] mbox.gz Atom feed top
2024-10-23 17:47 Some observations (results) on BPF acquire and release Andrea Parri
2024-10-24 4:25 ` Paul E. McKenney
2024-10-24 11:13 ` Andrea Parri
2024-10-25 13:56 ` Andrea Parri
2024-11-13 19:25 ` Andrea Parri
2024-11-13 22:59 ` Puranjay Mohan
2024-11-14 14:56 ` Andrea Parri
2024-10-24 11:44 ` Jonas Oberhauser
2024-10-24 12:11 ` Puranjay Mohan
2024-10-24 12:21 ` Jonas Oberhauser
2024-10-24 14:42 ` Paul E. McKenney
2024-10-25 9:32 ` Hernan Ponce de Leon
2024-10-25 13:15 ` Andrea Parri
2024-10-25 13:28 ` Hernan Ponce de Leon
2024-10-25 13:44 ` Andrea Parri
2024-10-25 13:57 ` Hernan Ponce de Leon [this message]
2024-10-25 14:27 ` Andrea Parri
2024-10-25 15:00 ` Hernan Ponce de Leon
2024-10-25 23:26 ` Paul E. McKenney
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=8360f999-0d64-3b4f-e4b8-8c84f7311af2@huaweicloud.com \
--to=hernan.poncedeleon@huaweicloud.com \
--cc=bpf@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=lkmm@lists.linux.dev \
--cc=parri.andrea@gmail.com \
--cc=paulmck@kernel.org \
--cc=puranjay@kernel.org \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).