Properly define asmo and fr in Vulkan (#528)

Signed-off-by: Hernan Ponce de Leon <[email protected]> Co-authored-by: Hernan Ponce de Leon <[email protected]>
hernanponcedeleon · Oct 7, 2023 · 3f3c8ce · 3f3c8ce
1 parent 35f36bc
commit 3f3c8ce
Show file tree

Hide file tree

Showing 10 changed files with 59 additions and 8 deletions.
diff --git a/cat/ptx-v6.0.cat b/cat/ptx-v6.0.cat
@@ -17,7 +17,9 @@ PTX
 (*******************)
 
 // Explicitly add transitivity for coherence since the co in PTX is not total
+// and recompute fr based on the new co
 let co = co+
+let fr = rf^-1; co
 
 (* Events *)
 let strong-write = W & (RLX | REL)

diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat
@@ -31,7 +31,9 @@ PTX
 (*******************)
 
 // Explicitly add transitivity for coherence since the co in PTX is not total
+// and recompute fr based on the new co
 let co = co+
+let fr = rf^-1; co
 
 (* Events *)
 let strong-write = W & (RLX | REL)

diff --git a/cat/spirv-check.cat b/cat/spirv-check.cat
@@ -44,7 +44,8 @@ let inscope = (DV * DV) |
               (swg & ((DV | QF | WG) * (DV | QF | WG))) |
               (ssg & ((DV | QF | WG | SG) * (DV | QF | WG | SG)))
 
-let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id // mutually ordered atomics
+ // mutually ordered atomics
+ let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id
 
 let avvisSem = ((SC0 | SC1) * (AVDEVICE | VISDEVICE))
                 | (SC0 * ((SEMAV | SEMVIS) & SEMSC0))
@@ -56,7 +57,13 @@ let avvisinc = ((avvisSem | avvisSem^-1) \ id) |
 let posctosem = ((SC0 * SEMSC0) | (SC1 * SEMSC1)) & po
 let posemtosc = ((SEMSC0 * SC0) | (SEMSC1 * SC1)) & po
 
-let asmo = co & (ATOM * ATOM)
+let asmo = co & ((ATOM | IW) * ATOM)
+// From-read is defined based on scoped modification order
+// instead of coherence. For reads that read-from init, they
+// from-read all writes at the same location.
+let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id))
+let fre = fr & ext
+
 let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
 let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
 

diff --git a/cat/spirv-nochains.cat b/cat/spirv-nochains.cat
@@ -57,7 +57,13 @@ let avvisinc = ((avvisSem | avvisSem^-1) \ id) |
 let posctosem = ((SC0 * SEMSC0) | (SC1 * SEMSC1)) & po
 let posemtosc = ((SEMSC0 * SC0) | (SEMSC1 * SC1)) & po
 
-let asmo = co & (ATOM * ATOM)
+let asmo = co & ((ATOM | IW) * ATOM)
+// From-read is defined based on scoped modification order
+// instead of coherence. For reads that read-from init, they
+// from-read all writes at the same location.
+let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id))
+let fre = fr & ext
+
 let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
 let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
 
