| 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
| ||
|
Message-ID: <ZzT9NR7mlSZQHzpD@andrea>
Date: Wed, 13 Nov 2024 21:25:41 +0200
From: Andrea Parri <parri.andrea@...il.com>
To: "Paul E. McKenney" <paulmck@...nel.org>
Cc: puranjay@...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
[...]
> I guess the next question (once clarified the intentions for the R
> and Z6.3 tests seen earlier) is "Does BPF really care about 2+2W
> and B-cumulativity for store-release?"; I mentioned some tradeoff,
> but in the end this is a call for the BPF community.
Interpreting the radio silence as an unanimous "No, it doesn't", please find
tentative fixes/patch (on top of the bpf_acquire_release branch cited in an
earlier post) at the bottom of this email.
While testing the changes in question, I noticed an (unrelated) omission in
the current PPO relation; the second patch below addresses that.
Both patches were tested using the "BPF catalogue" available in the tree at
stake: as expected, the only differences in outcomes were for the new/added
five tests.
Please use and integrate according to your preference, any feedback welcome.
Andrea
>From 5bf399413578b6a94c42f6367245be2bdbf58926 Mon Sep 17 00:00:00 2001
From: Andrea Parri <parri.andrea@...il.com>
Date: Mon, 11 Nov 2024 08:38:42 +0200
Subject: [PATCH 1/2] BPF: Fix propagation ordering, after LKMM
Signed-off-by: Andrea Parri <parri.andrea@...il.com>
---
catalogue/bpf/tests/2+2W+release+fence.litmus | 15 ++++++++++++
.../tests/ISA2+release+acquire+acquire.litmus | 15 ++++++++++++
catalogue/bpf/tests/R+release+fence.litmus | 14 +++++++++++
.../bpf/tests/Z6.3+fence+fence+acquire.litmus | 16 +++++++++++++
herd/libdir/bpf.cat | 24 +++++++++----------
5 files changed, 72 insertions(+), 12 deletions(-)
create mode 100644 catalogue/bpf/tests/2+2W+release+fence.litmus
create mode 100644 catalogue/bpf/tests/ISA2+release+acquire+acquire.litmus
create mode 100644 catalogue/bpf/tests/R+release+fence.litmus
create mode 100644 catalogue/bpf/tests/Z6.3+fence+fence+acquire.litmus
diff --git a/catalogue/bpf/tests/2+2W+release+fence.litmus b/catalogue/bpf/tests/2+2W+release+fence.litmus
new file mode 100644
index 0000000000000..0f88babbf27de
--- /dev/null
+++ b/catalogue/bpf/tests/2+2W+release+fence.litmus
@@ -0,0 +1,15 @@
+BPF 2+2W+release+fence
+(*
+ * Result: Sometimes
+ *)
+{
+ 0:r2=x; 0:r4=y;
+ 1:r2=y; 1:r4=x; 1:r6=l;
+}
+ P0 | P1 ;
+ r1 = 1 | r1 = 1 ;
+ *(u32 *)(r2 + 0) = r1 | *(u32 *)(r2 + 0) = r1 ;
+ r3 = 2 | r5 = atomic_fetch_add((u32 *)(r6 + 0), r5) ;
+ store_release((u32 *)(r4 + 0), r3) | r3 = 2 ;
+ | *(u32 *)(r4 + 0) = r3 ;
+exists ([x]=1 /\ [y]=1)
diff --git a/catalogue/bpf/tests/ISA2+release+acquire+acquire.litmus b/catalogue/bpf/tests/ISA2+release+acquire+acquire.litmus
new file mode 100644
index 0000000000000..44c1308d70b5a
--- /dev/null
+++ b/catalogue/bpf/tests/ISA2+release+acquire+acquire.litmus
@@ -0,0 +1,15 @@
+BPF ISA2+release+acquire+acquire
+(*
+ * Result: Sometimes
+ *)
+{
+ 0:r2=x; 0:r4=y;
+ 1:r2=y; 1:r4=z;
+ 2:r2=z; 2:r4=x;
+}
+ P0 | P1 | P2 ;
+ r1 = 1 | r1 = load_acquire((u32 *)(r2 + 0)) | r1 = load_acquire((u32 *)(r2 + 0)) ;
+ *(u32 *)(r2 + 0) = r1 | r3 = 1 | r3 = *(u32 *)(r4 + 0) ;
+ r3 = 1 | *(u32 *)(r4 + 0) = r3 | ;
+ store_release((u32 *)(r4 + 0), r3) | | ;
+exists (1:r1=1 /\ 2:r1=1 /\ 2:r3=0)
diff --git a/catalogue/bpf/tests/R+release+fence.litmus b/catalogue/bpf/tests/R+release+fence.litmus
new file mode 100644
index 0000000000000..a0bcbe0bbb804
--- /dev/null
+++ b/catalogue/bpf/tests/R+release+fence.litmus
@@ -0,0 +1,14 @@
+BPF R+release+fence
+(*
+ * Result: Sometimes
+ *)
+{
+ 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)
diff --git a/catalogue/bpf/tests/Z6.3+fence+fence+acquire.litmus b/catalogue/bpf/tests/Z6.3+fence+fence+acquire.litmus
new file mode 100644
index 0000000000000..67e9146bcef2b
--- /dev/null
+++ b/catalogue/bpf/tests/Z6.3+fence+fence+acquire.litmus
@@ -0,0 +1,16 @@
+BPF Z6.3+fence+fence+acquire
+(*
+ * Result: Never
+ *)
+{
+ 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)
diff --git a/herd/libdir/bpf.cat b/herd/libdir/bpf.cat
index 28b42497ea0fc..7803a1e818de7 100644
--- a/herd/libdir/bpf.cat
+++ b/herd/libdir/bpf.cat
@@ -43,9 +43,9 @@ show addr_dep as addr
show data_dep as data
show ctrl_dep as ctrl
-(*************)
-(* ppo rules *)
-(*************)
+(**********************)
+(* ppo and prop rules *)
+(**********************)
let ppo =
(* Explicit synchronization *)
@@ -65,6 +65,10 @@ include "cos-opt.cat"
let com = co | rf | fr
+(* Propagation ordering from SC and release operations *)
+let A-cumul = rfe? ; (po_amo_fetch | store_release)
+let prop = (coe | fre)? ; A-cumul* ; rfe?
+
(**********)
(* Axioms *)
(**********)
@@ -72,17 +76,13 @@ let com = co | rf | fr
(* Sc per location *)
acyclic com | po-loc as Coherence
-(* No thin air *)
-let hb = (ppo | rfe)+
-acyclic hb
+(* No-Thin-Air and Observation *)
+let hb = ppo | rfe | ((prop \ id) & int)
+acyclic hb as Happens-before
(* Propagation *)
-let A-cumul = rfe;po_amo_fetch | rfe;store_release | po_amo_fetch;fre
-let prop = (store_release | po_amo_fetch | A-cumul);hb*
-acyclic prop | co
-
-(* Observation *)
-irreflexive fre;prop
+let pb = prop ; po_amo_fetch ; hb*
+acyclic pb as Propagation
(* Atomicity *)
empty rmw & (fre;coe) as Atomic
--
2.43.0
>From 84520eaacbcb399b5cc7b4cbe0f716ad84e87824 Mon Sep 17 00:00:00 2001
From: Andrea Parri <parri.andrea@...il.com>
Date: Mon, 11 Nov 2024 08:03:48 +0200
Subject: [PATCH 2/2] BPF: Fix overlapping-address ordering
Signed-off-by: Andrea Parri <parri.andrea@...il.com>
---
catalogue/bpf/tests/LB+release-oa+acquire.litmus | 15 +++++++++++++++
herd/libdir/bpf.cat | 13 ++++++-------
2 files changed, 21 insertions(+), 7 deletions(-)
create mode 100644 catalogue/bpf/tests/LB+release-oa+acquire.litmus
diff --git a/catalogue/bpf/tests/LB+release-oa+acquire.litmus b/catalogue/bpf/tests/LB+release-oa+acquire.litmus
new file mode 100644
index 0000000000000..1544179357e9b
--- /dev/null
+++ b/catalogue/bpf/tests/LB+release-oa+acquire.litmus
@@ -0,0 +1,15 @@
+BPF LB+release-oa+acquire
+(*
+ * Result: Never
+ *)
+{
+ 0:r2=x; 0:r4=y;
+ 1:r2=y; 1:r4=x;
+}
+ P0 | P1 ;
+ r1 = *(u32 *)(r2 + 0) | r1 = load_acquire((u32 *)(r2 + 0)) ;
+ r3 = 1 | r3 = 1 ;
+ store_release((u32 *)(r4 + 0), r3) | *(u32 *)(r4 + 0) = r3 ;
+ r5 = 2 | ;
+ *(u32 *)(r4 + 0) = r5 | ;
+exists (0:r1=1 /\ 1:r1=2)
diff --git a/herd/libdir/bpf.cat b/herd/libdir/bpf.cat
index 7803a1e818de7..4917d0f77009f 100644
--- a/herd/libdir/bpf.cat
+++ b/herd/libdir/bpf.cat
@@ -47,6 +47,10 @@ show ctrl_dep as ctrl
(* ppo and prop rules *)
(**********************)
+(* Compute coherence relation *)
+include "cos-opt.cat"
+let com = co | rf | fr
+
let ppo =
(* Explicit synchronization *)
po_amo_fetch | rcpc
@@ -57,13 +61,8 @@ let ppo =
(* Pipeline Dependencies *)
| [M];(addr|data);[W];rfi;[R]
| [M];addr;[M];po;[W]
-(* Successful cmpxchg R -(M)> W *)
-| rmw
-
-(* Compute coherence relation *)
-include "cos-opt.cat"
-
-let com = co | rf | fr
+(* Overlapping-address ordering *)
+| (coi | fri)
(* Propagation ordering from SC and release operations *)
let A-cumul = rfe? ; (po_amo_fetch | store_release)
--
2.43.0
Powered by blists - more mailing lists