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