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
