diff --git a/cat/spirv-check.cat b/cat/spirv-check.cat index bffbbd4af0..e3da162858 100644 --- 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/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java index dcd8ed5bf4..2c3593780f 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusVulkan.java +++ b/dartagnan/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 index 5c30ccc4ea..781ea4fb8b 100644 --- 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 index 728d9d2d77..19bc6c8f0c 100644 --- 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 index 6f793fd3fb..e00ec6488c 100644 --- 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 index de035e9caf..4678465857 100644 --- 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) \ No newline at end of file diff --git a/litmus/VULKAN/Manual/XF-Barrier-weak.litmus b/litmus/VULKAN/Manual/XF-Barrier-weak.litmus index 9d7497a6b2..b068555907 100644 --- 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) \ No newline at end of file diff --git a/litmus/VULKAN/Kronos-Group/asmo-weak.litmus b/litmus/VULKAN/Manual/asmo-weak.litmus similarity index 85% rename from litmus/VULKAN/Kronos-Group/asmo-weak.litmus rename to litmus/VULKAN/Manual/asmo-weak.litmus index a69707b5e0..b5d0510e43 100644 --- a/litmus/VULKAN/Kronos-Group/asmo-weak.litmus +++ b/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) \ No newline at end of file