@@ -68,7 +74,7 @@ let sw = inscope & (
     ([REL & ATOM]; rs; (rf & mutordatom); [ATOM & R]; posctosem; [ACQ & F]) |                           // atomic->fence
     ([REL & F]; posemtosc; [ATOM & W]; hypors; (rf & mutordatom); [ATOM & R]; posctosem; [ACQ & F]) |   // fence->fence
     // (stor[CBAR]) terms are redundant because scbarinst is an equivalence relation on scbarinst, but they make the sequence of instructions more clear.
-    ([REL & F]; po?; [CBAR]; ((syncbar & inscope) \ id); [CBAR]; po?; [ACQ & F])                               // fence->cbar->cbar->fence,
+    ([REL & F]; po?; [CBAR]; ((syncbar & inscope) \ id); [CBAR]; po?; [ACQ & F])                        // fence->cbar->cbar->fence,
 )
 
 let ithbsemsc0 = ( ssw |
@@ -139,7 +145,7 @@ acyclic (locord | rf | fr | asmo) as consistency-cycle
 empty (rf; ([R \ ATOM])) & (([W]; locord); ([W]; locord)+) as consistency-rf
 
 // rmw events are atomic
-empty rmw & (fre; coe) as atomic
+empty rmw & (fre; (asmo & ext)) as atomic
 
 let non-rmw-reads = (R \ RMW) * (R \ RMW)
 empty ((((locord | locord^-1) | mutordatom) \ non-rmw-reads) \ (loc \ id \ non-rmw-reads)) as locord-complete

diff --git a/cat/spirv.cat b/cat/spirv.cat
@@ -44,7 +44,8 @@ let inscope = (DV * DV) |
               (swg & ((DV | QF | WG) * (DV | QF | WG))) |
               (ssg & ((DV | QF | WG | SG) * (DV | QF | WG | SG)))
 
-let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id // mutually ordered atomics
+// mutually ordered atomics
+let mutordatom = (loc & vloc & inscope & (ATOM * ATOM)) \ id
 
 let avvisSem = ((SC0 | SC1) * (AVDEVICE | VISDEVICE))
                 | (SC0 * ((SEMAV | SEMVIS) & SEMSC0))
@@ -56,7 +57,13 @@ let avvisinc = ((avvisSem | avvisSem^-1) \ id) |
 let posctosem = ((SC0 * SEMSC0) | (SC1 * SEMSC1)) & po
 let posemtosc = ((SEMSC0 * SC0) | (SEMSC1 * SC1)) & po
 
-let asmo = co & (ATOM * ATOM)
+let asmo = co & ((ATOM | IW) * ATOM)
+// From-read is defined based on scoped modification order
+// instead of coherence. For reads that read-from init, they
+// from-read all writes at the same location.
+let fr = (rf^-1; asmo) | (([IW]; rf)^-1; ((loc;[W]) \ id))
+let fre = fr & ext
+
 let rs = [REL & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
 let hypors = [W & ATOM]; ((asmo \ (asmo; asmo+)); [RMW])*
 
@@ -138,7 +145,7 @@ acyclic (locord | rf | fr | asmo) as consistency-cycle
 empty (rf; ([R \ ATOM])) & (([W]; locord); ([W]; locord)+) as consistency-rf
 
 // rmw events are atomic
-empty rmw & (fre; coe) as atomic
+empty rmw & (fre; (asmo & ext)) as atomic
 
 let non-rmw-reads = (R \ RMW) * (R \ RMW)
 empty ((((locord | locord^-1) | mutordatom) \ non-rmw-reads) \ (loc \ id \ non-rmw-reads)) as locord-complete

diff --git a/dartagnan/src/test/resources/PTXv6_0-expected.csv b/dartagnan/src/test/resources/PTXv6_0-expected.csv
@@ -57,3 +57,4 @@ litmus/PTX/Manual/LB-dlb-no-fence-1,1
 litmus/PTX/Manual/LB-dlb-no-fence-2,1
 litmus/PTX/Nvidia/SB+bar-dyn-reg-const,0
 litmus/PTX/Nvidia/SB+bar-sta-reg-const,1
+litmus/PTX/Manual/CoWW-weak.litmus,1
diff --git a/dartagnan/src/test/resources/PTXv7_5-expected.csv b/dartagnan/src/test/resources/PTXv7_5-expected.csv
@@ -122,3 +122,4 @@ litmus/PTX/Manual/LB-dlb-no-fence-1.litmus,1
 litmus/PTX/Manual/LB-dlb-no-fence-2.litmus,1
 litmus/PTX/Nvidia/SB+bar-dyn-reg-const.litmus,0
 litmus/PTX/Nvidia/SB+bar-sta-reg-const.litmus,1
+litmus/PTX/Manual/CoWW-weak.litmus,1
diff --git a/dartagnan/src/test/resources/VULKAN-expected.csv b/dartagnan/src/test/resources/VULKAN-expected.csv
@@ -83,3 +83,4 @@ litmus/VULKAN/Manual/MP-mesa-fence-loop.litmus,0
 litmus/VULKAN/Manual/MP-mesa-optimized.litmus,1
 litmus/VULKAN/Manual/MP-avvis.litmus,0
 litmus/VULKAN/Manual/MP-no-avvis.litmus,1
+litmus/VULKAN/Manual/CoWW-RR.litmus,1
diff --git a/litmus/PTX/Manual/CoWW-RR.litmus b/litmus/PTX/Manual/CoWW-RR.litmus
@@ -0,0 +1,12 @@
+PTX CoWW-RR
+"Non-atomic memory operations may be observed by one thread in a different order than they were written by another thread"
+{
+P1:r0 = 0;
+P1:r1 = 0;
+x=0;
+}
+ P0@cta 0,gpu 0 | P1@cta 0,gpu 0 ;
+ st.weak x, 1   | ld.weak r0, x  ;
+ st.weak x, 2   | ld.weak r1, x  ;
+exists
+(P1:r0 == 2 /\ P1:r1 == 1)
diff --git a/litmus/VULKAN/Manual/CoWW-RR.litmus b/litmus/VULKAN/Manual/CoWW-RR.litmus
@@ -0,0 +1,12 @@
+Vulkan CoWW-RR
+"Non-atomic memory operations may be observed by one thread in a different order than they were written by another thread"
+{
+P1:r0 = 0;
+P1:r1 = 0;
+x=0;
+}
+ P0@sg 0, wg 0, qf 0 | P1@sg 0,wg 1, qf 0 ;
+ st.sc0 x, 1         | ld.sc0 r0, x       ;
+ st.sc0 x, 2         | ld.sc0 r1, x       ;
+exists
+(P1:r0 == 2 /\ P1:r1 == 1)