Add Tests

tests/Manual/Atom-plus-register.test

@@ -0,0 +1,12 @@
+.global x;
+
+d0.b0.t0 {
+  atom.add.acq_rel.cta r0, [x], 1;
+}
+
+d0.b1.t0 {
+  atom.add.acq_rel.cta r1, [x], 1;
+  ld.acquire.cta r2, [x];
+}
+
+permit (r2 == 1) as r2_atom;

tests/Manual/Cause-base-strong.test

@@ -0,0 +1,22 @@
+.global x;
+.global f1;
+.global f2;
+
+d0.b0.t0 {
+  st.release.gpu [x], 1;
+  st.release.sys [f1], 1;
+}
+
+d0.b1.t0 {
+  ld.acquire.gpu r1, [x];
+  st.weak [x], 2;
+  st.release.sys [f2], 1;
+}
+
+d0.b2.t0 {
+  ld.acquire.sys r2, [f2];
+  ld.acquire.sys r3, [f2];
+  ld.weak r4, [x];
+}
+
+assert(r1 != 1 || r2 != 1 || r3 != 1 || r4 != 1) as check_cause_base_strong;

tests/Manual/Cause-base-weak.test

@@ -0,0 +1,22 @@
+.global x;
+.global f1;
+.global f2;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.release.sys [f1], 1;
+}
+
+d0.b1.t0 {
+  ld.acquire.gpu r1, [x];
+  st.weak [x], 2;
+  st.release.sys [f2], 1;
+}
+
+d0.b2.t0 {
+  ld.acquire.sys r2, [f2];
+  ld.acquire.sys r3, [f2];
+  ld.weak r4, [x];
+}
+
+permit(r1 == 1 && r2 == 1 && r3 == 1 && r4 == 1) as check_cause_base_weak;

tests/Manual/Co-Total-3-threads-scope-same.test

@@ -0,0 +1,22 @@
+.global x;
+.global f1;
+.global f2;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.release.sys [f1], 1;
+}
+
+d0.b0.t1 {
+  st.weak [x], 2;
+  st.release.sys [f2], 1;
+}
+
+d0.b0.t2 {
+  ld.acquire.sys r0, [f1];
+  ld.acquire.sys r1, [f2];
+  ld.weak r2, [x];
+  ld.weak r3, [x];
+}
+
+permit(r0 == 1 && r1 == 1 && r2 == 1 && r3 == 2) as co_total_3_threads_scope_same;

tests/Manual/Co-Total-4-threads.test

@@ -0,0 +1,27 @@
+.global x;
+.global f1;
+.global f2;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.release.sys [f1], 1;
+}
+
+d0.b0.t1 {
+  st.weak [x], 2;
+  st.release.sys [f2], 1;
+}
+
+d0.b0.t2 {
+  ld.acquire.sys r0, [f1];
+  ld.acquire.sys r1, [f2];
+  ld.weak r2, [x];
+}
+
+d0.b0.t3 {
+  ld.acquire.sys r3, [f1];
+  ld.acquire.sys r4, [f2];
+  ld.weak r5, [x];
+}
+
+permit(r0 == 1 && r1 == 1 && r2 == 1 && r3 == 1 && r4 == 1 && r5 == 2) as co_total_4_threads;

tests/Manual/CoRR-acquire-weak.test

@@ -0,0 +1,12 @@
+.global x;
+
+d0.b0.t0 {
+  st.release.gpu [x], 1;
+}
+
+d0.b1.t0 {
+  ld.acquire.gpu r1, [x];
+  ld.weak r2, [x];
+}
+
+assert (r1 != 1 || r2 != 0) as CoRR_acquire_weak;

tests/Manual/CoRR-relaxed-acquire-weak.test

@@ -0,0 +1,14 @@
+.global x;
+
+d0.b0.t0 {
+  st.release.gpu [x], 1;
+  st.release.gpu [x], 2;
+}
+
+d0.b1.t0 {
+  ld.relaxed.gpu r1, [x];
+  ld.acquire.gpu r2, [x];
+  ld.weak r3, [x];
+}
+
+permit (r1 == 2 || r3 == 1) as CoRR_relaxed_acquire_weak;

tests/Manual/CoRR-weak-acquire-weak.test

@@ -0,0 +1,14 @@
+.global x;
+
+d0.b0.t0 {
+  st.release.gpu [x], 1;
+  st.weak [x], 2;
+}
+
+d0.b1.t0 {
+  ld.weak r1, [x];
+  ld.acquire.gpu r2, [x];
+  ld.weak r3, [x];
+}
+
+permit (r1 == 2 || r3 == 1) as CoRR_relaxed_acquire_weak;

tests/Manual/CoRR-weak-acquire.test

