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