Add coherence tests

Co-authored-by: Hernan Ponce de Leon <hernanl.leon@huawei.com>
NVlabs · Oct 30, 2023 · 970b231 · 970b231
1 parent fc4f786
commit 970b231
Show file tree

Hide file tree

Showing 2 changed files with 44 additions and 0 deletions.
diff --git a/tests/Manual/Coherence-weak.test b/tests/Manual/Coherence-weak.test
@@ -0,0 +1,22 @@
+// Test if t2 and t3 can read updates to x in conflicting order
+.global x;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+}
+
+d0.b0.t1 {
+  st.weak [x], 2;
+}
+
+d0.b0.t2 {
+  ld.acquire.sys r0, [x];
+  ld.acquire.sys r1, [x];
+}
+
+d0.b0.t3 {
+  ld.acquire.sys r2, [x];
+  ld.acquire.sys r3, [x];
+}
+
+permit(r0 == 1 && r1 == 2 && r2 == 2 && r3 == 1) as coherence_weak;
diff --git a/tests/Manual/Coherence.test b/tests/Manual/Coherence.test
@@ -0,0 +1,22 @@
+// Test if t2 and t3 can read updates to x in conflicting order
+.global x;
+
+d0.b0.t0 {
+  st.relaxed.sys [x], 1;
+}
+
+d0.b0.t1 {
+  st.relaxed.sys [x], 2;
+}
+
+d0.b0.t2 {
+  ld.acquire.sys r0, [x];
+  ld.acquire.sys r1, [x];
+}
+
+d0.b0.t3 {
+  ld.acquire.sys r2, [x];
+  ld.acquire.sys r3, [x];
+}
+
+assert(r0 != 1 || r1 != 2 || r2 != 2 || r3 != 1) as coherence;