add privIsScoped check and update tests (#578)

hernanponcedeleon · Nov 28, 2023 · 27f88cd · 27f88cd
1 parent 5540b93
commit 27f88cd
Show file tree

Hide file tree

Showing 8 changed files with 14 additions and 15 deletions.
diff --git a/cat/spirv-check.cat b/cat/spirv-check.cat
@@ -172,6 +172,10 @@ flag ~empty nonprivIsRW as checkNonprivIsRW
 let atomicIsNonpriv = ([ATOM] \ [NONPRIV])
 flag ~empty atomicIsNonpriv as checkAtomicIsNonpriv
 
+// Private operations are not scoped
+let privIsScoped = ([PRIV] & [DV | QF | WG | SG])
+flag ~empty privIsScoped as checkPrivIsScoped
+
 // Atomic operations implicitly have availability/visibility operations
 let atomicIsAv = ([W & ATOM] \ [AV])
 flag ~empty atomicIsAv as checkAtomicIsAv

diff --git a/...agnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java b/...agnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java
@@ -423,11 +423,6 @@ private void tagControl(Event e, Boolean atomic, String mo, String avvis, String
             e.addTags(Tag.Vulkan.NON_PRIVATE);
         }
 
-        // add nonpriv tag to all M with scope
-        if (!scope.isEmpty() && (e instanceof MemoryEvent)) {
-            e.addTags(Tag.Vulkan.NON_PRIVATE);
-        }
-
         // Atomics implicitly have AV/VIS ops, hence they are implicitly nonpriv
         if (atomic && e instanceof Store) {
             e.addTags(Tag.Vulkan.AVAILABLE);

diff --git a/dartagnan/src/test/resources/VULKAN-CK-expected.csv b/dartagnan/src/test/resources/VULKAN-CK-expected.csv
@@ -69,7 +69,6 @@ litmus/VULKAN/Data-Race/test7-filter.litmus,1
 litmus/VULKAN/Data-Race/test9-filter.litmus,1
 litmus/VULKAN/Data-Race/waw-filter.litmus,1
 litmus/VULKAN/Kronos-Group/asmo.litmus,1
-litmus/VULKAN/Kronos-Group/asmo-weak.litmus,1
 litmus/VULKAN/Kronos-Group/atomicsc.litmus,1
 litmus/VULKAN/Kronos-Group/atomwrongsc.litmus,1
 litmus/VULKAN/Kronos-Group/cbarinst.litmus,1
@@ -144,6 +143,7 @@ litmus/VULKAN/Kronos-Group/test5.litmus,1
 litmus/VULKAN/Kronos-Group/test6.litmus,1
 litmus/VULKAN/Kronos-Group/test9.litmus,1
 litmus/VULKAN/Kronos-Group/waw.litmus,1
+litmus/VULKAN/Manual/asmo-weak.litmus,1
 litmus/VULKAN/Manual/CoWW-RR.litmus,1
 litmus/VULKAN/Manual/SB-2-wg.litmus,1
 litmus/VULKAN/Manual/SB-2-dv.litmus,1

diff --git a/dartagnan/src/test/resources/VULKAN-DR-expected.csv b/dartagnan/src/test/resources/VULKAN-DR-expected.csv
@@ -85,4 +85,4 @@ litmus/VULKAN/Manual/MP-mesa-optimized.litmus,1
 litmus/VULKAN/Manual/XF-Barrier-relacq.litmus,1
 litmus/VULKAN/Manual/XF-Barrier-rlx.litmus,0
 litmus/VULKAN/Manual/XF-Barrier-weak.litmus,0
-litmus/VULKAN/Kronos-Group/asmo-weak.litmus,0
+litmus/VULKAN/Manual/asmo-weak.litmus,0
diff --git a/dartagnan/src/test/resources/VULKAN-expected.csv b/dartagnan/src/test/resources/VULKAN-expected.csv
@@ -1,5 +1,4 @@
 litmus/VULKAN/Kronos-Group/asmo.litmus,1
-litmus/VULKAN/Kronos-Group/asmo-weak.litmus,0
 litmus/VULKAN/Kronos-Group/atomicsc.litmus,1
 litmus/VULKAN/Kronos-Group/atomwrongsc.litmus,1
 litmus/VULKAN/Kronos-Group/cbarinst.litmus,1
@@ -74,6 +73,7 @@ litmus/VULKAN/Kronos-Group/test5.litmus,1
 litmus/VULKAN/Kronos-Group/test6.litmus,1
 litmus/VULKAN/Kronos-Group/test9.litmus,1
 litmus/VULKAN/Kronos-Group/waw.litmus,1
+litmus/VULKAN/Manual/asmo-weak.litmus,0
 litmus/VULKAN/Manual/ticketlock-same-wg.litmus,0
 litmus/VULKAN/Manual/ticketlock-diff-wg.litmus,1
 litmus/VULKAN/Manual/ticketlock-acq2rlx-1.litmus,0

diff --git a/litmus/VULKAN/Manual/MP-no-avvis.litmus b/litmus/VULKAN/Manual/MP-no-avvis.litmus
@@ -6,7 +6,7 @@ x=0;
 y=0;
 }
  P0@sg 0, wg 0, qf 0            | P1@sg 1,wg 0, qf 0              ;
- st.dv.sc0 x, 1                 | ld.atom.acq.wg.sc0.semsc0 r0, y ;
- st.atom.rel.wg.sc0.semsc0 y, 1 | ld.dv.sc0 r1, x                 ;
+ st.sc0 x, 1                    | ld.atom.acq.wg.sc0.semsc0 r0, y ;
+ st.atom.rel.wg.sc0.semsc0 y, 1 | ld.sc0 r1, x                    ;
 exists
 (P1:r0 == 1 /\ P1:r1 == 0)
diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus
@@ -10,13 +10,13 @@ P1:r0=0;
 }
  P0@sg 0, wg 0, qf 0 | P1@sg 0, wg 1, qf 0 | P2@sg 0, wg 1, qf 0 ;
  st.av.dv.sc0 x, 1   | cbar.wg 1           | cbar.wg 1           ;
