[PATCH 2/2] BPF: Fix overlapping-address ordering

[Andrea Parri]

Signed-off-by: Andrea Parri <parri.andrea@xxxxxxxxx>
---
 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