Re: Some observations (results) on BPF acquire and release

[Andrea Parri <parri.andrea@gmail.com>]

[...]

> 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@gmail.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@gmail.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@gmail.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@gmail.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