From: "Paul E. McKenney" <paulmck@kernel.org>
To: Andrea Parri <parri.andrea@gmail.com>
Cc: puranjay@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: Wed, 23 Oct 2024 21:25:40 -0700 [thread overview]
Message-ID: <13f60db0-b334-4638-a768-d828ecf7c8d0@paulmck-laptop> (raw)
In-Reply-To: <Zxk2wNs4sxEIg-4d@andrea>
On Wed, Oct 23, 2024 at 08:47:44PM +0300, Andrea Parri wrote:
> Hi Puranjay and Paul,
>
> I'm running some experiment on the (experimental) formalization of BPF
> acquire and release available from [1] and wanted to report about some
> (initial) observations for discussion and possibly future developments;
> apologies in advance for the relatively long email and any repetition.
>
>
> A first and probably most important observation is that the (current)
> formalization of acquire and release appears to be "too strong": IIUC,
> the simplest example/illustration for this is given by the following
>
> 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).
Yes, you are quite right, for efficient use on PowerPC, we need the BPF
memory model to allow the above cycle in the R litmus test. My bad,
as I put too much emphasis on ARM64.
> At first, the previous observation (validated via simulations and later
> extended to similar but more complex scenarios ) made me believe that
> the BPF formalization of acquire and release could be strictly stronger
> than the corresponding LKMM formalization; but that is _not_ the case:
>
> The following "exists" condition is satisfiable according to the BPF
> model (and it remains satisfiable even if the load_acquire() in P2 is
> paired with an additional store_release() in P1). In contrast, the
> corresponding LKMM condition (e.g load_acquire() --> smp_load_acquire()
> and atomic_fetch_add() --> smp_mb()) is not satisfiable (in fact, the
> same conclusion holds even if the putative smp_load_acquire() in P2 is
> "replaced" with an smp_rmb() or with an address dependency).
>
> BPF Z6.3+fence+fence+acquire
> {
> 0:r2=x; 0:r4=y; 0:r6=l;
> 1:r2=y; 1:r4=z; 1:r6=m;
> 2:r2=z; 2:r4=x;
> }
> P0 | P1 | P2 ;
> r1 = 1 | r1 = 2 | r1 = load_acquire((u32 *)(r2 + 0)) ;
> *(u32 *)(r2 + 0) = r1 | *(u32 *)(r2 + 0) = r1 | r3 = *(u32 *)(r4 + 0) ;
> r5 = atomic_fetch_add((u32 *)(r6 + 0), r5) | r5 = atomic_fetch_add((u32 *)(r6 + 0), r5) | ;
> r3 = 1 | r3 = 1 | ;
> *(u32 *)(r4 + 0) = r3 | *(u32 *)(r4 + 0) = r3 | ;
> exists ([y]=2 /\ 2:r1=1 /\ 2:r3=0)
And again agreed, we do want to forbid Z6.3.
> These remarks show that the proposed BPF formalization of acquire and
> release somehow, but substantially, diverged from the corresponding
> LKMM formalization. My guess is that the divergences mentioned above
> were not (fully) intentional, or I'm wondering -- why not follow the
> latter (the LKMM's) more closely? - This is probably the first question
> I would need to clarify before trying/suggesting modifications to the
> present formalizations. ;-) Thoughts?
Thank you for digging into this!
I clearly need to get my validation work going again, but I very much
welcome any further help you would be willing to provide.
Thanx, Paul
> Andrea
>
>
> [1] https://github.com/puranjaymohan/herdtools7/commits/bpf_acquire_release/
next prev parent reply other threads:[~2024-10-24 4:25 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 [this message]
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
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=13f60db0-b334-4638-a768-d828ecf7c8d0@paulmck-laptop \
--to=paulmck@kernel.org \
--cc=bpf@vger.kernel.org \
--cc=linux-kernel@vger.kernel.org \
--cc=lkmm@lists.linux.dev \
--cc=parri.andrea@gmail.com \
--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).