- LC00:               | st.dv.sc0 f, 1      | cbar.wg 2           ;
- ld.dv.sc0 r2, f     | LC10:               |                     ;
- bne r2, 0, LC01     | ld.dv.sc0 r2, f     |                     ;
+ LC00:               | st.sc0 f, 1         | cbar.wg 2           ;
+ ld.sc0 r2, f        | LC10:               |                     ;
+ bne r2, 0, LC01     | ld.sc0 r2, f        |                     ;
  goto LC00           | bne r2, 1, LC11     |                     ;
  LC01:               | goto LC10           |                     ;
  cbar.wg 1           | LC11:               |                     ;
- st.dv.sc0 f, 0      | cbar.wg 2           |                     ;
+ st.sc0 f, 0         | cbar.wg 2           |                     ;
                      | ld.vis.dv.sc0 r1, x |                     ;
 exists
 (P1:r2 != 1 /\ P1:r1 == 0)
diff --git a/litmus/VULKAN/Kronos-Group/asmo-weak.litmus → litmus/VULKAN/Manual/asmo-weak.litmus b/litmus/VULKAN/Kronos-Group/asmo-weak.litmus → litmus/VULKAN/Manual/asmo-weak.litmus
@@ -8,7 +8,7 @@ P3:r3=0;
 x=0;
 }
  P0@sg 0,wg 0, qf 0 | P1@sg 0,wg 1, qf 0  | P2@sg 0,wg 2, qf 0   | P3@sg 0,wg 3, qf 0   ;
- st.dv.sc0 x, 1     | st.dv.sc0 x, 2      | ld.atom.dv.sc0 r0, x | ld.atom.dv.sc0 r2, x ;
+ st.sc0 x, 1        | st.sc0 x, 2         | ld.atom.dv.sc0 r0, x | ld.atom.dv.sc0 r2, x ;
                     |                     | ld.atom.dv.sc0 r1, x | ld.atom.dv.sc0 r3, x ;
 ~exists
 (P2:r0 == 1 /\ P2:r1 == 2 /\ P3:r2 == 2 /\ P3:r3 == 1)