diff --git a/tests/Manual/Atom-plus-register.test b/tests/Manual/Atom-plus-register.test new file mode 100644 index 0000000..767ab71 --- /dev/null +++ b/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; diff --git a/tests/Manual/Cause-base-strong.test b/tests/Manual/Cause-base-strong.test new file mode 100644 index 0000000..79fd7ea --- /dev/null +++ b/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; diff --git a/tests/Manual/Cause-base-weak.test b/tests/Manual/Cause-base-weak.test new file mode 100644 index 0000000..ce311f0 --- /dev/null +++ b/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; diff --git a/tests/Manual/Co-Total-3-threads-scope-same.test b/tests/Manual/Co-Total-3-threads-scope-same.test new file mode 100644 index 0000000..10f5ff6 --- /dev/null +++ b/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; diff --git a/tests/Manual/Co-Total-4-threads.test b/tests/Manual/Co-Total-4-threads.test new file mode 100644 index 0000000..3744ca3 --- /dev/null +++ b/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; diff --git a/tests/Manual/CoRR-acquire-weak.test b/tests/Manual/CoRR-acquire-weak.test new file mode 100644 index 0000000..c4ea891 --- /dev/null +++ b/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; diff --git a/tests/Manual/CoRR-relaxed-acquire-weak.test b/tests/Manual/CoRR-relaxed-acquire-weak.test new file mode 100644 index 0000000..0195d06 --- /dev/null +++ b/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; diff --git a/tests/Manual/CoRR-weak-acquire-weak.test b/tests/Manual/CoRR-weak-acquire-weak.test new file mode 100644 index 0000000..2cde3e8 --- /dev/null +++ b/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; diff --git a/tests/Manual/CoRR-weak-acquire.test b/tests/Manual/CoRR-weak-acquire.test new file mode 100644 index 0000000..8856dc4 --- /dev/null +++ b/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; diff --git a/tests/Manual/CoRW-R.test b/tests/Manual/CoRW-R.test new file mode 100644 index 0000000..19cbf91 --- /dev/null +++ b/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; diff --git a/tests/Manual/CoWR-R.test b/tests/Manual/CoWR-R.test new file mode 100644 index 0000000..8054947 --- /dev/null +++ b/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; diff --git a/tests/Manual/CoWW-R.test b/tests/Manual/CoWW-R.test new file mode 100644 index 0000000..1592a92 --- /dev/null +++ b/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; diff --git a/tests/Manual/CoWW-RR.test b/tests/Manual/CoWW-RR.test new file mode 100644 index 0000000..7fed0b9 --- /dev/null +++ b/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; diff --git a/tests/Manual/Coherence-weak.test b/tests/Manual/Coherence-weak.test new file mode 100644 index 0000000..9921d19 --- /dev/null +++ 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 new file mode 100644 index 0000000..b538822 --- /dev/null +++ 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; diff --git a/tests/Manual/MP-3-transitive.test b/tests/Manual/MP-3-transitive.test new file mode 100644 index 0000000..75edafe --- /dev/null +++ b/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; diff --git a/tests/Manual/MP-cta-gpu.test b/tests/Manual/MP-cta-gpu.test new file mode 100644 index 0000000..843b9c0 --- /dev/null +++ b/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; diff --git a/tests/Manual/MP-cta.test b/tests/Manual/MP-cta.test new file mode 100644 index 0000000..964ac8e --- /dev/null +++ b/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; diff --git a/tests/Manual/MP-gpu.test b/tests/Manual/MP-gpu.test new file mode 100644 index 0000000..726b75e --- /dev/null +++ b/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; diff --git a/tests/Manual/MP-relaxed.test b/tests/Manual/MP-relaxed.test new file mode 100644 index 0000000..c84f0ab --- /dev/null +++ b/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; diff --git a/tests/Manual/MP-sys.test b/tests/Manual/MP-sys.test new file mode 100644 index 0000000..78feb13 --- /dev/null +++ b/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; diff --git a/tests/Manual/Proxy-Alias-AliasFence.test b/tests/Manual/Proxy-Alias-AliasFence.test new file mode 100644 index 0000000..37f64d4 --- /dev/null +++ b/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; diff --git a/tests/Manual/Proxy-SingleThread-rf-surW-surF-genR.test b/tests/Manual/Proxy-SingleThread-rf-surW-surF-genR.test new file mode 100644 index 0000000..270b9d3 --- /dev/null +++ b/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; diff --git a/tests/Manual/SB+acq_rel-cta.test b/tests/Manual/SB+acq_rel-cta.test new file mode 100644 index 0000000..e5a5354 --- /dev/null +++ b/tests/Manual/SB+acq_rel-cta.test @@ -0,0 +1,16 @@ +.global x; +.global y; + +d0.b0.t0 { + st.release.cta [x], 1; + fence.acq_rel.cta; + ld.acquire.cta r1, [y]; +} + +d0.b0.t1 { + st.release.cta [y], 1; + fence.acq_rel.cta; + ld.acquire.cta r2, [x]; +} + +permit (r1 == 1 && r2 == 0) as SB_acq_rel_cta; diff --git a/tests/Manual/SB+sc-cta-outScope.test b/tests/Manual/SB+sc-cta-outScope.test new file mode 100644 index 0000000..cc2a8b6 --- /dev/null +++ b/tests/Manual/SB+sc-cta-outScope.test @@ -0,0 +1,16 @@ +.global x; +.global y; + +d0.b0.t0 { + st.weak [x], 1; + fence.sc.cta; + ld.weak r0, [y]; +} + +d0.b1.t0 { + st.weak [y], 1; + fence.sc.cta; + ld.weak r1, [x]; +} + +permit (r0 == 1 || r1 == 1) as SB_acq_rel_cta; diff --git a/tests/Manual/SB+sc-cta.test b/tests/Manual/SB+sc-cta.test new file mode 100644 index 0000000..1f164cf --- /dev/null +++ b/tests/Manual/SB+sc-cta.test @@ -0,0 +1,16 @@ +.global x; +.global y; + +d0.b0.t0 { + st.weak [x], 1; + fence.sc.cta; + ld.weak r0, [y]; +} + +d0.b0.t1 { + st.weak [y], 1; + fence.sc.cta; + ld.weak r1, [x]; +} + +permit (r0 == 1 || r1 != 1) as SB_acq_rel_cta; diff --git a/tests/Manual/SB+sc-gpu-multipleFence-TotalOrder.test b/tests/Manual/SB+sc-gpu-multipleFence-TotalOrder.test new file mode 100644 index 0000000..aa3c536 --- /dev/null +++ b/tests/Manual/SB+sc-gpu-multipleFence-TotalOrder.test @@ -0,0 +1,21 @@ +.global x; +.global y; + +d0.b0.t0 { + st.weak [x], 1; + fence.sc.gpu; + st.weak [x], 2; + fence.sc.gpu; + ld.weak r1, [y]; + +} + +d0.b1.t0 { + st.weak [y], 1; + fence.sc.gpu; + st.weak [y], 2; + fence.sc.gpu; + ld.weak r2, [x]; +} + +permit (r1 == 2 || r2 == 2) as SB_sc_gpu_multiFence; diff --git a/tests/Manual/SB+sc-gpu-multipleFence.test b/tests/Manual/SB+sc-gpu-multipleFence.test new file mode 100644 index 0000000..afb82b2 --- /dev/null +++ b/tests/Manual/SB+sc-gpu-multipleFence.test @@ -0,0 +1,21 @@ +.global x; +.global y; + +d0.b0.t0 { + st.weak [x], 1; + fence.sc.gpu; + st.weak [x], 2; + fence.sc.gpu; + ld.weak r1, [y]; + +} + +d0.b1.t0 { + st.weak [y], 1; + fence.sc.gpu; + st.weak [y], 2; + fence.sc.gpu; + ld.weak r2, [x]; +} + +assert (r1 == 2 || r2 == 2) as SB_sc_gpu_multiFence; diff --git a/tests/Manual/SB+sc-gpu.test b/tests/Manual/SB+sc-gpu.test new file mode 100644 index 0000000..075912e --- /dev/null +++ b/tests/Manual/SB+sc-gpu.test @@ -0,0 +1,16 @@ +.global x; +.global y; + +d0.b0.t0 { + st.weak [x], 1; + fence.sc.gpu; + ld.weak r0, [y]; +} + +d0.b1.t0 { + st.weak [y], 1; + fence.sc.gpu; + ld.weak r1, [x]; +} + +assert (r0 == 1 || r1 == 1) as SB_acq_rel_cta; diff --git a/tests/Manual/SB+sc-sys-gpu.test b/tests/Manual/SB+sc-sys-gpu.test new file mode 100644 index 0000000..bf98580 --- /dev/null +++ b/tests/Manual/SB+sc-sys-gpu.test @@ -0,0 +1,16 @@ +.global x; +.global y; + +d0.b0.t0 { + st.weak [x], 1; + fence.sc.sys; + ld.weak r0, [y]; +} + +d0.b1.t0 { + st.weak [y], 1; + fence.sc.gpu; + ld.weak r1, [x]; +} + +assert (r0 == 1 || r1 == 1) as SB_sc_sys_gpu; diff --git a/tests/Manual/SB+sc-sys.test b/tests/Manual/SB+sc-sys.test new file mode 100644 index 0000000..3060c10 --- /dev/null +++ b/tests/Manual/SB+sc-sys.test @@ -0,0 +1,16 @@ +.global x; +.global y; + +d0.b0.t0 { + st.weak [x], 1; + fence.sc.sys; + ld.weak r0, [y]; +} + +d0.b1.t0 { + st.weak [y], 1; + fence.sc.sys; + ld.weak r1, [x]; +} + +assert (r0 == 1 || r1 == 1) as SB_acq_rel_cta; diff --git a/tests/Manual/SB-weak.test b/tests/Manual/SB-weak.test new file mode 100644 index 0000000..7c5a266 --- /dev/null +++ b/tests/Manual/SB-weak.test @@ -0,0 +1,14 @@ +.global x; +.global y; + +d0.b0.t0 { + st.weak [x], 1; + ld.weak r1, [y]; +} + +d0.b1.t0 { + st.weak [y], 1; + ld.weak r2, [x]; +} + +permit (r1 != 1 && r2 != 1) as SB_acq_rel_cta;