@@ -0,0 +1,12 @@
+.global x;
+
+d0.b0.t0 {
+  st.release.gpu [x], 1;
+}
+
+d0.b1.t0 {
+  ld.weak r1, [x];
+  ld.acquire.gpu r2, [x];
+}
+
+permit (r1 == 0 || r2 == 1) as CoRR_acquire_weak;

tests/Manual/CoRW-R.test

@@ -0,0 +1,13 @@
+.global x;
+
+d0.b0.t0 {
+  st.release.sys [x], 1;
+}
+
+d0.b1.t0 {
+  ld.acquire.sys r1, [x];
+  st.weak [x], 2;
+  ld.weak r2, [x];
+}
+
+assert (r1 != 1 || r2 != 1) as CoRW_R;

tests/Manual/CoWR-R.test

@@ -0,0 +1,13 @@
+.global x;
+
+d0.b0.t0 {
+  st.release.gpu [x], 1;
+}
+
+d0.b1.t0 {
+  st.release.sys [x], 2;
+  ld.weak r1, [x];
+  ld.weak r2, [x];
+}
+
+permit (r1 == 1 && r2 == 1) as CoWR_R;

tests/Manual/CoWW-R.test

@@ -0,0 +1,9 @@
+.global x;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.weak [x], 2;
+  ld.acquire.sys r1, [x];
+}
+
+assert (r1 != 1) as CoWW_R;

tests/Manual/CoWW-RR.test

@@ -0,0 +1,13 @@
+.global x;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.weak [x], 2;
+}
+
+d0.b0.t1 {
+  ld.weak r0, [x];
+  ld.weak r1, [x];
+}
+
+permit(r0 == 2 && r1 ==1) as check_co;

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;

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;

tests/Manual/MP-3-transitive.test

@@ -0,0 +1,21 @@
+// Adapted from Figure 6 of paper: Heterogeneous-race-free Memory Models
+.global x;
+.global y;
+.global z;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.release.cta [y], 1;
+}
+
+d0.b0.t0 {
+  ld.acquire.cta r0, [y] == 1;
+  st.release.gpu [z], 1;
+}
+
+d0.b1.t0 {
+  ld.acquire.gpu r1, [z] == 1;
+  ld.weak r2, [x];
+}
+
+assert (r2 == 1) as mp_transitive;

tests/Manual/MP-cta-gpu.test

@@ -0,0 +1,14 @@
+.global x;
+.global y;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.release.cta [y], 1;
+}
+
+d0.b0.t1 {
+  ld.acquire.gpu r1, [y];
+  ld.weak r2, [x];
+}
+
+assert (r1 != 1 || r2 == 1) as mp_cta;

tests/Manual/MP-cta.test

@@ -0,0 +1,14 @@
+.global x;
+.global y;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.release.cta [y], 1;
+}
+
+d0.b1.t0 {
+  ld.acquire.cta r1, [y];
+  ld.weak r2, [x];
+}
+
+permit (r1 == 1 || r2 != 1) as mp_cta;

tests/Manual/MP-gpu.test

@@ -0,0 +1,14 @@
+.global x;
+.global y;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.release.gpu [y], 1;
+}
+
+d0.b0.t1 {
+  ld.acquire.gpu r1, [y];
+  ld.weak r2, [x];
+}
+
+assert (r1 != 1 || r2 == 1) as mp_gpu;

tests/Manual/MP-relaxed.test

@@ -0,0 +1,14 @@
+.global x;
+.global y;
+
+d0.b0.t0 {
+  st.release.sys [x], 1;
+  st.release.sys [y], 1;
+}
+
+d0.b0.t1 {
+  ld.relaxed.sys r1, [y];
+  ld.acquire.gpu r2, [x];
+}
+
+permit (r1 == 1 && r2 != 1) as mp_relaxed;

tests/Manual/MP-sys.test

@@ -0,0 +1,14 @@
+.global x;
+.global y;
+
+d0.b0.t0 {
+  st.weak [x], 1;
+  st.release.sys [y], 1;
+}
+
+d0.b0.t1 {
+  ld.acquire.sys r1, [y];
+  ld.weak r2, [x];
+}
+
+assert (r1 != 1 || r2 == 1) as mp_sys;

tests/Manual/Proxy-Alias-AliasFence.test

@@ -0,0 +1,10 @@
+.global x;
+.global y physically aliases x;
+
+d0.b0.t0 {
+  st.weak [x], 42;
+  fence.proxy.alias;
+  ld.weak r0, [y];
+}
+
+assert (r0 == 42) as proxy_alias;

tests/Manual/Proxy-SingleThread-rf-surW-surF-genR.test

@@ -0,0 +1,11 @@
+.global x;
+.texref t virtually aliases x;
+.surfref s virtually aliases x;
+
+d0.b0.t0 {
+  sust.weak [s], 1;
+  fence.proxy.surface;
+  ld.weak r0, [x];
+}
+
+assert (r0 == 1) as proxy_alias;