From ad03ba3ac7c361d5e458bf94a7c8088ae98b652b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?=E8=83=BD=E8=80=90=E5=AE=81?= Date: Sun, 21 May 2023 15:59:13 +0300 Subject: [PATCH] Add SC-per-Location Axiom This commit adds the Sequential Consistency Per Location axiom(https://docs.nvidia.com/cuda/parallel-thread-execution/index.html#sc-per-loc-axiom) which is missing in the model. We add a litmus test from issue(https://github.com/NVlabs/mixedproxy/issues/4). If the Program Order (PO) relation removed from cause_base relation which makes the model roll back to ptx-v6.0 (proxy-less version), this test shows the SC-per-Location axiom is missing. Co-authored-by: Hernan Ponce de Leon --- alloy/ptx.als | 6 +++++- tests/SC_per_location.test | 21 +++++++++++++++++++++ 2 files changed, 26 insertions(+), 1 deletion(-) create mode 100644 tests/SC_per_location.test diff --git a/alloy/ptx.als b/alloy/ptx.als index d54b512..1bff2cd 100644 --- a/alloy/ptx.als +++ b/alloy/ptx.als @@ -129,8 +129,12 @@ pred no_thin_air { acyclic[rf + dep] } +pred sc_per_location { + acyclic[strong[com] + po_loc] +} + pred ptx_mm { - no_thin_air and atomicity and coherence and causality and seq_cst + no_thin_air and atomicity and coherence and causality and seq_cst and sc_per_location } diff --git a/tests/SC_per_location.test b/tests/SC_per_location.test new file mode 100644 index 0000000..4412f91 --- /dev/null +++ b/tests/SC_per_location.test @@ -0,0 +1,21 @@ +.global x; +.global f1; +.global f2; + +d0.b0.t0 { + st.release.sys [x], 1; + st.release.sys [f1], 1; +} + +d0.b1.t0 { + st.release.gpu [x], 2; + ld.acquire.sys r0, [x]; + st.release.sys [f2], 1; +} +d0.b2.t0 { + ld.acquire.sys r1, [f2]; + ld.acquire.sys r2, [f2]; + ld.acquire.sys r3, [x]; +} + +assert (r0 != 0 || r1 != 1 || r2 != 1 || r3 != 2) as my_test; \ No newline at end of file