Restrict avvisinc relation by event type

alloy/spirv.als

@@ -153,21 +153,21 @@ sig Exec {
   // inverse) and add the identity over R+W
   sref = ^(rai[pgmsref]) + stor[R+W]
 
-  // AVDEVICE operation applies to all operations that are ordered before
+  // AVDEVICE operation applies to all writes that are ordered before
   // the current operation, but not to the current operation itself.
-  // VISDEVICE operation applies to all operations that are ordered after
+  // VISDEVICE operation applies to all reads that are ordered after
   // the current operation, but not to the current operation itself.
-  // SEMAV operation with SEMSCi applies to all operations in SCi that are ordered before
+  // SEMAV operation with SEMSCi applies to all writes in SCi that are ordered before
   // the current operation, but not to the current operation itself.
-  // SEMVIS operation with SEMSCi applies to all operations in SCi that are ordered after
+  // SEMVIS operation with SEMSCi applies to all reads in SCi that are ordered after
   // the current operation, but not to the current operation itself.
   // AV+VIS ops (per-instruction) are avvisinc with themselves (av/vis op happens in the right order)
   // and with those operations on the same reference.
   // Note that this complexity exists in part because we don't split out implicit av/vis
   // ops as distinct instructions.
-  avvisinc = ((SC0+SC1)->AVDEVICE) + (VISDEVICE->(SC0+SC1)) +
-             (SC0->(SEMSC0&SEMAV)) + ((SEMSC0&SEMVIS)->SC0) +
-             (SC1->(SEMSC1&SEMAV)) + ((SEMSC1&SEMVIS)->SC1) +
+  avvisinc = (W->AVDEVICE) + (VISDEVICE->R) +
+             ((W&SC0)->(SEMSC0&SEMAV)) + ((SEMSC0&SEMVIS)->(R&SC0)) +
+             ((W&SC1)->(SEMSC1&SEMAV)) + ((SEMSC1&SEMVIS)->(R&SC1)) +
              (rai[stor[AV+VIS] . (sref & sloc)])
 
   // same thread is a subset of same subgroup which is a subset of same workgroup

alloy/tests/mpinscope6.test

@@ -0,0 +1,17 @@
+// Copyright (c) 2025 Khronos Group. This work is licensed under a
+// Creative Commons Attribution 4.0 International License; see
+// http://creativecommons.org/licenses/by/4.0/
+
+NEWWG
+NEWSG
+NEWTHREAD
+st.nonpriv.sc0 x = 1
+membar.acq.rel.scopeqf.semsc0.semsc1.semav
+st.atom.rel.scopeqf.sc1.semsc1 y = 1
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopeqf.sc1.semsc0.semsc1.semvis y = 1
+ld.nonpriv.sc0 x = 0
+
+NOSOLUTION consistent[X]

alloy/tests/mpnotinscope7.test

@@ -0,0 +1,18 @@
+// Copyright (c) 2025 Khronos Group. This work is licensed under a
+// Creative Commons Attribution 4.0 International License; see
+// http://creativecommons.org/licenses/by/4.0/
+
+NEWWG
+NEWSG
+NEWTHREAD
+st.nonpriv.sc0 x = 1
+membar.acq.rel.scopewg.semsc0.semsc1.semav
+st.atom.rel.scopeqf.sc1.semsc1 y = 1
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopeqf.sc1.semsc0.semsc1.semvis y = 1
+ld.nonpriv.sc0 x = 0
+
+SATISFIABLE consistent[X] && #dr>0
+NOSOLUTION consistent[X] && #dr=0

alloy/tests/mpnotinscope8.test

@@ -0,0 +1,18 @@
+// Copyright (c) 2025 Khronos Group. This work is licensed under a
+// Creative Commons Attribution 4.0 International License; see
+// http://creativecommons.org/licenses/by/4.0/
+
+NEWWG
+NEWSG
+NEWTHREAD
+st.nonpriv.sc0 x = 1
+membar.acq.rel.scopewg.semsc0.semsc1.semav.semvis
+st.atom.rel.scopeqf.sc1.semsc1 y = 1
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopeqf.sc1.semsc0.semsc1.semvis y = 1
+ld.nonpriv.sc0 x = 0
+
+SATISFIABLE consistent[X] && #dr>0
+NOSOLUTION consistent[X] && #dr=0